PALT01Ind
Premises:
(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (+ ?X ?Y) (* ?X ?Y)))) (forall (?X ?Y) (=> (< ?X ?Y) (=< ?X ?Y))) (forall(?X ?Y) (=> (=< (succ ?X) ?Y) (=< ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (=< ?X ?Y) (=< ?Y ?Z)) (=< ?X ?Z))) (not (< 0 0)) (< 0 (succ 0)) (forall (?X ?Y) (=> (< ?X ?Y) (=< (succ ?X) ?Y))) (forall (?X ?Y)(=> (and (not (= ?X 0)) (not (= ?Y 0)))(=< (+ ?X ?Y) (* ?X ?Y)))) (forall (?X ?Y) (<=> (=< ?X ?Y) (=< (succ ?X) (succ ?Y))))
Conclusion:
(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (=< (+ ?X ?Y) (* ?X ?Y))))