PrA44
Premises:
(forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X))) (forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (succ ?Z)) (= (+ ?X ?Y) ?Z)))
Conclusion:
(forall (?Y ?X ?Z) (=> (= (+ (succ ?X) ?Y) (succ ?Z)) (= (+ ?X ?Y) ?Z)))