CMMultInd
Premises:
(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 ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y))) (forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z)))) (forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y)))) (forall ?X (= (* 0 ?X) 0)) (forall ?X (= (succ ?X) (+ ?X (succ 0)))) (forall ?X (= (+ 0 ?X) ?X)) (forall (?X ?Y ?Z) (= (+ (+ ?X ?Y) ?Z) (+ ?X (+ ?Y ?Z)))) (forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X))) (forall ?X (= (* (succ 0) ?X) ?X))
Conclusion:
(forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))