Page 96 of 800
| Page 96 of 800 | Search internet |
Recall the proof of 
:
Line L09 references Lemma 
which says:
The unification tactic is not smart enough to see that induction is in 
. Thus, the meta variable 
of the lemma has to be instantiated to the object variable explicitly. That is done by the instantiation operator 
of the Logiweb sequent calculus in Line 
.
Apart from that, the unification tactic is smart enough to guess how all the other meta variables have to be instantiated. Furthermore, it guesses that the two side conditions have to be verified by evaluating them, so it adds two 'verify' sequent operators 
. The verify sequent operator eliminates a side condition by evaluating it and checking that the result is 
. Finally, the unification tactic uses meta modus ponens two times to get rid of the two premisses. The 
in the rules allows to do induction under an arbitrary hypothesis . That is needed if induction is used inside a hypothetical proof.
| Page 96 of 800 | Search logiweb.eu |