Sch11.16
Premises:
(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y)))) (forall ?X (= (+ ?X 0) ?X)) (forall (?X ?Y) (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y)))) (forall ?X (= (* ?X 0) 0)) (forall (?X ?Y) (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X))) (forall ?X (= (+ 0 ?X) ?X)) (forall (?X ?Y) (= (* (succ ?X) ?Y) (succ (* ?X ?Y)))) (forall ?X (= 0 (* 0 ?X) ))
Conclusion:
(= (* (succ 0) (succ (succ 0))) (succ (succ 0)))