[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?
    Thank you!