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