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

[PVS-Help] two problems



 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折纯珍比萨,必胜宅急送网上点餐优惠多