|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|