PAOE05bInd
Premises:
(forall ?X (<=> (even ?X) (exists ?Y (= ?X (+ ?Y ?Y))))) (forall ?X (<=> (odd ?X) (not (even ?X)))) (forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?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 (= (* ?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) (= (+ ?X ?Y) (+ ?Y ?X))) (forall ?X (even (* ?X 0))) (forall (?X ?Y) (<=> (even (* ?X ?Y)) (exists ?Z (= (+ ?Z ?Z) (* ?X ?Y) (+ ?Z ?Z)))))
Conclusion:
(forall (?X ?Y) (=> (even ?X) (even (* ?X ?Y))))
Proof Trace