PrAOE16Ind
Premises:
(forall ?X (<=> (even ?X) (exists ?Y (= ?X (+ ?Y ?Y))))) (forall ?X (<=> (odd ?X) (not (even ?X)))) (odd (succ 0)) (forall ?X(or (not (odd ?X)) (not (even ?X)))) (forall ?X (=> (odd ?X) (odd (succ (succ ?X))))) (forall ?X (or (even ?X) (odd ?X)))
Conclusion:
(forall ?X (=> (even ?X) (odd (succ ?X))))
Proof Trace