PAOE07Ind

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 (= (* ?X 0) 0))
(forall (?X ?Y) (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X)))
(forall (?X ?Y) (<=> (= (* ?X 0) ?Y) (= 0 ?Y)))
(forall (?X ?Y ?Z) (<=> (= (* ?X (succ ?Y)) ?Z) (= (+ (* ?X ?Y) ?X) ?Z)))
(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?X ?Y) (* ?X ?Z))) (= ?Y ?Z)))
(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?Y ?X) (* ?Z ?X))) (= ?Y ?Z)))
(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z))))
(forall (?X ?Y ?Z) (= (* (+ ?Y ?Z) ?X) (+ (* ?Y ?X) (* ?Z ?X))))
(forall ?X (= ?X (* (succ 0) ?X)))
(forall ?X (= ?X (* ?X (succ 0))))
(forall ?X (= (* 0 ?X) 0))
(forall (?X ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y)))
(forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))
(forall (?X ?Y ?Z) (= (* (* ?X ?Y) ?Z) (* ?X (* ?Y ?Z))))
(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 (= (+ 0 ?X) ?X))
(forall ?X (= (succ ?X) (+ ?X (succ 0))))
(forall ?X (= (succ ?X) (+ (succ 0) ?X)))
(forall ?Y (= (succ (succ (+ 0 ?Y))) (+ (succ 0) (succ ?Y))))
(forall ?X (=> (not (exists ?Y (= ?X (+ ?Y ?Y)))) (exists ?Y (= (succ ?X) (+ ?Y ?Y)))))
(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))
(forall (?X ?Y) (=> (= (succ ?X) ?Y) (= ?Y (+ ?X (succ 0)))))
(forall ?X (= (+ (succ ?X) 0) (succ (+ ?X 0))))
(forall (?X ?Y) (forall ?Z (=> (and (= ?X (+ ?Y ?Y)) (= ?X (+ ?Z ?Z))) (= ?Y ?Z))))
(forall (?X ?Y ?Z) (=> (= (succ ?X) (+ (succ ?Y) (succ ?Z))) (= ?X (succ (+ ?Y ?Z)))))
(forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))
(not (exists ?X (= 0 (+ (succ ?X) (succ ?X)))))
(forall (?X ?Y) (= (+ (succ 0) (+ ?X ?Y)) (succ (+ ?X ?Y))))
(forall (?X ?Y) (=> (= 0 (+ ?X ?Y)) (and (= 0 ?X) (= 0 ?Y))))
(forall (?X ?Y) (=> (= (+ ?X ?X) (+ ?Y ?Y)) (= ?X ?Y)))
(forall (?X ?Y ?Z) (=> (= (+ ?Z ?X) (+ ?Y ?X)) (= ?Z ?Y)))
(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (succ ?Y) (succ ?Z))))
(= 0 (+ 0 0))
(forall (?X ?Y) (=> (= (+ 0 ?X) (+ 0 ?Y)) (= ?X ?Y)))
(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))
(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= ?Y ?Z)))
(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (+ (succ ?X) (succ ?Y)) (+ (succ ?Z) (succ ?W)))))
(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))
(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))
(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))
(forall (?X ?Y) (=> (= (succ (succ ?X)) (succ (succ ?Y))) (= ?X ?Y)))
(forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X))))
(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (succ (+ ?X ?Y)) (succ (+ ?Z ?W)))))
(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (succ (+ ?X ?Y)) (succ ?Z))))
(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))
(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (+ ?X (succ ?Y)) (+ ?X (succ ?Z)))))
(forall (?X ?Y ?Z) (<=> (= (+ ?Y ?X) (+ ?Z ?X)) (= (+ (succ ?Y) ?X) (+ (succ ?Z) ?X))))
(forall (?X ?Y) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))
(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))
(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))
(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (succ ?Z)) (= (+ ?X ?Y) ?Z)))
(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z))) (= (+ ?X ?Y) ?Z)))
(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z)))))
(forall (?X ?Y) (<=> (= (+ 0 0) (+ ?X ?X)) (= 0 ?X)))
(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?X ?Z) (+ ?Y ?Z))))
(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?Z ?X) (+ ?Z ?Y))))
(forall (?X ?Y) (=> (= (+ ?X ?Y) ?X) (= ?Y 0)))
(forall ?X (not (= ?X (succ ?X))))
(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))
(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))
(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= (+ ?X ?Y) (+ ?X ?Z))))
(forall (?X ?Y ?Z) (<=> (= (+ ?Y (succ ?X)) (+ ?Z (succ ?X))) (= (+ ?Y ?X) (+ ?Z ?X))))
(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) ?Z) (= (+ ?X ?Y) (succ ?Z))))
(forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X)))
(forall (?X ?Y ?Z) (= (+ (+ ?X ?Y) ?Z) (+ ?X (+ ?Y ?Z))))
(even 0)
(even (+ 0 0))
(not (even (succ 0)))
(even (succ (succ 0)))
(odd (succ 0))
(not (odd 0))
(forall ?X (=> (even ?X) (even (+ 0 ?X))))
(forall ?X (even (+ ?X ?X)))
(forall ?X (<=> (even ?X) (not (odd ?X))))
(forall ?X (=> (even ?X) (even (+ ?X ?X))))
(forall ?X (or (even ?X) (odd ?X)))
(forall ?X (=> (even ?X) (even (succ (succ ?X)))))
(forall ?X (=> (even ?X) (even (+ (succ (succ 0)) ?X))))
(forall ?X (=> (even ?X) (odd (succ ?X))))
(forall ?X (<=> (even ?X) (not (odd ?X))))
(forall ?X (=> (odd ?X) (even (succ ?X))))
(forall ?X (=> (odd ?X) (odd (succ (succ ?X)))))
(forall ?X (<=> (odd ?X) (not (even ?X))))
(forall (?X ?Y) (=> (and (even ?X) (even ?Y)) (even (+ ?X ?Y))))
(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ (succ ?X) (succ ?Y)))))
(forall (?X ?Y) (=> (and (odd ?X) (odd ?Y)) (even (+ ?X ?Y))))
(forall (?X ?Y) (=> (and (odd ?X) (even ?Y)) (odd (+ ?X ?Y))))
(forall (?X ?Y) (=> (odd (+ ?X ?Y)) (or (odd ?X) (odd ?Y))))
(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))
(forall ?X (=> (even (succ (succ ?X))) (even ?X)))
(forall ?X(or (not (odd ?X)) (not (even ?X))))
(forall (?X ?Y) (<=> (= ?Y (+ (+ ?X ?X) (succ 0))) (odd ?Y)))
(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ ?Y ?X))))

Conclusion:

Proof Trace