I am converting a program written in c language to typed transition system accepted by pvs theorem prover.a main program calls another procedure.
Procedure rt(int x, int y)
I want to express this .
I wrote two theories named rt and dt. when I tried to import dt in rt, an error message came “there is no next method for method” what is it.how to resolve it.