[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] two problems
1.when I define the ^ as follows:
f1,f2,q : form
^(f1,f2)(q) : form = prj(cons(f1,cons(f2,null),empty(q))
when I prove some lemmas ,I want to introduce the definition of ^ in the antecedent formulas,then I use (lemma "abbr.^"),abbr is a theory which contains the definiton of ^,but the prover product this :
^=(lambda (f1,f2) : lambda (q) : prj(cons(f1,cons9f2,null)),empty(q)))
how could I get rid of "lambda"?
2.in the proving,if I want to substitute a definition in a formula just for partly,how could I do?