[PVS-Help] two problems

[applehopedream <applehopedream@xxxxxxx>]

 Hello,

 

    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!

 

---

22元超值饭面,8.5折纯珍比萨,必胜宅急送网上点餐优惠多