|Page 336 of 800||Search internet|
The verify operation says that if the side condition endorses the conclusion , written , and if the side condition evaluates to , then we can conclude . The verification operator is named .
As an example of use, consider the following lemma and proof:
In Line L04 of the proof above, adaption replaces by to get rid of three meta-quantifiers and a side condition. The side condition evaluates to because avoids (i.e. does not occur free in ).
We may also prove the lemma thus:
Above, the verify operator has to be given explicitly because adaption is not applied to the second argument of ponens operators.
As noted later, one can write in place of .
|Page 336 of 800||Search logiweb.eu|