(BOOT-STRAP NQTHM) [ 0.1 0.1 0.0 ] GROUND-ZERO (COMPILE-UNCOMPILED-DEFNS "tmp") Loading ./basic/tmp.o Finished loading ./basic/tmp.o /v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp (ADD-SHELL ZN NIL ZNP ((POS (ONE-OF NUMBERP) ZERO) (NEG (ONE-OF NUMBERP) ZERO))) [ 0.1 0.0 0.0 ] ZN (DEFN ZLESSP (X Y) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) From the definition we can conclude that: (OR (FALSEP (ZLESSP X Y)) (TRUEP (ZLESSP X Y))) is a theorem. [ 0.0 0.0 0.0 ] ZLESSP (DEFN ZLESSEQP (X Y) (NOT (ZLESSP Y X))) Note that (OR (FALSEP (ZLESSEQP X Y)) (TRUEP (ZLESSEQP X Y))) is a theorem. [ 0.0 0.0 0.0 ] ZLESSEQP (DEFN ZMAX (X Y) (IF (ZLESSP X Y) Y X)) Note that (OR (EQUAL (ZMAX X Y) X) (EQUAL (ZMAX X Y) Y)) is a theorem. [ 0.0 0.0 0.0 ] ZMAX (DEFN ZMIN (X Y) (IF (ZLESSP X Y) X Y)) Note that (OR (EQUAL (ZMIN X Y) X) (EQUAL (ZMIN X Y) Y)) is a theorem. [ 0.0 0.0 0.0 ] ZMIN (DEFN ZSUB1 (X) (ZN (POS X) (ADD1 (NEG X)))) From the definition we can conclude that (ZNP (ZSUB1 X)) is a theorem. [ 0.0 0.0 0.0 ] ZSUB1 (DEFN PZDIFFERENCE (X Y) (DIFFERENCE (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) From the definition we can conclude that (NUMBERP (PZDIFFERENCE X Y)) is a theorem. [ 0.0 0.0 0.0 ] PZDIFFERENCE (DEFN M1 (X Y Z) (IF (ZLESSEQP X Y) 0 1)) WARNING: Z is in the arglist but not in the body of the definition of M1. Observe that (NUMBERP (M1 X Y Z)) is a theorem. [ 0.0 0.0 0.0 ] M1 (DEFN M2 (X Y Z) (PZDIFFERENCE (ZMAX X (ZMAX Y Z)) (ZMIN X (ZMIN Y Z)))) Note that (NUMBERP (M2 X Y Z)) is a theorem. [ 0.0 0.0 0.0 ] M2 (DEFN M3 (X Y Z) (PZDIFFERENCE X (ZMIN X (ZMIN Y Z)))) Note that (NUMBERP (M3 X Y Z)) is a theorem. [ 0.0 0.0 0.0 ] M3 (DEFN TAK0 (X Y Z) (IF (ZLESSEQP X Y) Y (IF (ZLESSEQP Y Z) Z X))) Observe that: (OR (EQUAL (TAK0 X Y Z) X) (EQUAL (TAK0 X Y Z) Y) (EQUAL (TAK0 X Y Z) Z)) is a theorem. [ 0.0 0.0 0.0 ] TAK0 (DEFN M (X Y Z) (CONS (M1 X Y Z) (CONS (M2 X Y Z) (CONS (M3 X Y Z) NIL)))) Note that (LISTP (M X Y Z)) is a theorem. [ 0.0 0.0 0.0 ] M (PROVE-LEMMA TAK0-SATISFIES-TAK-EQUATION NIL (EQUAL (TAK0 X Y Z) (IF (ZLESSEQP X Y) Y (TAK0 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y))))) This conjecture simplifies, rewriting with the lemmas POS-ZN and NEG-ZN, and unfolding the functions ZLESSEQP, ZLESSP, TAK0, and ZSUB1, to 24 new conjectures: Case 24.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z X (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 23.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) X (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 22.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y X (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 21.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y X (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 20.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 19.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 18.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 17.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 16.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z Z (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, rewriting with the lemmas SUB1-ADD1, NEG-ZN, and POS-ZN, and expanding the functions LESSP, PLUS, ZLESSEQP, ZLESSP, and TAK0, to the conjecture: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (NEG Z)) (PLUS (NEG Z) (POS Z))) (NOT (EQUAL (PLUS (POS Z) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS Z) (NEG Z))) (PLUS (NEG Z) (POS Z))))) (EQUAL Z (ZN (POS Z) (ADD1 (NEG Z))))). This again simplifies, using linear arithmetic, to: T. Case 15.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) Z (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 14.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y Z (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, using linear arithmetic, to: T. Case 13.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y Z (ZN (POS Z) (ADD1 (NEG Z)))))), which again simplifies, unfolding the definitions of ZLESSEQP, ZLESSP, and TAK0, to: T. Case 12.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z X X))), which again simplifies, using linear arithmetic, to: T. Case 11.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) X X))), which again simplifies, applying POS-ZN and NEG-ZN, and opening up the functions ZLESSEQP, ZLESSP, and TAK0, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (ADD1 (NEG X))) (PLUS (NEG X) (POS X))) (LESSP (PLUS (POS X) (NEG X)) (PLUS (NEG X) (POS X)))) (EQUAL X (ZN (POS X) (ADD1 (NEG X))))), which again simplifies, using linear arithmetic, to: T. Case 10.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y X X))), which again simplifies, unfolding the functions ZLESSEQP, ZLESSP, and TAK0, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (LESSP (PLUS (POS X) (NEG X)) (PLUS (NEG X) (POS X)))) (EQUAL X Y)). However this again simplifies, using linear arithmetic, to: T. Case 9. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y X X))), which again simplifies, using linear arithmetic, to: T. Case 8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z (ZN (POS Y) (ADD1 (NEG Y))) X))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) (ZN (POS Y) (ADD1 (NEG Y))) X))), which again simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y (ZN (POS Y) (ADD1 (NEG Y))) X))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y (ZN (POS Y) (ADD1 (NEG Y))) X))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Z Z X))), which again simplifies, expanding the functions ZLESSEQP, ZLESSP, and TAK0, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (NEG Z)) (PLUS (NEG Z) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (EQUAL Z X)). However this again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 (ZN (POS X) (ADD1 (NEG X))) Z X))), which again simplifies, applying POS-ZN and NEG-ZN, and unfolding ZLESSEQP, ZLESSP, and TAK0, to the following two new formulas: Case 3.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG X))) (PLUS (NEG Z) (POS X))))) (EQUAL X Z)). However this again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Z) (ADD1 (NEG X))) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (EQUAL X (ZN (POS X) (ADD1 (NEG X))))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (EQUAL X (TAK0 Y Z X))), which again simplifies, opening up the functions ZLESSEQP, ZLESSP, and TAK0, to the formula: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (EQUAL X Y)). But this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))))) (EQUAL Z (TAK0 Y Z X))), which again simplifies, unfolding ZLESSEQP, ZLESSP, and TAK0, to: T. Q.E.D. [ 0.0 0.0 0.1 ] TAK0-SATISFIES-TAK-EQUATION (PROVE-LEMMA M1-LESSEQP-0 (REWRITE) (IMPLIES (NOT (ZLESSEQP X Y)) (NOT (LESSP (M1 X Y Z) (M1 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y)))))) WARNING: Note that the linear lemma M1-LESSEQP-0 is being stored under the term (M1 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y)), which is unusual because M1 is a nonrecursive function symbol. WARNING: Note that the proposed lemma M1-LESSEQP-0 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZLESSEQP, NOT, and IMPLIES, to: (IMPLIES (ZLESSP Y X) (NOT (LESSP (M1 X Y Z) (M1 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y))))), which simplifies, applying POS-ZN and NEG-ZN, and unfolding the functions ZLESSP, ZLESSEQP, M1, ZSUB1, and TAK0, to the following 18 new formulas: Case 18.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (ZLESSP X Z))) (NOT (LESSP 1 0))). This again simplifies, using linear arithmetic, to: T. Case 17.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) Z))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 16.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (ZLESSP Z Z))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 15.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (ZLESSP X (ZN (POS X) (ADD1 (NEG X)))))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 14.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS X) (ADD1 (NEG X)))))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 13.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (ZLESSP Z (ZN (POS X) (ADD1 (NEG X)))))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 12.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (ZLESSP X Y))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 11.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) Y))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 10.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (ZLESSP Z Y))) (NOT (LESSP 1 0))), which again simplifies, using linear arithmetic, to: T. Case 9. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (ZLESSP X Z)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) Z)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (ZLESSP Z Z)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (ZLESSP X (ZN (POS X) (ADD1 (NEG X))))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) (ZN (POS X) (ADD1 (NEG X))))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (ZLESSP Z (ZN (POS X) (ADD1 (NEG X))))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (ZLESSP X Y)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (ZLESSP (ZN (POS Y) (ADD1 (NEG Y))) Y)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (ZLESSP Z Y)) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] M1-LESSEQP-0 (PROVE-LEMMA M1-LESSEQP-1 (REWRITE) (IMPLIES (NOT (ZLESSEQP X Y)) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 X) Y Z))))) WARNING: Note that the linear lemma M1-LESSEQP-1 is being stored under the term (M1 (ZSUB1 X) Y Z), which is unusual because M1 is a nonrecursive function symbol. WARNING: Note that the proposed lemma M1-LESSEQP-1 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZLESSEQP, NOT, and IMPLIES, to the new conjecture: (IMPLIES (ZLESSP Y X) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 X) Y Z)))), which simplifies, applying POS-ZN and NEG-ZN, and unfolding the functions ZLESSP, ZLESSEQP, M1, and ZSUB1, to the following two new goals: Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))))) (NOT (LESSP 1 0))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] M1-LESSEQP-1 (PROVE-LEMMA M1-LESSEQP-2 (REWRITE) (IMPLIES (NOT (ZLESSEQP X Y)) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 Y) Z X))))) WARNING: Note that the linear lemma M1-LESSEQP-2 is being stored under the term (M1 (ZSUB1 Y) Z X), which is unusual because M1 is a nonrecursive function symbol. WARNING: Note that the proposed lemma M1-LESSEQP-2 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZLESSEQP, NOT, and IMPLIES, to the new conjecture: (IMPLIES (ZLESSP Y X) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 Y) Z X)))), which simplifies, applying POS-ZN and NEG-ZN, and unfolding the functions ZLESSP, ZLESSEQP, M1, and ZSUB1, to the following two new goals: Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y))))) (NOT (LESSP 1 0))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] M1-LESSEQP-2 (PROVE-LEMMA M1-LESSEQP-3 (REWRITE) (IMPLIES (NOT (ZLESSEQP X Y)) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 Z) X Y))))) WARNING: Note that the linear lemma M1-LESSEQP-3 is being stored under the term (M1 (ZSUB1 Z) X Y), which is unusual because M1 is a nonrecursive function symbol. WARNING: Note that the proposed lemma M1-LESSEQP-3 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZLESSEQP, NOT, and IMPLIES, to the new conjecture: (IMPLIES (ZLESSP Y X) (NOT (LESSP (M1 X Y Z) (M1 (ZSUB1 Z) X Y)))), which simplifies, applying POS-ZN and NEG-ZN, and unfolding the functions ZLESSP, ZLESSEQP, M1, and ZSUB1, to the following two new goals: Case 2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z))))) (NOT (LESSP 1 0))). However this again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP 1 1))), which again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] M1-LESSEQP-3 (PROVE-LEMMA M2-LESSEQP-0 (REWRITE) (IMPLIES (NOT (ZLESSEQP X Y)) (NOT (LESSP (M2 X Y Z) (M2 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y)))))) WARNING: Note that the linear lemma M2-LESSEQP-0 is being stored under the term (M2 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y)), which is unusual because M2 is a nonrecursive function symbol. WARNING: Note that the proposed lemma M2-LESSEQP-0 is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZLESSEQP, NOT, and IMPLIES, to: (IMPLIES (ZLESSP Y X) (NOT (LESSP (M2 X Y Z) (M2 (TAK0 (ZSUB1 X) Y Z) (TAK0 (ZSUB1 Y) Z X) (TAK0 (ZSUB1 Z) X Y))))), which simplifies, applying POS-ZN and NEG-ZN, and unfolding the functions ZLESSP, ZMIN, ZMAX, M2, ZSUB1, ZLESSEQP, and TAK0, to the following 36 new formulas: Case 36.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Y) (ZMIN X Z)) (M2 Y Z X)))). This again simplifies, opening up ZLESSP, ZMAX, ZMIN, and M2, to eight new goals: Case 36.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 36.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 36.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 36.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 36.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, opening up the definitions of PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to the formula: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))))). But this again simplifies, using linear arithmetic, to: T. Case 36.3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 36.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 36.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 35.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Z) (ZMIN X Y)) (M2 Y Z X)))), which again simplifies, expanding the definitions of ZLESSP, ZMAX, ZMIN, and M2, to eight new formulas: Case 35.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X Y) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, expanding PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))))). This again simplifies, using linear arithmetic, to: T. Case 35.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z Y) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, unfolding the definitions of PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to the goal: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))))). However this again simplifies, using linear arithmetic, to: T. Case 35.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 35.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z X) (PZDIFFERENCE (ZMAX Y Z) (ZMIN Y X))))), which again simplifies, using linear arithmetic, to: T. Case 35.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X Y) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 35.3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z Y) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 35.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 35.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z X) (PZDIFFERENCE (ZMAX Y X) (ZMIN Y Z))))), which again simplifies, using linear arithmetic, to: T. Case 34.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Y) (ZMIN X Z)) (M2 (ZN (POS X) (ADD1 (NEG X))) Z X)))), which again simplifies, opening up the functions ZLESSP, ZMAX, ZMIN, and M2, to eight new conjectures: Case 34.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) Z) (ZMIN (ZN (POS X) (ADD1 (NEG X))) X))))), which again simplifies, using linear arithmetic, to: T. Case 34.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) Z) (ZMIN (ZN (POS X) (ADD1 (NEG X))) X))))), which again simplifies, using linear arithmetic, to: T. Case 34.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) Z) (ZMIN (ZN (POS X) (ADD1 (NEG X))) X))))), which again simplifies, using linear arithmetic, to: T. Case 34.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) Z) (ZMIN (ZN (POS X) (ADD1 (NEG X))) X))))), which again simplifies, using linear arithmetic, to: T. Case 34.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) X) (ZMIN (ZN (POS X) (ADD1 (NEG X))) Z))))), which again simplifies, applying POS-ZN, NEG-ZN, and SUB1-ADD1, and expanding the definitions of PZDIFFERENCE, ZLESSP, PLUS, LESSP, ZMAX, and ZMIN, to the following nine new goals: Case 34.4.9. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (EQUAL (PLUS (POS X) (NEG Z)) 0) (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X (ZN (POS X) (ADD1 (NEG X))))))). But this again simplifies, using linear arithmetic, to: T. Case 34.4.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (EQUAL (PLUS (POS X) (NEG Z)) 0) (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X)))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X (ZN (POS X) (ADD1 (NEG X))))))), which again simplifies, using linear arithmetic, to: T. Case 34.4.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z))) (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X (ZN (POS X) (ADD1 (NEG X))))))), which again simplifies, using linear arithmetic, to: T. Case 34.4.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z))) (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X)))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X (ZN (POS X) (ADD1 (NEG X))))))), which again simplifies, using linear arithmetic, to: T. Case 34.4.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z))) (NOT (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE (ZN (POS X) (ADD1 (NEG X))) (ZN (POS X) (ADD1 (NEG X))))))), which again simplifies, using linear arithmetic, to: T. Case 34.4.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (EQUAL (PLUS (POS X) (NEG Z)) 0) (NOT (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE (ZN (POS X) (ADD1 (NEG X))) (ZN (POS X) (ADD1 (NEG X))))))), which again simplifies, using linear arithmetic, to: T. Case 34.4.3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (EQUAL (PLUS (POS X) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X)))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X Z)))), which again simplifies, expanding the function PZDIFFERENCE, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (EQUAL (PLUS (POS X) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z)))) (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X)))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))))). But this again simplifies, using linear arithmetic, to: T. Case 34.4.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (EQUAL (PLUS (POS X) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z)))) (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE X Z)))), which again simplifies, unfolding the function PZDIFFERENCE, to the goal: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (EQUAL (PLUS (POS X) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z)))) (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))))). This again simplifies, using linear arithmetic, to: T. Case 34.4.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (EQUAL (PLUS (POS X) (NEG Z)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (EQUAL (PLUS (POS X) (NEG X)) 0)) (NOT (LESSP (SUB1 (PLUS (POS X) (NEG X))) (PLUS (NEG X) (POS X))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (PZDIFFERENCE (ZN (POS X) (ADD1 (NEG X))) Z)))), which again simplifies, using linear arithmetic, to: T. Case 34.3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) X) (ZMIN (ZN (POS X) (ADD1 (NEG X))) Z))))), which again simplifies, using linear arithmetic, to: T. Case 34.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) X) (ZMIN (ZN (POS X) (ADD1 (NEG X))) Z))))), which again simplifies, using linear arithmetic, to: T. Case 34.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX (ZN (POS X) (ADD1 (NEG X))) X) (ZMIN (ZN (POS X) (ADD1 (NEG X))) Z))))), which again simplifies, using linear arithmetic, to: T. Case 33.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Z) (ZMIN X Y)) (M2 (ZN (POS X) (ADD1 (NEG X))) Z X)))), which again simplifies, using linear arithmetic, to: T. Case 32.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Y) (ZMIN X Z)) (M2 Z Z X)))), which again simplifies, opening up the definitions of ZLESSP, ZMAX, ZMIN, and M2, to eight new goals: Case 32.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 32.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 32.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 32.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 32.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X Z) (PZDIFFERENCE (ZMAX Z X) (ZMIN Z Z))))), which again simplifies, unfolding PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to the goal: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (DIFFERENCE (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))))). This again simplifies, using linear arithmetic, to: T. Case 32.3. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y Z) (PZDIFFERENCE (ZMAX Z X) (ZMIN Z Z))))), which again simplifies, using linear arithmetic, to: T. Case 32.2. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Z X) (ZMIN Z Z))))), which again simplifies, using linear arithmetic, to: T. Case 32.1. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (NOT (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PZDIFFERENCE Y X) (PZDIFFERENCE (ZMAX Z X) (ZMIN Z Z))))), which again simplifies, using linear arithmetic, to: T. Case 31.(IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z)))) (NOT (LESSP (PZDIFFERENCE (ZMAX X Z) (ZMIN X Y)) (M2 Z Z X)))), which again simplifies, opening up the definitions of ZLESSP, ZMAX, ZMIN, and M2, to eight new formulas: Case 31.8. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X Y) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, unfolding PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (DIFFERENCE (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))))). However this again simplifies, using linear arithmetic, to: T. Case 31.7. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z Y) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, expanding the functions PZDIFFERENCE, ZLESSP, ZMAX, and ZMIN, to: (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (NOT (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y)))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (DIFFERENCE (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y))) (DIFFERENCE (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))))). But this again simplifies, using linear arithmetic, to: T. Case 31.6. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (NOT (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z))))) (NOT (LESSP (PZDIFFERENCE X X) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 31.5. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (ADD1 (NEG X))) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS Z) (NEG Y)) (PLUS (NEG Z) (POS Y)))) (LESSP (PLUS (POS Y) (NEG Z)) (PLUS (NEG Y) (POS Z))) (NOT (LESSP (PLUS (POS Z) (NEG X)) (PLUS (NEG Z) (POS X)))) (LESSP (PLUS (POS X) (NEG Y)) (PLUS (NEG X) (POS Y))) (LESSP (PLUS (POS X) (NEG Z)) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PZDIFFERENCE Z X) (PZDIFFERENCE (ZMAX Z Z) (ZMIN Z X))))), which again simplifies, using linear arithmetic, to: T. Case 31.4. (IMPLIES (AND (LESSP (PLUS (POS Y) (NEG X)) (PLUS (NEG Y) (POS X))) (NOT (LESSP (PLUS (POS X) (ADD1 (NEG Z))) (PLUS (NEG X) (POS Z)))) (NOT (LESSP (PLUS (POS Z) (ADD1 (NEG Y))) (PLUS (NEG Z) (POS Y)