PA_JH05
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 ?Y) (+ ?Y ?X))) (forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X))) (forall ?X (forall ?Y (= (+ (succ ?X) ?X) (succ (+ ?X ?Y)))))
Conclusion:
(forall ?X (forall ?Y (= (+ (succ ?X) (succ ?Y)) (succ (+ ?X (succ ?Y))))))
Proof Trace