PrA59Ind
Premises:
(forall ?X (= (+ 0 ?X) ?X)) (forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y))) (forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y)))) (forall ?X (= (+ ?X 0) ?X)) (forall ?X (= (+ (succ 0) ?X) (succ ?X))) (forall (?X ?Y ?Z) (=> (= (+ (succ 0) ?X) (+ (succ 0) ?Y)) (= ?X ?Y))) (forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) ?Z) (= (+ ?X ?Y) (succ ?Z) ) ) )
Conclusion:
(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= (+ ?X ?Y) (+ ?X ?Z))))