|Page 320 of 800||Search internet|
The following constructs allow to assume that a side condition holds:
line L : Condition >> C ; N
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|