PALT02Ind

Premises:

(forall ?X (not (= 0 (succ ?X))))
(forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y)))
(forall ?X (= (+ ?X 0) ?X))
(forall (?X ?Y) (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y))))
(forall (?X ?Y) (<=> (= (+ ?X 0) ?Y) (= ?X ?Y)))
(forall (?X ?Y ?Z) (<=> (= (+ ?X (succ ?Y)) ?Z) (= (+ (+ ?X ?Y) (succ 0)) ?Z)))
(forall ?X (= (* ?X 0) 0))
(forall (?X ?Y) (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X)))
(forall (?X ?Y) (<=> (= (* ?X 0) ?Y) (= 0 ?Y)))
(forall (?X ?Y ?Z) (<=> (= (* ?X (succ ?Y)) ?Z) (= (+ (* ?X ?Y) ?X) ?Z)))
(forall (?X ?Y) (<=> (< ?X ?Y) (exists ?Z (and (not (= 0 ?Z)) (= (+ ?X ?Z) ?Y)))))
(forall (?X ?Y) (<=> (exists ?Z (= ?X (+ ?Y ?Z))) (=< ?Y ?X)))
(forall (?X ?Y) (<=> (=< ?X ?Y) (not (< ?Y ?X))))
(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ ?X) (* ?X ?Y))))
(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ (+ ?X ?Y)) (* ?X ?Y))))
(forall (?X ?Y) (=> (< 0 ?Y) (< (* ?X ?Y) (* (succ ?X) ?Y))))
(forall (?X ?Y) (=> (< 0 ?X) (< (* ?X ?Y) (* ?X (succ ?Y)))))
(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (< (succ (+ ?X ?Y)) (succ (* ?X ?Y)))))
(forall (?X ?Y ?Z) (=> (and (< (succ 0) ?Z) (< 0 ?X) (< 0 ?Y)) (< (* ?X ?Y) (* ?X (* ?Y ?Z)))))
(forall (?X ?Y) (<=> (< ?X (succ ?Y)) (or (= ?X ?Y) (< ?X ?Y))))
(forall (?X ?Y) (or (< ?X ?Y) (< ?Y ?X) (= ?X ?Y)))
(forall (?X ?Y) (<=> (< ?X ?Y) (and (not (= ?X ?Y)) (not (< ?Y ?X)))))
(forall (?X ?Y) (<=> (= ?X ?Y) (and (not (< ?X ?Y)) (not (< ?Y ?X)))))
(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))
(forall (?X ?Y) (=> (< ?X ?Y) (not (= ?X ?Y))))
(forall (?X ?Y) (=> (< (succ ?X) ?Y) (< ?X ?Y)))
(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))
(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))
(forall ?X (= (+ 0 ?X) ?X))
(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))
(forall ?X (= (* 0 ?X) 0))
(forall (?X ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?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 ?Y) (= (+ ?X ?Y) (+ ?Y ?X)))
(forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))
(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))

PALT02Ind

Premises:

Conclusion: