Sir, I am converting a program written in c language to typed transition system accepted by pvs theorem prover.a main program calls another procedure. For eg. Procedure rt(int x, int y) …….. ….. X=dt(a,b) . 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. |