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

[PVS-Help] Another strange thing with PVS 6



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))))



  [condition type: simple-error]


Any idea?


Kind regards,

Sjaak Smetsers