PrALT22Ind
Premises:
(forall ?X (not (= 0 (succ ?X)))) (forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))) (forall (?X ?Y) (<=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))) (forall ?X (= (+ ?X 0) ?X)) (forall (?X ?Y) (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))) (forall (?X ?Y) (<=> (= (+ ?X 0) ?Y) (= ?X ?Y))) (forall (?X ?Y ?Z) (<=> (= (+ ?X (succ ?Y)) ?Z) (= (+ (+ ?X ?Y) (succ 0)) ?Z))) (forall (?X ?Y) (<=> (< ?X ?Y) (exists ?Z (and (not (= 0 ?Z)) (= (+ ?X ?Z) ?Y))))) (forall (?X ?Y) (<=> (exists ?Z (= ?X (+ ?Y ?Z))) (=< ?Y ?X))) (forall (?X ?Y) (<=> (=< ?X ?Y) (not (< ?Y ?X)))) (forall (?X ?Y) (or (=< ?X ?Y) (=< ?Y ?X))) (forall (?X ?Y) (<=> (=< ?X ?Y) (or (= ?X ?Y) (< ?X ?Y))))
Conclusion:
(forall (?X ?Y) (=> (and (=< ?X ?Y) (=< ?Y ?X)) (= ?X ?Y)))