PAOE02
Premises:
(forall ?X (not (= 0 (succ ?X)))) (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 ?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)))) (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:
(even (* 0 0))