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