Page 320 of 800
| Page 320 of 800 | Search internet |
The following constructs allow to assume that a side condition holds:
line L : Condition >> C ; N
Example:
We say that the variable 
avoids the term 
, written 
if the variable does not occur free in the term . The lemma above says that if avoids and if 
then 
. The proof of the lemma reads:
In Line L01 we assume that avoids 
.
In Line L02 we assume as a premise and in Line L03 we generalize the premise.
Axiom 
of first order predicate calculus says:
In Line L04 we use modus probans on Axiom and the side condition we assumed in Line L01. Finally, we use modus ponens on Line L04 and Line L03.
Using a condition is the typical way to prove a lemma of form 
.
Do not use conditions in proof of form
T proof of L : P qed
where T is Prop, FOL, or Peano from the Peano page. The tactics of Prop, FOL, and Peano are not intended to be used together with conditions.
| Page 320 of 800 | Search logiweb.eu |