Sch11.17i
Premises:
(forall ?X (not (= 0 (1+ ?X)))) (forall (?X ?Y) (=> (not (= ?X ?Y)) (not (= (1+ ?X) (1+ ?Y))))) (forall ?X (= (+ ?X 0) ?X)) (forall (?X ?Y) (= (+ ?X (1+ ?Y)) (1+ (+ ?X ?Y))))
Conclusion:
(forall ?X (=> (= (+ 0 ?X) ?X) (= (+ 0 (1+ ?X)) (1+ ?X))))
Proof Trace