PrALT19
Premises:
(forall (?X ?Y) (<=> (exists ?Z (= ?X (+ ?Y ?Z))) (=< ?Y ?X))) (forall (?X ?Y ?Z ?W ?T) (=> (and (= (+ ?X ?Y) ?Z) (= (+ ?Z ?W) ?T)) (= (+ ?X (+ ?Y ?W)) ?T)))
Conclusion:
(forall (?Y ?X) (forall ?Z (=> (and (=< ?X ?Y) (=< ?Y ?Z)) (=< ?X ?Z))))