PrAOE12
Premises:
(forall ?X (<=> (even ?X) (exists ?Y (= ?X (+ ?Y ?Y))))) (forall ?X (<=> (odd ?X) (not (even ?X))))
Conclusion:
(forall ?X (=> (even ?X) (even (+ ?X ?X))))
Proof Trace