PrA18pInd
Premises:
(forall ?X (not (= 0 (succ ?X)))) (forall ?X (= (+ 0 ?X) ?X)) (forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))
Conclusion:
(forall (?X ?Y) (=> (= 0 (+ ?X ?Y)) (and (= 0 ?X) (= 0 ?Y))))