PrA56
Premises:
(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 (= (+ 0 ?X) ?X)) (forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y)))) (forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z))) (forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X)))) (forall ?X (= (succ ?X) (succ (+ ?X 0))))
Conclusion:
(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))