[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Another strange thing with PVS 6



Hi,

 

I’ve finally found a file in my project that type checked. However, when I tried to redo the proof the expansion of the function foldTerm produced the following error:

 

  |-------

{1}   foldTerm(e!1, a!1)(tapp(x!1, x!2)) =

       a!1(S_map(foldTerm(e!1, a!1))(x!1, x!2))

 

Rule? (expand "foldTerm")

Error: the assertion

       (every #'(lambda (sps)

                  (every #'(lambda (sfmla)

                             (null (freevars (formula sfmla))))

                         (s-forms (current-goal sps))))

              subgoal-proofstates)

       failed.

  [condition type: simple-error]

 

Any idea?

 

Kind regards,


Sjaak Smetsers