(NOTE-LIB "fortran" T)
Loading ./basic/fortran.lib
Finished loading ./basic/fortran.lib
Loading ./basic/fortran.o
Finished loading ./basic/fortran.o
(#./basic/fortran.lib #./basic/fortran)
(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
(PROVE-LEMMA ZPLUS-COMM1
(REWRITE)
(EQUAL (ZPLUS X Y) (ZPLUS Y X)))
WARNING: Note that the rewrite rule ZPLUS-COMM1 will be stored so as to apply
only to terms with the nonrecursive function symbol ZPLUS.
This formula simplifies, rewriting with COMMUTATIVITY-OF-PLUS, and expanding
the function ZPLUS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZPLUS-COMM1
(PROVE-LEMMA ZPLUS-COMM2
(REWRITE)
(EQUAL (ZPLUS X (ZPLUS Y Z))
(ZPLUS Y (ZPLUS X Z))))
WARNING: Note that the rewrite rule ZPLUS-COMM2 will be stored so as to apply
only to terms with the nonrecursive function symbol ZPLUS.
WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever
the newly proposed ZPLUS-COMM2 could!
This simplifies, unfolding the definition of ZPLUS, to the following 18 new
goals:
Case 18.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(ZPLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))).
This again simplifies, opening up the definition of ZPLUS, to the goal:
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(PLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))).
This again simplifies, using linear arithmetic, to:
T.
Case 17.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(ZPLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, applying the lemma NEGATIVE-GUTS-MINUS, and opening
up the function ZPLUS, to two new goals:
Case 17.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(PLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 17.2.2.
(IMPLIES (AND (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(PLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(PLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))).
This again simplifies, using linear arithmetic, to:
T.
Case 17.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(PLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))).
This again simplifies, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y))
(EQUAL (ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(ZPLUS Y
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding
the definition of ZPLUS, to the following four new formulas:
Case 16.4.
(IMPLIES
(AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))
(EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE X (NEGATIVE-GUTS Z)))))).
However this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS
and MINUS-EQUAL, to the formula:
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE X (NEGATIVE-GUTS Z))))).
This again simplifies, using linear arithmetic, to two new conjectures:
Case 16.4.2.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y)
(DIFFERENCE X (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE X (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.3.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(NOT (LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))
(EQUAL (DIFFERENCE X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))
(DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(NOT (LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))
(EQUAL (DIFFERENCE X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))
(DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 16.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y))))
(NOT (LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(NOT (LESSP X (NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))),
which again simplifies, applying the lemma NEGATIVE-GUTS-MINUS, and opening
up the function ZPLUS, to two new formulas:
Case 15.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to two new goals:
Case 15.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.2.1.
(IMPLIES (AND (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 15.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(NOT (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(NOT (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))).
This again simplifies, using linear arithmetic, to:
T.
Case 14.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding
ZPLUS, to the following four new conjectures:
Case 14.4.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))
(MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y)))).
This again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to:
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))),
which again simplifies, using linear arithmetic, to four new formulas:
Case 14.4.4.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))).
This again simplifies, using linear arithmetic, to:
T.
Case 14.4.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.4.2.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(LESSP (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))).
This again simplifies, using linear arithmetic, to:
T.
Case 14.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) X)
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.3.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to three new conjectures:
Case 14.3.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.3.2.
(IMPLIES (AND (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 14.3.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 14.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS Z) X)))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))).
But this again simplifies, using linear arithmetic, to:
T.
Case 13.(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(EQUAL (ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) X))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and opening up ZPLUS,
to the following two new goals:
Case 13.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))
(MINUS (PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS Z) X))))).
This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL,
to:
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 13.2.2.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) X)
(NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS Z) X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NEGATIVEP Z)
(LESSP X (NEGATIVE-GUTS Z))
(NEGATIVEP Y))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 12.(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NOT (NEGATIVEP Y)))
(EQUAL (ZPLUS X (PLUS Y Z))
(ZPLUS Y (PLUS X Z)))),
which again simplifies, appealing to the lemma COMMUTATIVITY2-OF-PLUS, and
unfolding the function ZPLUS, to:
T.
Case 11.(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(ZPLUS Y (PLUS X Z)))),
which again simplifies, unfolding the definition of ZPLUS, to two new
formulas:
Case 11.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(DIFFERENCE (PLUS X Z)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(DIFFERENCE (PLUS X Z)
(NEGATIVE-GUTS Y)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 11.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(NOT (LESSP (PLUS X Z)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(ZPLUS Y (PLUS X Z)))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up
the definition of ZPLUS, to the following four new formulas:
Case 10.4.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
(PLUS X Z))))).
But this again simplifies, rewriting with the lemmas NEGATIVE-GUTS-MINUS
and MINUS-EQUAL, to the formula:
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(PLUS X Z)))).
This again simplifies, using linear arithmetic, to three new goals:
Case 10.4.3.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(PLUS X Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(PLUS X Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) (PLUS X Z))
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(DIFFERENCE (NEGATIVE-GUTS Y)
(PLUS X Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.3.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (PLUS X Z)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 10.3.2.
(IMPLIES (AND (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (PLUS X Z)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.3.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))
(EQUAL (DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (PLUS X Z)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.2.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (LESSP (PLUS X Z) (NEGATIVE-GUTS Y))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 10.1.
(IMPLIES (AND (NOT (NEGATIVEP X))
(NOT (NEGATIVEP Z))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y))
(LESSP (PLUS X Z) (NEGATIVE-GUTS Y)))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 9. (IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z))))
(EQUAL (ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(ZPLUS Y
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding ZPLUS,
to the following four new formulas:
Case 9.4.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))
(MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y)))).
However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to the new formula:
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 9.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.4.1.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y)
(NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.3.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 9.2.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.1.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))),
which again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(ZPLUS Y
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding ZPLUS,
to the following two new conjectures:
Case 8.2.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (MINUS (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y)))).
But this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 8.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 8.2.1.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y)
(NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z))
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 8.1.
(IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NOT (NEGATIVEP Y))
(LESSP Y (NEGATIVE-GUTS Z)))
(LESSP Y
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NEGATIVEP X)
(NEGATIVEP Z)
(NEGATIVEP Y))
(EQUAL (ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(ZPLUS Y
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Z)))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS and
COMMUTATIVITY2-OF-PLUS, and opening up the definition of ZPLUS, to:
T.
Case 6. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y)))
(EQUAL (ZPLUS X (PLUS Y Z))
(ZPLUS Y
(DIFFERENCE Z (NEGATIVE-GUTS X))))).
However this again simplifies, opening up the function ZPLUS, to two new
conjectures:
Case 6.2.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y)))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(PLUS Y
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y)))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(PLUS Y
(DIFFERENCE Z (NEGATIVE-GUTS X))))).
This again simplifies, using linear arithmetic, to:
T.
Case 6.1.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y)))
(NOT (LESSP (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(ZPLUS Y
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, expanding ZPLUS, to four new conjectures:
Case 5.4.
(IMPLIES
(AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y))))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X)))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to
the new goal:
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 5.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X)))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.3.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))
(DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))
(DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 5.2.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y))))
(NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.1.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(ZPLUS Y
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up
the function ZPLUS, to the following two new conjectures:
Case 4.2.
(IMPLIES
(AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (MINUS (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X)))))).
However this again simplifies, applying NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 4.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X)))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(DIFFERENCE (NEGATIVE-GUTS Y)
(DIFFERENCE Z (NEGATIVE-GUTS X))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS X)))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y)))
(EQUAL (ZPLUS X (PLUS Y Z))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and unfolding
the function ZPLUS, to the following four new conjectures:
Case 3.4.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z)))
(MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y)))).
However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))),
which again simplifies, using linear arithmetic, to three new conjectures:
Case 3.4.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (PLUS Y Z))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(LESSP (NEGATIVE-GUTS X) (PLUS Y Z))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))).
But this again simplifies, using linear arithmetic, to:
T.
Case 3.4.2.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(LESSP (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))).
But this again simplifies, using linear arithmetic, to:
T.
Case 3.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Z)
Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.3.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to two new goals:
Case 3.3.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.3.1.
(IMPLIES (AND (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X))
(DIFFERENCE Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3.2.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z))))
(NOT (LESSP (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(LESSP Y
(DIFFERENCE (NEGATIVE-GUTS X) Z)))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and unfolding
the function ZPLUS, to the following two new formulas:
Case 2.2.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y))))
(MINUS (PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z))))).
But this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))).
But this again simplifies, using linear arithmetic, to two new conjectures:
Case 2.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (LESSP Z (NEGATIVE-GUTS Y))))
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(ZPLUS Y
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Z))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, and
expanding the function ZPLUS, to:
(IMPLIES (AND (NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Z)
(NEGATIVEP X)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS X))
(NEGATIVEP Y)
(LESSP Z (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(PLUS (NEGATIVE-GUTS Y)
(DIFFERENCE (NEGATIVE-GUTS X) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.1 ]
ZPLUS-COMM2
(PROVE-LEMMA ZPLUS-ASSOC
(REWRITE)
(EQUAL (ZPLUS (ZPLUS X Y) Z)
(ZPLUS X (ZPLUS Y Z))))
WARNING: Note that the rewrite rule ZPLUS-ASSOC will be stored so as to apply
only to terms with the nonrecursive function symbol ZPLUS.
WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever
the newly proposed ZPLUS-ASSOC could!
This simplifies, rewriting with ZPLUS-COMM1, and expanding ZPLUS, to 18 new
formulas:
Case 18.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP X)))
(EQUAL (ZPLUS Z (PLUS X Y))
(ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, opening up the definition of ZPLUS, to two new
conjectures:
Case 18.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP X)))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP X)))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(PLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 18.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP X)))
(NOT (LESSP (PLUS X Y)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (ZPLUS Z
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, unfolding the function ZPLUS, to four new
conjectures:
Case 17.4.
(IMPLIES
(AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X))))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to
the new conjecture:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 17.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.3.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))
(DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))
(DIFFERENCE (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 17.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))))
(NOT (LESSP (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 17.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y)))
(ZPLUS X
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and expanding
the function ZPLUS, to the following two new goals:
Case 16.2.
(IMPLIES
(AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (MINUS (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y)))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))))).
However this again simplifies, applying NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to two new goals:
Case 16.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z)))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Y (NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(NOT (LESSP Y (NEGATIVE-GUTS Z)))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS Z))
(NEGATIVE-GUTS X))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X)))
(EQUAL (ZPLUS Z (PLUS X Y))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding the
function ZPLUS, to the following four new goals:
Case 15.4.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y)))
(MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)))).
But this again simplifies, appealing to the lemmas NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))).
However this again simplifies, using linear arithmetic, to three new goals:
Case 15.4.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) (PLUS X Y))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(LESSP (NEGATIVE-GUTS Z) (PLUS X Y))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))).
This again simplifies, using linear arithmetic, to:
T.
Case 15.4.2.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(LESSP (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))).
This again simplifies, using linear arithmetic, to:
T.
Case 15.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(PLUS X Y))
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Z) Y)
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.3.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 15.3.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.3.1.
(IMPLIES (AND (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(NOT (LESSP (PLUS X Y) (NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (PLUS X Y)
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 15.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))
(NOT (LESSP (PLUS X Y)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(LESSP (PLUS X Y) (NEGATIVE-GUTS Z))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NOT (NEGATIVEP X))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))
(LESSP (PLUS X Y) (NEGATIVE-GUTS Z))).
This again simplifies, using linear arithmetic, to:
T.
Case 14.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (ZPLUS Z
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))),
which again simplifies, rewriting with the lemma NEGATIVE-GUTS-MINUS, and
unfolding the function ZPLUS, to two new formulas:
Case 14.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X))))
(MINUS (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL,
to:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to two new goals:
Case 14.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 14.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(LESSP (DIFFERENCE Y (NEGATIVE-GUTS X))
(NEGATIVE-GUTS Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y)))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Z) Y))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, and
opening up ZPLUS, to:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 13.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z) Y)
(NOT (NEGATIVEP Y))
(NEGATIVEP Z)
(LESSP Y (NEGATIVE-GUTS Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Z) Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 12.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NOT (NEGATIVEP X)))
(EQUAL (ZPLUS Z (PLUS X Y))
(ZPLUS X (PLUS Y Z)))),
which again simplifies, applying COMMUTATIVITY2-OF-PLUS and
COMMUTATIVITY-OF-PLUS, and opening up ZPLUS, to:
T.
Case 11.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (ZPLUS Z
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(ZPLUS X (PLUS Y Z)))).
But this again simplifies, expanding ZPLUS, to two new formulas:
Case 11.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (PLUS Z
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(EQUAL (PLUS Z
(DIFFERENCE Y (NEGATIVE-GUTS X)))
(DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 11.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(NOT (LESSP Y (NEGATIVE-GUTS X))))
(NOT (LESSP (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS X) Y)))
(ZPLUS X (PLUS Y Z)))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and opening up the
function ZPLUS, to the following four new formulas:
Case 10.4.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z))))).
This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL,
to:
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z)))),
which again simplifies, using linear arithmetic, to three new conjectures:
Case 10.4.3.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z)
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y)
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) (PLUS Y Z))
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS X) Y)
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(PLUS Y Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.3.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 10.3.2.
(IMPLIES (AND (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.3.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y)
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))
(DIFFERENCE (PLUS Y Z)
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to:
T.
Case 10.2.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y)))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X) Y)
(NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(NOT (LESSP (PLUS Y Z) (NEGATIVE-GUTS X))))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 10.1.
(IMPLIES (AND (NOT (NEGATIVEP Y))
(NOT (NEGATIVEP Z))
(NEGATIVEP X)
(LESSP Y (NEGATIVE-GUTS X))
(LESSP (PLUS Y Z) (NEGATIVE-GUTS X)))
(LESSP Z
(DIFFERENCE (NEGATIVE-GUTS X) Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 9. (IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up
the definition of ZPLUS, to the following four new conjectures:
Case 9.4.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(EQUAL (MINUS (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE X (NEGATIVE-GUTS Y))))
(MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)))).
This again simplifies, applying NEGATIVE-GUTS-MINUS and MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to two new goals:
Case 9.4.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Z)
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.4.1.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (NEGATIVE-GUTS Z)
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.3.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))
(NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z))))
(EQUAL (DIFFERENCE (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z))
(DIFFERENCE X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 9.2.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(NOT (LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))
(NOT (LESSP (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 9.1.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))))
(LESSP (DIFFERENCE X (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS Z))),
which again simplifies, using linear arithmetic, to:
T.
Case 8. (IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X)))
(ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS, and opening up
ZPLUS, to the following two new formulas:
Case 8.2.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (MINUS (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS Y) X)))
(MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)))).
However this again simplifies, rewriting with NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to two new formulas:
Case 8.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 8.2.1.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X)
(NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (PLUS (NEGATIVE-GUTS Z)
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z))
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 8.1.
(IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(LESSP X
(PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NEGATIVEP Y)
(NEGATIVEP Z)
(NEGATIVEP X))
(EQUAL (ZPLUS Z
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))))
(ZPLUS X
(MINUS (PLUS (NEGATIVE-GUTS Y)
(NEGATIVE-GUTS Z)))))),
which again simplifies, appealing to the lemmas COMMUTATIVITY2-OF-PLUS,
COMMUTATIVITY-OF-PLUS, and NEGATIVE-GUTS-MINUS, and unfolding ZPLUS, to:
T.
Case 6. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, opening up ZPLUS, to:
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (PLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X)))
(ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, appealing to the lemma NEGATIVE-GUTS-MINUS, and
unfolding the definition of ZPLUS, to two new conjectures:
Case 5.2.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to two new goals:
Case 5.2.2.
(IMPLIES (AND (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))).
This again simplifies, using linear arithmetic, to:
T.
Case 5.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(PLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to:
T.
Case 5.1.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X)))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X))
(EQUAL (ZPLUS Z
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))))
(ZPLUS X
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and expanding the
definition of ZPLUS, to the following four new formulas:
Case 4.4.
(IMPLIES
(AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))
(EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z))
(MINUS (DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))))).
This again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL,
to:
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to two new goals:
Case 4.4.2.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y)))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(DIFFERENCE (NEGATIVE-GUTS X)
(DIFFERENCE Z (NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.3.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (LESSP Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))))
(EQUAL (DIFFERENCE Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (LESSP Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))))
(EQUAL (DIFFERENCE Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))
(DIFFERENCE (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 4.2.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(NOT (LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X))))
(NOT (LESSP Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(NOT (LESSP Z (NEGATIVE-GUTS Y)))
(NEGATIVEP X)
(LESSP (DIFFERENCE Z (NEGATIVE-GUTS Y))
(NEGATIVE-GUTS X)))
(LESSP Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (ZPLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))))),
which again simplifies, applying NEGATIVE-GUTS-MINUS, and opening up the
definition of ZPLUS, to the following two new formulas:
Case 3.2.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (PLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
However this again simplifies, using linear arithmetic, to two new
conjectures:
Case 3.2.2.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (PLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.2.1.
(IMPLIES (AND (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (PLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(EQUAL (PLUS Z
(DIFFERENCE X (NEGATIVE-GUTS Y)))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(NOT (LESSP X (NEGATIVE-GUTS Y))))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y)))
(EQUAL (ZPLUS Z
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) X)))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))))),
which again simplifies, applying the lemma NEGATIVE-GUTS-MINUS, and
unfolding ZPLUS, to four new goals:
Case 2.4.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z))
(MINUS (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)))),
which again simplifies, rewriting with NEGATIVE-GUTS-MINUS and MINUS-EQUAL,
to:
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))),
which again simplifies, using linear arithmetic, to four new formulas:
Case 2.4.4.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(LESSP (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.4.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.4.2.
(IMPLIES (AND (LESSP (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(LESSP (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2.4.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(EQUAL (DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) X)
Z)
(DIFFERENCE (DIFFERENCE (NEGATIVE-GUTS Y) Z)
X))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.3.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to three new goals:
Case 2.3.3.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.3.2.
(IMPLIES (AND (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2.3.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))))
(EQUAL (DIFFERENCE Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))
(DIFFERENCE X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X)))),
which again simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) X)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(NOT (LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))
(NOT (LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X)))).
This again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NOT (NEGATIVEP X))
(LESSP X (NEGATIVE-GUTS Y))
(LESSP X
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))
(LESSP Z
(DIFFERENCE (NEGATIVE-GUTS Y) X))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(EQUAL (ZPLUS Z
(MINUS (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))))
(ZPLUS X
(MINUS (DIFFERENCE (NEGATIVE-GUTS Y) Z))))),
which again simplifies, rewriting with the lemma NEGATIVE-GUTS-MINUS, and
opening up the function ZPLUS, to two new conjectures:
Case 1.2.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(EQUAL (MINUS (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z))
(MINUS (PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z))))),
which again simplifies, applying the lemmas NEGATIVE-GUTS-MINUS and
MINUS-EQUAL, to:
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))).
But this again simplifies, using linear arithmetic, to two new conjectures:
Case 1.2.2.
(IMPLIES (AND (LESSP (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.2.1.
(IMPLIES (AND (LESSP (NEGATIVE-GUTS Y) Z)
(NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(EQUAL (DIFFERENCE (PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y))
Z)
(PLUS (NEGATIVE-GUTS X)
(DIFFERENCE (NEGATIVE-GUTS Y) Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NEGATIVEP Y)
(NOT (NEGATIVEP Z))
(LESSP Z (NEGATIVE-GUTS Y))
(NEGATIVEP X))
(LESSP Z
(PLUS (NEGATIVE-GUTS X)
(NEGATIVE-GUTS Y)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.1 ]
ZPLUS-ASSOC
(DISABLE ZPLUS)
[ 0.0 0.0 0.0 ]
ZPLUS-OFF
(ADD-SHELL VEHICLE-STATE NIL VEHICLE-STATEP
((W (NONE-OF) ZERO)
(Y (NONE-OF) ZERO)
(V (NONE-OF) ZERO)))
[ 0.0 0.0 0.0 ]
VEHICLE-STATE
(DEFN HD (X) (CAR X))
[ 0.0 0.0 0.0 ]
HD
(DEFN TL (X) (CDR X))
[ 0.0 0.0 0.0 ]
TL
(DEFN EMPTY (X) (NOT (LISTP X)))
From the definition we can conclude that:
(OR (FALSEP (EMPTY X))
(TRUEP (EMPTY X)))
is a theorem.
[ 0.0 0.0 0.0 ]
EMPTY
(PROVE-LEMMA TL-REWRITE
(REWRITE)
(EQUAL (TL X) (CDR X)))
WARNING: Note that the rewrite rule TL-REWRITE will be stored so as to apply
only to terms with the nonrecursive function symbol TL.
This formula can be simplified, using the abbreviation TL, to:
(EQUAL (CDR X) (CDR X)),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TL-REWRITE
(DISABLE TL)
[ 0.0 0.0 0.0 ]
TL-OFF
(PROVE-LEMMA DOWN-ON-TL
(REWRITE)
(IMPLIES (NOT (EMPTY X))
(LESSP (COUNT (TL X)) (COUNT X))))
WARNING: Note that the proposed lemma DOWN-ON-TL is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
This conjecture can be simplified, using the abbreviations EMPTY, NOT, IMPLIES,
and TL-REWRITE, to:
(IMPLIES (LISTP X)
(LESSP (COUNT (CDR X)) (COUNT X))).
This simplifies, using linear arithmetic and applying CDR-LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DOWN-ON-TL
(DEFN RANDOM-DELTA-WS
(LST)
(IF (EMPTY LST)
T
(AND (OR (EQUAL (HD LST) -1)
(EQUAL (HD LST) 0)
(EQUAL (HD LST) 1))
(RANDOM-DELTA-WS (TL LST)))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT LST) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
RANDOM-DELTA-WS is accepted under the principle of definition. Note that:
(OR (FALSEP (RANDOM-DELTA-WS LST))
(TRUEP (RANDOM-DELTA-WS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
RANDOM-DELTA-WS
(DEFN CONTROLLER
(SGN-Y SGN-OLD-Y)
(ZPLUS (ZTIMES -3 SGN-Y)
(ZTIMES 2 SGN-OLD-Y)))
Note that:
(OR (NUMBERP (CONTROLLER SGN-Y SGN-OLD-Y))
(NEGATIVEP (CONTROLLER SGN-Y SGN-OLD-Y)))
is a theorem.
[ 0.0 0.0 0.0 ]
CONTROLLER
(DISABLE CONTROLLER)
[ 0.0 0.0 0.0 ]
CONTROLLER-OFF
(DEFN SGN
(X)
(IF (NEGATIVEP X)
(IF (EQUAL (NEGATIVE-GUTS X) 0) 0 -1)
(IF (ZEROP X) 0 1)))
Note that (OR (NUMBERP (SGN X)) (NEGATIVEP (SGN X))) is a theorem.
[ 0.0 0.0 0.0 ]
SGN
(DISABLE SGN)
[ 0.0 0.0 0.0 ]
SGN-OFF
(DEFN NEXT-STATE
(DELTA-W STATE)
(VEHICLE-STATE
(ZPLUS (W STATE) DELTA-W)
(ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE) DELTA-W)))
(ZPLUS (V STATE)
(CONTROLLER (SGN (ZPLUS (Y STATE)
(ZPLUS (V STATE)
(ZPLUS (W STATE) DELTA-W))))
(SGN (Y STATE))))))
From the definition we can conclude that:
(VEHICLE-STATEP (NEXT-STATE DELTA-W STATE))
is a theorem.
[ 0.0 0.0 0.0 ]
NEXT-STATE
(DEFN FINAL-STATE-OF-VEHICLE
(DELTA-WS STATE)
(IF (EMPTY DELTA-WS)
STATE
(FINAL-STATE-OF-VEHICLE (TL DELTA-WS)
(NEXT-STATE (HD DELTA-WS) STATE))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT DELTA-WS) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
FINAL-STATE-OF-VEHICLE is accepted under the definitional principle. From the
definition we can conclude that:
(OR (VEHICLE-STATEP (FINAL-STATE-OF-VEHICLE DELTA-WS STATE))
(EQUAL (FINAL-STATE-OF-VEHICLE DELTA-WS STATE)
STATE))
is a theorem.
[ 0.0 0.0 0.0 ]
FINAL-STATE-OF-VEHICLE
(DEFN GOOD-STATEP
(STATE)
(IF (EQUAL (Y STATE) 0)
(OR (EQUAL (ZPLUS (V STATE) (W STATE)) -1)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 1))
(IF (EQUAL (Y STATE) 1)
(OR (EQUAL (ZPLUS (V STATE) (W STATE)) -2)
(EQUAL (ZPLUS (V STATE) (W STATE))
-3))
(IF (EQUAL (Y STATE) 2)
(OR (EQUAL (ZPLUS (V STATE) (W STATE)) -1)
(EQUAL (ZPLUS (V STATE) (W STATE))
-2))
(IF (EQUAL (Y STATE) 3)
(EQUAL (ZPLUS (V STATE) (W STATE)) -1)
(IF (EQUAL (Y STATE) -3)
(EQUAL (ZPLUS (V STATE) (W STATE)) 1)
(IF (EQUAL (Y STATE) -2)
(OR (EQUAL (ZPLUS (V STATE) (W STATE)) 1)
(EQUAL (ZPLUS (V STATE) (W STATE)) 2))
(IF (EQUAL (Y STATE) -1)
(OR (EQUAL (ZPLUS (V STATE) (W STATE)) 2)
(EQUAL (ZPLUS (V STATE) (W STATE)) 3))
F))))))))
Note that (OR (FALSEP (GOOD-STATEP STATE)) (TRUEP (GOOD-STATEP STATE)))
is a theorem.
[ 0.0 0.0 0.0 ]
GOOD-STATEP
(PROVE-LEMMA NEXT-GOOD-STATE
(REWRITE)
(IMPLIES (AND (GOOD-STATEP STATE)
(OR (EQUAL R -1)
(EQUAL R 0)
(EQUAL R 1)))
(GOOD-STATEP (NEXT-STATE R STATE))))
WARNING: Note that the rewrite rule NEXT-GOOD-STATE will be stored so as to
apply only to terms with the nonrecursive function symbol GOOD-STATEP.
This formula simplifies, rewriting with ZPLUS-COMM2, ZPLUS-COMM1, ZPLUS-ASSOC,
W-VEHICLE-STATE, V-VEHICLE-STATE, and Y-VEHICLE-STATE, and opening up the
functions GOOD-STATEP, OR, CONTROLLER, SGN, ZPLUS, NEXT-STATE, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
NEXT-GOOD-STATE
(DEFN ZERO-DELTA-WS
(LST)
(IF (EMPTY LST)
T
(AND (EQUAL (HD LST) 0)
(ZERO-DELTA-WS (TL LST)))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT LST) decreases according
to the well-founded relation LESSP in each recursive call. Hence,
ZERO-DELTA-WS is accepted under the principle of definition. Note that:
(OR (FALSEP (ZERO-DELTA-WS LST))
(TRUEP (ZERO-DELTA-WS LST)))
is a theorem.
[ 0.0 0.0 0.0 ]
ZERO-DELTA-WS
(DEFN CONCAT
(X Y)
(IF (EMPTY X)
Y
(CONS (HD X) (CONCAT (TL X) Y))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call. Hence, CONCAT is
accepted under the definitional principle. From the definition we can
conclude that (OR (LISTP (CONCAT X Y)) (EQUAL (CONCAT X Y) Y)) is a theorem.
[ 0.0 0.0 0.0 ]
CONCAT
(DEFN LENGTH
(X)
(IF (EMPTY X)
0
(ADD1 (LENGTH (TL X)))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT X) decreases according
to the well-founded relation LESSP in each recursive call. Hence, LENGTH is
accepted under the principle of definition. From the definition we can
conclude that (NUMBERP (LENGTH X)) is a theorem.
[ 0.0 0.0 0.0 ]
LENGTH
(PROVE-LEMMA LENGTH-0
(REWRITE)
(EQUAL (EQUAL (LENGTH X) 0)
(EMPTY X)))
This formula simplifies, opening up the definition of EMPTY, to two new
conjectures:
Case 2. (IMPLIES (NOT (EQUAL (LENGTH X) 0))
(LISTP X)),
which again simplifies, unfolding the definitions of EMPTY, LENGTH, and
EQUAL, to:
T.
Case 1. (IMPLIES (EQUAL (LENGTH X) 0)
(NOT (LISTP X))),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY X) (p X))
(IMPLIES (AND (NOT (EMPTY X)) (p (TL X)))
(p X))).
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the definition of
EMPTY can be used to prove that the measure (COUNT X) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme produces three new formulas:
Case 3. (IMPLIES (AND (EMPTY X) (EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, opening up EMPTY, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY X))
(NOT (EQUAL (LENGTH (TL X)) 0))
(EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, opening up EMPTY and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (EMPTY X))
(NOT (LISTP (TL X)))
(EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, applying TL-REWRITE, and expanding the functions EMPTY and
LENGTH, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-0
(PROVE-LEMMA DECOMPOSE-LIST-OF-LENGTH-4
(REWRITE)
(IMPLIES (ZERO-DELTA-WS LST)
(EQUAL (LESSP (LENGTH LST) 4)
(NOT (EQUAL LST
(CONCAT '(0 0 0 0) (CDDDDR LST)))))))
This formula simplifies, appealing to the lemmas TL-REWRITE, CDR-NLISTP, and
EQUAL-LESSP, and expanding the definitions of HD, EMPTY, ZERO-DELTA-WS, LENGTH,
LESSP, CDR, CONCAT, NOT, EQUAL, ADD1, and TL, to the following 28 new formulas:
Case 28.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (LESSP 1 4)))
(EQUAL LST '(0 0 0 0 . 0))).
But this again simplifies, using linear arithmetic, to:
T.
Case 27.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(LESSP 1 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, expanding the functions CAR, EQUAL, CDR, and LISTP,
to:
T.
Case 26.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(NOT (LESSP 2 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 25.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(LESSP 2 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, opening up CAR, EQUAL, CDR, and LISTP, to:
T.
Case 24.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(NOT (LISTP LST))
(NOT (LESSP 0 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 23.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(NOT (LISTP (CDDR LST)))
(NOT (LISTP LST))
(LESSP 0 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, obviously, to:
T.
Case 22.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (LESSP 1 4)))
(EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST))))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 21.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(LESSP 1 4))
(NOT (EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST)))))))),
which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
expanding the functions EQUAL, CAR, CDR, ZERO-DELTA-WS, LESSP, and CONS, to:
(IMPLIES (AND (EQUAL (CAR LST) 0)
(NOT (LISTP (CDR LST))))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, expanding CAR, EQUAL, CDR, and LISTP, to:
T.
Case 20.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(NOT (LISTP (CDDDR LST)))
(NOT (LESSP 3 4)))
(EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 19.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(NOT (LISTP (CDDDR LST)))
(LESSP 3 4))
(NOT (EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST)))))))),
which again simplifies, applying CAR-NLISTP and CDR-NLISTP, and opening up
EQUAL, ZERO-DELTA-WS, LESSP, and CONS, to:
(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(NOT (LISTP (CDDDR LST))))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, unfolding the functions CAR, EQUAL, CDR, and LISTP,
to:
T.
Case 18.(IMPLIES
(AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(LISTP (CDDDR LST))
(NOT (LESSP (ADD1 (ADD1 (ADD1 (ADD1 (LENGTH (CDDDDR LST))))))
4)))
(EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST))))))),
which again simplifies, rewriting with the lemmas SUB1-ADD1, CAR-CONS, and
CDR-CONS, and unfolding the definitions of SUB1, NUMBERP, EQUAL, and LESSP,
to:
T.
Case 17.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(LISTP (CDDDR LST))
(LESSP (ADD1 (ADD1 (ADD1 (ADD1 (LENGTH (CDDDDR LST))))))
4))
(NOT (EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST)))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 16.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(NOT (LISTP (CDDR LST)))
(NOT (LESSP 2 4)))
(EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 15.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(LISTP LST)
(LISTP (CDR LST))
(NOT (LISTP (CDDR LST)))
(LESSP 2 4))
(NOT (EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST)))))))),
which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
opening up the functions EQUAL, CAR, CDR, ZERO-DELTA-WS, LESSP, and CONS, to:
(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(LISTP (CDR LST))
(NOT (LISTP (CDDR LST))))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, unfolding CAR, EQUAL, CDR, and LISTP, to:
T.
Case 14.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(NOT (LISTP LST))
(NOT (LESSP 0 4)))
(EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(EQUAL (CADDDR LST) 0)
(ZERO-DELTA-WS (CDDDDR LST))
(NOT (LISTP LST))
(LESSP 0 4))
(NOT (EQUAL LST
(CONS 0
(CONS 0
(CONS 0 (CONS 0 (CDDDDR LST)))))))),
which again simplifies, obviously, to:
T.
Case 12.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (LESSP 1 4)))
(EQUAL LST '(0 0 0 0 . 0))).
But this again simplifies, using linear arithmetic, to:
T.
Case 11.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(NOT (LISTP (CDR LST)))
(LESSP 1 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, expanding the functions CAR, EQUAL, CDR, and LISTP,
to:
T.
Case 10.(IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(NOT (LESSP 3 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 9. (IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(LISTP (CDDR LST))
(LESSP 3 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, unfolding the functions CAR, EQUAL, CDR, and LISTP,
to:
T.
Case 8. (IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(NOT (LISTP (CDDR LST)))
(NOT (LESSP 2 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(LISTP LST)
(LISTP (CDR LST))
(NOT (LISTP (CDDR LST)))
(LESSP 2 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, opening up CAR, EQUAL, CDR, and LISTP, to:
T.
Case 6. (IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(NOT (LISTP LST))
(NOT (LESSP 0 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (EQUAL (CAR LST) 0)
(EQUAL (CADR LST) 0)
(EQUAL (CADDR LST) 0)
(NOT (LISTP (CDDDR LST)))
(NOT (LISTP LST))
(LESSP 0 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, trivially, to:
T.
Case 4. (IMPLIES (AND (EQUAL (CAR LST) 0)
(NOT (LISTP (CDR LST)))
(LISTP LST)
(NOT (LESSP 1 4)))
(EQUAL LST '(0 0 0 0 . 0))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (EQUAL (CAR LST) 0)
(NOT (LISTP (CDR LST)))
(LISTP LST)
(LESSP 1 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, opening up CAR, EQUAL, CDR, and LISTP, to:
T.
Case 2. (IMPLIES (AND (EQUAL (CAR LST) 0)
(NOT (LISTP (CDR LST)))
(NOT (LISTP LST))
(NOT (LESSP 0 4)))
(EQUAL LST '(0 0 0 0 . 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (CAR LST) 0)
(NOT (LISTP (CDR LST)))
(NOT (LISTP LST))
(LESSP 0 4))
(NOT (EQUAL LST '(0 0 0 0 . 0)))),
which again simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
DECOMPOSE-LIST-OF-LENGTH-4
(PROVE-LEMMA DRIFT-TO-0-IN-4
(REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(EQUAL (Y (FINAL-STATE-OF-VEHICLE '(0 0 0 0)
STATE))
0)))
This simplifies, rewriting with ZPLUS-COMM1, ZPLUS-COMM2, W-VEHICLE-STATE,
ZPLUS-ASSOC, Y-VEHICLE-STATE, and V-VEHICLE-STATE, and opening up GOOD-STATEP,
NEXT-STATE, ZPLUS, SGN, CONTROLLER, HD, TL, EMPTY, FINAL-STATE-OF-VEHICLE, and
EQUAL, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
DRIFT-TO-0-IN-4
(PROVE-LEMMA CANCEL-WIND-IN-4
(REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE '(0 0 0 0)
STATE))
(W (FINAL-STATE-OF-VEHICLE '(0 0 0 0)
STATE)))
0)))
WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever
the newly proposed CANCEL-WIND-IN-4 could!
This simplifies, rewriting with ZPLUS-COMM1, ZPLUS-COMM2, W-VEHICLE-STATE,
ZPLUS-ASSOC, Y-VEHICLE-STATE, and V-VEHICLE-STATE, and expanding the functions
GOOD-STATEP, NEXT-STATE, ZPLUS, SGN, CONTROLLER, HD, TL, EMPTY,
FINAL-STATE-OF-VEHICLE, and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.2 0.0 ]
CANCEL-WIND-IN-4
(PROVE-LEMMA ONCE-0-ALWAYS-0
(REWRITE)
(IMPLIES (AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(AND (EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0))))
WARNING: the previously added lemma, ZPLUS-COMM1, could be applied whenever
the newly proposed ONCE-0-ALWAYS-0 could!
WARNING: Note that the proposed lemma ONCE-0-ALWAYS-0 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and two replacement rules.
This conjecture simplifies, rewriting with ZPLUS-COMM1, and opening up AND, to
two new formulas:
Case 2. (IMPLIES (AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
Applying the lemma W-Y-V-ELIM, replace STATE by (VEHICLE-STATE V X Z) to
eliminate (Y STATE), (V STATE), and (W STATE). We thus obtain the following
two new formulas:
Case 2.2.
(IMPLIES (AND (NOT (VEHICLE-STATEP STATE))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
But this further simplifies, appealing to the lemmas Y-NVEHICLE-STATEP,
V-NVEHICLE-STATEP, and W-NVEHICLE-STATEP, and unfolding the definitions of
EQUAL and ZPLUS, to the conjecture:
(IMPLIES (AND (NOT (VEHICLE-STATEP STATE))
(ZERO-DELTA-WS LST))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)),
which we would usually push and work on later by induction. But if we
must use induction to prove the input conjecture, we prefer to induct on
the original formulation of the problem. Thus we will disregard all that
we have previously done, give the name *1 to the original input, and work
on it.
So now let us consider:
(AND (IMPLIES (AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0))
(IMPLIES (AND (ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0))),
which we named *1 above. We will appeal to induction. The recursive terms in
the conjecture suggest five inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (EMPTY LST) (p LST STATE))
(IMPLIES (AND (NOT (EMPTY LST))
(p (TL LST)
(NEXT-STATE (HD LST) STATE)))
(p LST STATE))).
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the definition of
EMPTY inform us that the measure (COUNT LST) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for STATE. The above induction scheme
produces the following ten new conjectures:
Case 10.(IMPLIES (AND (EMPTY LST)
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
This simplifies, appealing to the lemma ZPLUS-COMM1, and opening up EMPTY,
ZERO-DELTA-WS, FINAL-STATE-OF-VEHICLE, and EQUAL, to:
T.
Case 9. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (ZERO-DELTA-WS (TL LST)))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
This simplifies, opening up the functions EMPTY, ZERO-DELTA-WS, and HD, to:
T.
Case 8. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (EQUAL (Y (NEXT-STATE (HD LST) STATE))
0))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
This simplifies, applying ZPLUS-COMM2, ZPLUS-COMM1, and Y-VEHICLE-STATE, and
expanding EMPTY, HD, SGN, NEXT-STATE, ZERO-DELTA-WS, and
FINAL-STATE-OF-VEHICLE, to:
(IMPLIES
(AND (LISTP LST)
(NOT (EQUAL (ZPLUS 0
(ZPLUS (CAR LST)
(ZPLUS (V STATE) (W STATE))))
0))
(EQUAL (CAR LST) 0)
(ZERO-DELTA-WS (TL LST))
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
0)).
However this again simplifies, unfolding the functions ZPLUS and EQUAL, to:
T.
Case 7. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (EQUAL (ZPLUS (W (NEXT-STATE (HD LST) STATE))
(V (NEXT-STATE (HD LST) STATE)))
0))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)),
which simplifies, rewriting with the lemmas ZPLUS-COMM2, ZPLUS-COMM1,
W-VEHICLE-STATE, V-VEHICLE-STATE, and ZPLUS-ASSOC, and unfolding the
functions EMPTY, HD, SGN, NEXT-STATE, ZERO-DELTA-WS, and
FINAL-STATE-OF-VEHICLE, to:
(IMPLIES
(AND
(LISTP LST)
(NOT
(EQUAL
(ZPLUS
(CAR LST)
(ZPLUS
(V STATE)
(ZPLUS
(W STATE)
(CONTROLLER (SGN (ZPLUS 0
(ZPLUS (CAR LST)
(ZPLUS (V STATE) (W STATE)))))
0))))
0))
(EQUAL (CAR LST) 0)
(ZERO-DELTA-WS (TL LST))
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
0)).
However this again simplifies, applying ZPLUS-COMM1 and ZPLUS-COMM2, and
unfolding ZPLUS, SGN, CONTROLLER, and EQUAL, to:
T.
Case 6. (IMPLIES
(AND
(NOT (EMPTY LST))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
0)
(EQUAL
(ZPLUS (V (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
(W (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE))))
0)
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST STATE))
0)).
This simplifies, applying ZPLUS-COMM1, and expanding the functions EMPTY,
ZERO-DELTA-WS, HD, FINAL-STATE-OF-VEHICLE, and EQUAL, to:
T.
Case 5. (IMPLIES (AND (EMPTY LST)
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0)),
which simplifies, rewriting with the lemma ZPLUS-COMM1, and expanding EMPTY,
ZERO-DELTA-WS, FINAL-STATE-OF-VEHICLE, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (ZERO-DELTA-WS (TL LST)))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0)),
which simplifies, opening up the definitions of EMPTY, ZERO-DELTA-WS, and HD,
to:
T.
Case 3. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (EQUAL (Y (NEXT-STATE (HD LST) STATE))
0))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0)),
which simplifies, rewriting with the lemmas ZPLUS-COMM2, ZPLUS-COMM1, and
Y-VEHICLE-STATE, and expanding EMPTY, HD, SGN, NEXT-STATE, ZERO-DELTA-WS,
and FINAL-STATE-OF-VEHICLE, to the conjecture:
(IMPLIES
(AND (LISTP LST)
(NOT (EQUAL (ZPLUS 0
(ZPLUS (CAR LST)
(ZPLUS (V STATE) (W STATE))))
0))
(EQUAL (CAR LST) 0)
(ZERO-DELTA-WS (TL LST))
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL
(ZPLUS (V (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
(W (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE))))
0)).
This again simplifies, expanding the functions ZPLUS and EQUAL, to:
T.
Case 2. (IMPLIES (AND (NOT (EMPTY LST))
(NOT (EQUAL (ZPLUS (W (NEXT-STATE (HD LST) STATE))
(V (NEXT-STATE (HD LST) STATE)))
0))
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0)),
which simplifies, rewriting with ZPLUS-COMM2, ZPLUS-COMM1, W-VEHICLE-STATE,
V-VEHICLE-STATE, and ZPLUS-ASSOC, and opening up the definitions of EMPTY,
HD, SGN, NEXT-STATE, ZERO-DELTA-WS, and FINAL-STATE-OF-VEHICLE, to:
(IMPLIES
(AND
(LISTP LST)
(NOT
(EQUAL
(ZPLUS
(CAR LST)
(ZPLUS
(V STATE)
(ZPLUS
(W STATE)
(CONTROLLER (SGN (ZPLUS 0
(ZPLUS (CAR LST)
(ZPLUS (V STATE) (W STATE)))))
0))))
0))
(EQUAL (CAR LST) 0)
(ZERO-DELTA-WS (TL LST))
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (V STATE) (W STATE)) 0))
(EQUAL
(ZPLUS (V (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
(W (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE))))
0)),
which again simplifies, rewriting with the lemmas ZPLUS-COMM1 and
ZPLUS-COMM2, and opening up the definitions of ZPLUS, SGN, CONTROLLER, and
EQUAL, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EMPTY LST))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
0)
(EQUAL
(ZPLUS (V (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE)))
(W (FINAL-STATE-OF-VEHICLE (TL LST)
(NEXT-STATE (HD LST) STATE))))
0)
(ZERO-DELTA-WS LST)
(EQUAL (Y STATE) 0)
(EQUAL (ZPLUS (W STATE) (V STATE)) 0))
(EQUAL (ZPLUS (V (FINAL-STATE-OF-VEHICLE LST STATE))
(W (FINAL-STATE-OF-VEHICLE LST STATE)))
0)),
which simplifies, rewriting with ZPLUS-COMM1, and unfolding EMPTY,
ZERO-DELTA-WS, HD, FINAL-STATE-OF-VEHICLE, and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
ONCE-0-ALWAYS-0
(PROVE-LEMMA FINAL-STATE-OF-VEHICLE-CONCAT
(REWRITE)
(EQUAL (FINAL-STATE-OF-VEHICLE (CONCAT A B)
STATE)
(FINAL-STATE-OF-VEHICLE B
(FINAL-STATE-OF-VEHICLE A STATE))))
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (EMPTY A) (p A B STATE))
(IMPLIES (AND (NOT (EMPTY A))
(p (TL A)
B
(NEXT-STATE (HD A) STATE)))
(p A B STATE))).
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the definition of
EMPTY can be used to prove that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for STATE. The above induction scheme
leads to two new goals:
Case 2. (IMPLIES
(EMPTY A)
(EQUAL (FINAL-STATE-OF-VEHICLE (CONCAT A B)
STATE)
(FINAL-STATE-OF-VEHICLE B
(FINAL-STATE-OF-VEHICLE A STATE)))),
which simplifies, opening up the definitions of EMPTY, CONCAT, and
FINAL-STATE-OF-VEHICLE, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EMPTY A))
(EQUAL
(FINAL-STATE-OF-VEHICLE (CONCAT (TL A) B)
(NEXT-STATE (HD A) STATE))
(FINAL-STATE-OF-VEHICLE B
(FINAL-STATE-OF-VEHICLE (TL A)
(NEXT-STATE (HD A) STATE)))))
(EQUAL (FINAL-STATE-OF-VEHICLE (CONCAT A B)
STATE)
(FINAL-STATE-OF-VEHICLE B
(FINAL-STATE-OF-VEHICLE A STATE)))),
which simplifies, applying ZPLUS-COMM2, ZPLUS-COMM1, CAR-CONS, TL-REWRITE,
and CDR-CONS, and unfolding EMPTY, HD, NEXT-STATE, CONCAT, and
FINAL-STATE-OF-VEHICLE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FINAL-STATE-OF-VEHICLE-CONCAT
(PROVE-LEMMA ZERO-DELTA-WS-CONCAT
(REWRITE)
(EQUAL (ZERO-DELTA-WS (CONCAT '(0 0 0 0) V))
(ZERO-DELTA-WS V)))
This conjecture simplifies, rewriting with TL-REWRITE, CDR-CONS, and CAR-CONS,
and unfolding TL, HD, EMPTY, CONCAT, EQUAL, and ZERO-DELTA-WS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZERO-DELTA-WS-CONCAT
(DISABLE CONCAT)
[ 0.0 0.0 0.0 ]
CONCAT-OFF
(DISABLE NEXT-STATE)
[ 0.0 0.0 0.0 ]
NEXT-STATE-OFF
(PROVE-LEMMA GOOD-STATEP-BOUNDED-ABOVE
(REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP 3 (Y STATE)))))
WARNING: Note that the rewrite rule GOOD-STATEP-BOUNDED-ABOVE will be stored
so as to apply only to terms with the nonrecursive function symbol ZLESSP.
This formula simplifies, expanding the functions GOOD-STATEP and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-STATEP-BOUNDED-ABOVE
(PROVE-LEMMA GOOD-STATEP-BOUNDED-BELOW
(REWRITE)
(IMPLIES (GOOD-STATEP STATE)
(NOT (ZLESSP (Y STATE) -3))))
WARNING: Note that the rewrite rule GOOD-STATEP-BOUNDED-BELOW will be stored
so as to apply only to terms with the nonrecursive function symbol ZLESSP.
This formula simplifies, expanding the functions GOOD-STATEP and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-STATEP-BOUNDED-BELOW
(DISABLE GOOD-STATEP)
[ 0.0 0.0 0.0 ]
GOOD-STATEP-OFF
(PROVE-LEMMA ZLESSP-IS-LESSP
(REWRITE)
(IMPLIES (AND (NUMBERP X) (NUMBERP Y))
(EQUAL (ZLESSP X Y) (LESSP X Y))))
WARNING: Note that the rewrite rule ZLESSP-IS-LESSP will be stored so as to
apply only to terms with the nonrecursive function symbol ZLESSP.
This conjecture simplifies, expanding the definition of ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZLESSP-IS-LESSP
(DISABLE ZLESSP)
[ 0.0 0.0 0.0 ]
ZLESSP-OFF
(DEFN FSV
(D S)
(IF (EMPTY D)
S
(FSV (TL D) (NEXT-STATE (HD D) S))))
Linear arithmetic, the lemmas TL-REWRITE and CDR-LESSP, and the
definition of EMPTY inform us that the measure (COUNT D) decreases according
to the well-founded relation LESSP in each recursive call. Hence, FSV is
accepted under the definitional principle. From the definition we can
conclude that (OR (VEHICLE-STATEP (FSV D S)) (EQUAL (FSV D S) S)) is a theorem.
[ 0.0 0.0 0.0 ]
FSV
(PROVE-LEMMA ALL-GOOD-STATES
(REWRITE)
(IMPLIES (AND (RANDOM-DELTA-WS LST)
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE)))
((INDUCT (FSV LST STATE))))
This formula can be simplified, using the abbreviations IMPLIES, EMPTY, NOT,
OR, AND, HD, and TL-REWRITE, to the following two new conjectures:
Case 2. (IMPLIES (AND (NOT (LISTP LST))
(RANDOM-DELTA-WS LST)
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))).
This simplifies, opening up EMPTY, RANDOM-DELTA-WS, and
FINAL-STATE-OF-VEHICLE, to:
T.
Case 1. (IMPLIES
(AND
(LISTP LST)
(IMPLIES
(AND (RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP (NEXT-STATE (CAR LST) STATE)))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE (CAR LST) STATE))))
(RANDOM-DELTA-WS LST)
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))).
This simplifies, rewriting with TL-REWRITE, and unfolding the definitions of
AND, IMPLIES, HD, EMPTY, and RANDOM-DELTA-WS, to six new goals:
Case 1.6.
(IMPLIES (AND (LISTP LST)
(NOT (GOOD-STATEP (NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) 0)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, rewriting with NEXT-GOOD-STATE, and opening up the
definitions of OR and EQUAL, to:
T.
Case 1.5.
(IMPLIES (AND (LISTP LST)
(NOT (GOOD-STATEP (NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) -1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))).
But this again simplifies, appealing to the lemma NEXT-GOOD-STATE, and
unfolding OR and EQUAL, to:
T.
Case 1.4.
(IMPLIES (AND (LISTP LST)
(NOT (GOOD-STATEP (NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) 1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, rewriting with the lemma NEXT-GOOD-STATE, and
unfolding OR and EQUAL, to:
T.
Case 1.3.
(IMPLIES
(AND
(LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) 0)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, clearly, to the new formula:
(IMPLIES
(AND (LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE 0 STATE)))
(EQUAL (CAR LST) 0)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, rewriting with TL-REWRITE, and opening up the
functions HD, EMPTY, and FINAL-STATE-OF-VEHICLE, to:
T.
Case 1.2.
(IMPLIES
(AND
(LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) -1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))).
This again simplifies, obviously, to:
(IMPLIES
(AND (LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE -1 STATE)))
(EQUAL (CAR LST) -1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, rewriting with TL-REWRITE, and expanding the
functions HD, EMPTY, and FINAL-STATE-OF-VEHICLE, to:
T.
Case 1.1.
(IMPLIES
(AND
(LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE (CAR LST) STATE)))
(EQUAL (CAR LST) 1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))).
This again simplifies, clearly, to:
(IMPLIES
(AND (LISTP LST)
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE (CDR LST)
(NEXT-STATE 1 STATE)))
(EQUAL (CAR LST) 1)
(RANDOM-DELTA-WS (CDR LST))
(GOOD-STATEP STATE))
(GOOD-STATEP (FINAL-STATE-OF-VEHICLE LST STATE))),
which again simplifies, applying the lemma TL-REWRITE, and unfolding HD,
EMPTY, and FINAL-STATE-OF-VEHICLE, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
ALL-GOOD-STATES
(PROVE-LEMMA VEHICLE-STAYS-WITHIN-3-OF-COURSE NIL
(IMPLIES (AND (RANDOM-DELTA-WS LST)
(EQUAL STATE
(FINAL-STATE-OF-VEHICLE LST
(VEHICLE-STATE 0 0 0))))
(AND (ZLESSEQP -3 (Y STATE))
(ZLESSEQP (Y STATE) 3))))
This conjecture simplifies, appealing to the lemmas GOOD-STATEP-BOUNDED-BELOW,
ALL-GOOD-STATES, and GOOD-STATEP-BOUNDED-ABOVE, and expanding GOOD-STATEP,
ZLESSEQP, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
VEHICLE-STAYS-WITHIN-3-OF-COURSE
(DISABLE FINAL-STATE-OF-VEHICLE)
[ 0.0 0.0 0.0 ]
FINAL-STATE-OF-VEHICLE-OFF
(PROVE-LEMMA ZERO-DELTA-WS-CDDDDR
(REWRITE)
(IMPLIES (ZERO-DELTA-WS X)
(ZERO-DELTA-WS (CDDDDR X))))
This simplifies, rewriting with TL-REWRITE and CDR-NLISTP, and expanding HD,
EMPTY, ZERO-DELTA-WS, and CDR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZERO-DELTA-WS-CDDDDR
(PROVE-LEMMA GOOD-STATES-FIND-AND-STAY-AT-0
(REWRITE)
(IMPLIES (AND (GOOD-STATEP STATE)
(ZERO-DELTA-WS LST2)
(NOT (LESSP (LENGTH LST2) 4)))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST2 STATE))
0)))
This simplifies, applying DECOMPOSE-LIST-OF-LENGTH-4, to:
(IMPLIES (AND (GOOD-STATEP STATE)
(ZERO-DELTA-WS LST2)
(EQUAL LST2
(CONCAT '(0 0 0 0) (CDDDDR LST2))))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST2 STATE))
0)).
Applying the lemma CAR-CDR-ELIM, replace LST2 by (CONS Z X) to eliminate
(CDR LST2) and (CAR LST2), X by (CONS W V) to eliminate (CDR X) and (CAR X), V
by (CONS D X) to eliminate (CDR V) and (CAR V), and X by (CONS C V) to
eliminate (CDR X) and (CAR X). We would thus like to prove the following five
new formulas:
Case 5. (IMPLIES (AND (NOT (LISTP LST2))
(GOOD-STATEP STATE)
(ZERO-DELTA-WS LST2)
(EQUAL LST2
(CONCAT '(0 0 0 0) (CDDDDR LST2))))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE LST2 STATE))
0)).
However this further simplifies, applying CDR-NLISTP, and opening up the
definitions of EMPTY, ZERO-DELTA-WS, CDR, and CONCAT, to:
T.
Case 4. (IMPLIES (AND (NOT (LISTP X))
(GOOD-STATEP STATE)
(ZERO-DELTA-WS (CONS Z X))
(EQUAL (CONS Z X)
(CONCAT '(0 0 0 0) (CDDDR X))))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (CONS Z X)
STATE))
0)).
This further simplifies, rewriting with the lemmas ZERO-DELTA-WS-CONCAT,
CDR-NLISTP, CAR-CONS, and CONS-EQUAL, and expanding the functions CDR,
CONCAT, and CAR, to:
T.
Case 3. (IMPLIES (AND (NOT (LISTP V))
(GOOD-STATEP STATE)
(ZERO-DELTA-WS (CONS Z (CONS W V)))
(EQUAL (CONS Z (CONS W V))
(CONCAT '(0 0 0 0) (CDDR V))))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (CONS Z (CONS W V))
STATE))
0)),
which further simplifies, applying the lemmas ZERO-DELTA-WS-CONCAT,
CDR-NLISTP, CAR-CONS, and CONS-EQUAL, and expanding the functions CDR,
CONCAT, and CAR, to:
T.
Case 2. (IMPLIES (AND (NOT (LISTP X))
(GOOD-STATEP STATE)
(ZERO-DELTA-WS (CONS Z (CONS W (CONS D X))))
(EQUAL (CONS Z (CONS W (CONS D X)))
(CONCAT '(0 0 0 0) (CDR X))))
(EQUAL (Y (FINAL-STATE-OF-VEHICLE (CONS Z (CONS W (CONS D X)))
STATE))
0)),
which further simplifies, appealing to the lemmas ZERO-DELTA-WS-CONCAT,
CDR-NLISTP, CAR-CONS, and CONS-EQUAL, and opening up CONCAT and CAR, to:
T.
Case 1. (IMPLIES
(AND (GOOD-STATEP STATE)
(ZERO-DELTA-WS (CONS Z (CONS W (CONS D (CONS C V)))))
(EQUAL (CONS Z (CONS W (CONS D (CONS C V))))
(CONCAT '(0 0 0 0) V)))
(EQUAL
(Y (FINAL-STATE-OF-VEHICLE (CONS Z (CONS W (CONS D (CONS C V))))
STATE))
0)),
which further simplifies, rewriting with ZERO-DELTA-WS-CONCAT,
FINAL-STATE-OF-VEHICLE-CONCAT, ZPLUS-COMM1, CANCEL-WIND-IN-4,
DRIFT-TO-0-IN-4, and ONCE-0-ALWAYS-0, and unfolding EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GOOD-STATES-FIND-AND-STAY-AT-0
(PROVE-LEMMA VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND NIL
(IMPLIES (AND (RANDOM-DELTA-WS LST1)
(ZERO-DELTA-WS LST2)
(ZGREATEREQP (LENGTH LST2) 4)
(EQUAL STATE
(FINAL-STATE-OF-VEHICLE (CONCAT LST1 LST2)
(VEHICLE-STATE 0 0 0))))
(EQUAL (Y STATE) 0))
NIL)
This conjecture can be simplified, using the abbreviations ZGREATEREQP, AND,
IMPLIES, and FINAL-STATE-OF-VEHICLE-CONCAT, to:
(IMPLIES
(AND
(RANDOM-DELTA-WS LST1)
(ZERO-DELTA-WS LST2)
(NOT (ZLESSP (LENGTH LST2) 4))
(EQUAL STATE
(FINAL-STATE-OF-VEHICLE LST2
(FINAL-STATE-OF-VEHICLE LST1
(VEHICLE-STATE 0 0 0)))))
(EQUAL (Y STATE) 0)).
This simplifies, rewriting with DECOMPOSE-LIST-OF-LENGTH-4, ZLESSP-IS-LESSP,
ALL-GOOD-STATES, and GOOD-STATES-FIND-AND-STAY-AT-0, and opening up the
functions GOOD-STATEP and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
VEHICLE-GETS-ON-COURSE-IN-STEADY-WIND