PA101a
Premises:
(forall ?X (= (+ ?X 0) ?X)) (forall (?X ?Y) (= (+ ?X (1+ ?Y)) (1+ (+ ?X ?Y)))) (forall ?X (= (* ?X 0) 0)) (forall (?X ?Y) (= (* ?X (1+ ?Y)) (+ (* ?X ?Y) ?X)))
Conclusion:
(= (* (1+ 0) (1+ 0)) (1+ 0))
Proof Trace