(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./basic/tmp.o
Finished loading ./basic/tmp.o
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp
(DEFN RT
(X)
(IF (ZEROP X)
0
(IF (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(ADD1 (RT (SUB1 X)))
(RT (SUB1 X)))))
Linear arithmetic, the lemmas COUNT-NUMBERP and SUB1-ADD1, and the
definitions of ZEROP, TIMES, and PLUS can be used to show that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, RT is accepted under the definitional principle. From
the definition we can conclude that (NUMBERP (RT X)) is a theorem.
[ 0.0 0.0 0.0 ]
RT
(PROVE-LEMMA TIMES-ADD1
(REWRITE)
(EQUAL (TIMES X (ADD1 Y))
(PLUS X (TIMES X Y))))
Give the conjecture the name *1.
We will try to prove it by induction. There are three plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X Y))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y))
(p X Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
generates two new goals:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (TIMES X (ADD1 Y))
(PLUS X (TIMES X Y)))),
which simplifies, expanding ZEROP, EQUAL, TIMES, PLUS, and NUMBERP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (SUB1 X) (ADD1 Y))
(PLUS (SUB1 X) (TIMES (SUB1 X) Y))))
(EQUAL (TIMES X (ADD1 Y))
(PLUS X (TIMES X Y)))),
which simplifies, appealing to the lemma SUB1-ADD1, and unfolding the
definitions of ZEROP, TIMES, and PLUS, to two new conjectures:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (TIMES (SUB1 X) (ADD1 Y))
(PLUS (SUB1 X) (TIMES (SUB1 X) Y)))
(NOT (NUMBERP Y)))
(EQUAL (ADD1 (PLUS 0 (TIMES (SUB1 X) (ADD1 Y))))
(PLUS X Y (TIMES (SUB1 X) Y)))),
which again simplifies, opening up EQUAL and PLUS, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (TIMES (SUB1 X) (ADD1 Y))
(PLUS (SUB1 X) (TIMES (SUB1 X) Y)))
(NUMBERP Y))
(EQUAL (ADD1 (PLUS Y (TIMES (SUB1 X) (ADD1 Y))))
(PLUS X Y (TIMES (SUB1 X) Y)))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-ADD1
(PROVE-LEMMA PLUS-ADD1
(REWRITE)
(EQUAL (PLUS X (ADD1 Y))
(ADD1 (PLUS X Y))))
This conjecture simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PLUS-ADD1
(PROVE-LEMMA SQUARE-0
(REWRITE)
(EQUAL (EQUAL (TIMES X X) 0)
(ZEROP X)))
This conjecture simplifies, expanding ZEROP, to the following three new goals:
Case 3. (IMPLIES (NOT (EQUAL (TIMES X X) 0))
(NUMBERP X)).
However this again simplifies, expanding the definitions of TIMES and EQUAL,
to:
T.
Case 2. (IMPLIES (NOT (EQUAL (TIMES X X) 0))
(NOT (EQUAL X 0))),
which again simplifies, expanding the definitions of TIMES and EQUAL, to:
T.
Case 1. (IMPLIES (AND (EQUAL (TIMES X X) 0)
(NOT (EQUAL X 0)))
(NOT (NUMBERP 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 (ZEROP X) (p X))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X)))
(p X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us 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 the following three new goals:
Case 3. (IMPLIES (AND (ZEROP X)
(EQUAL (TIMES X X) 0)
(NOT (EQUAL X 0)))
(NOT (NUMBERP X))).
This simplifies, expanding the function ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL (TIMES (SUB1 X) (SUB1 X)) 0))
(EQUAL (TIMES X X) 0)
(NOT (EQUAL X 0)))
(NOT (NUMBERP X))).
This simplifies, opening up ZEROP and TIMES, to the new formula:
(IMPLIES (AND (NOT (EQUAL (TIMES (SUB1 X) (SUB1 X)) 0))
(EQUAL (PLUS X (TIMES (SUB1 X) X)) 0)
(NOT (EQUAL X 0)))
(NOT (NUMBERP X))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (SUB1 X) 0)
(EQUAL (TIMES X X) 0)
(NOT (EQUAL X 0)))
(NOT (NUMBERP X))),
which simplifies, expanding the functions ZEROP, TIMES, EQUAL, ADD1, and
PLUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SQUARE-0
(PROVE-LEMMA SQUARE-MONOTONIC NIL
(IMPLIES (NOT (LESSP B A))
(NOT (LESSP (TIMES B B) (TIMES A A)))))
Name the conjecture *1.
Perhaps we can prove it by induction. Four inductions are suggested by
terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL A 0) (NOT (NUMBERP A)))
(p B A))
(IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(OR (EQUAL B 0) (NOT (NUMBERP B))))
(p B A))
(IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(p (SUB1 B) (SUB1 A)))
(p B A))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT B) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for A. The above induction scheme
leads to the following four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL A 0) (NOT (NUMBERP A)))
(NOT (LESSP B A)))
(NOT (LESSP (TIMES B B) (TIMES A A)))).
This simplifies, opening up NOT, OR, EQUAL, LESSP, and TIMES, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(OR (EQUAL B 0) (NOT (NUMBERP B)))
(NOT (LESSP B A)))
(NOT (LESSP (TIMES B B) (TIMES A A)))).
This simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(LESSP (SUB1 B) (SUB1 A))
(NOT (LESSP B A)))
(NOT (LESSP (TIMES B B) (TIMES A A)))).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP A 1)
(NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(LESSP (SUB1 B) (SUB1 A))
(NOT (LESSP B A)))
(NOT (LESSP (TIMES B B) (TIMES A A)))),
which again simplifies, unfolding the definitions of SUB1, NUMBERP, EQUAL,
LESSP, NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(NOT (LESSP (TIMES (SUB1 B) (SUB1 B))
(TIMES (SUB1 A) (SUB1 A))))
(NOT (LESSP B A)))
(NOT (LESSP (TIMES B B) (TIMES A A)))),
which simplifies, expanding NOT, OR, LESSP, and TIMES, to:
(IMPLIES (AND (NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL B 0))
(NUMBERP B)
(NOT (LESSP (TIMES (SUB1 B) (SUB1 B))
(TIMES (SUB1 A) (SUB1 A))))
(NOT (LESSP (SUB1 B) (SUB1 A))))
(NOT (LESSP (PLUS B (TIMES (SUB1 B) B))
(PLUS A (TIMES (SUB1 A) A))))).
Appealing to the lemma SUB1-ELIM, we now replace B by (ADD1 X) to eliminate
(SUB1 B). We use the type restriction lemma noted when SUB1 was introduced
to constrain the new variable. We must thus prove the goal:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (EQUAL (ADD1 X) 0))
(NOT (LESSP (TIMES X X)
(TIMES (SUB1 A) (SUB1 A))))
(NOT (LESSP X (SUB1 A))))
(NOT (LESSP (PLUS (ADD1 X) (TIMES X (ADD1 X)))
(PLUS A (TIMES (SUB1 A) A))))).
However this further simplifies, appealing to the lemmas TIMES-ADD1 and
SUB1-ADD1, and expanding PLUS and LESSP, to:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL A 0))
(NUMBERP A)
(NOT (LESSP (TIMES X X)
(TIMES (SUB1 A) (SUB1 A))))
(NOT (LESSP X (SUB1 A)))
(NOT (EQUAL (PLUS A (TIMES (SUB1 A) A))
0)))
(NOT (LESSP (PLUS X X (TIMES X X))
(SUB1 (PLUS A (TIMES (SUB1 A) A)))))).
Appealing to the lemma SUB1-ELIM, we now replace A by (ADD1 Z) to eliminate
(SUB1 A). We employ the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. We must thus prove:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(NOT (EQUAL (ADD1 Z) 0))
(NOT (LESSP (TIMES X X) (TIMES Z Z)))
(NOT (LESSP X Z))
(NOT (EQUAL (PLUS (ADD1 Z) (TIMES Z (ADD1 Z)))
0)))
(NOT (LESSP (PLUS X X (TIMES X X))
(SUB1 (PLUS (ADD1 Z)
(TIMES Z (ADD1 Z))))))).
However this further simplifies, rewriting with the lemmas TIMES-ADD1 and
SUB1-ADD1, and expanding the definition of PLUS, to:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(NOT (LESSP (TIMES X X) (TIMES Z Z)))
(NOT (LESSP X Z)))
(NOT (LESSP (PLUS X X (TIMES X X))
(PLUS Z Z (TIMES Z Z))))).
But this finally simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SQUARE-MONOTONIC
(PROVE-LEMMA SPEC-FOR-RT NIL
(AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP Y
(ADD1 (PLUS (RT Y)
(PLUS (RT Y)
(TIMES (RT Y) (RT Y))))))))
This formula can be simplified, using the abbreviations NOT and AND, to the
following two new goals:
Case 2. (NOT (LESSP Y (TIMES (RT Y) (RT Y)))).
Name the above subgoal *1.
Case 1. (LESSP Y
(ADD1 (PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))).
This simplifies, appealing to the lemma SUB1-ADD1, and unfolding LESSP, to:
(IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))).
Applying the lemma SUB1-ELIM, replace Y by (ADD1 X) to eliminate (SUB1 Y).
We rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove the new formula:
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (ADD1 X) 0)))
(LESSP X
(PLUS (RT (ADD1 X))
(RT (ADD1 X))
(TIMES (RT (ADD1 X))
(RT (ADD1 X)))))),
which further simplifies, rewriting with ADD1-EQUAL, TIMES-ADD1, and
SUB1-ADD1, and opening up PLUS, TIMES, and RT, to the following two new
formulas:
Case 1.2.
(IMPLIES (AND (NUMBERP X)
(NOT (EQUAL (PLUS (RT X)
(RT X)
(TIMES (RT X) (RT X)))
X)))
(LESSP X
(PLUS (RT X)
(RT X)
(TIMES (RT X) (RT X))))),
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 (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP Y
(ADD1 (PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))).
We gave this the name *1 above. Perhaps we can prove it by induction. There
are eight plausible inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y)))))
(p Y))
(IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(p Y))
(IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(p (SUB1 Y)))
(p Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates the following six new conjectures:
Case 6. (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y)))))
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))).
This simplifies, applying the lemmas SUB1-ADD1, TIMES-ADD1, and SQUARE-0,
and expanding the definitions of RT, TIMES, PLUS, NOT, OR, EQUAL, LESSP, and
ADD1, to the following six new formulas:
Case 6.6.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(NOT (EQUAL 1 Y)))
(NOT (LESSP Y (TIMES 0 0)))).
But this again simplifies, unfolding the functions TIMES, PLUS, ADD1,
EQUAL, and LESSP, to:
T.
Case 6.5.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(NOT (NUMBERP Y)))
(NOT (LESSP Y (TIMES 0 0)))),
which again simplifies, opening up TIMES, PLUS, ADD1, EQUAL, and LESSP, to:
T.
Case 6.4.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(EQUAL Y 0))
(NOT (LESSP Y (TIMES 0 0)))),
which again simplifies, expanding the definitions of TIMES, PLUS, ADD1,
EQUAL, SUB1, RT, and LESSP, to:
T.
Case 6.3.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL 1 Y))
(NOT (LESSP Y (TIMES 1 1)))),
which again simplifies, expanding TIMES, PLUS, ADD1, and EQUAL, to:
T.
Case 6.2.
(IMPLIES
(AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y)
(EQUAL (ADD1 (RT (SUB1 Y))) 0)
(NOT (EQUAL Y 0)))
(NOT (LESSP Y
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 6.1.
(IMPLIES
(AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y)
(EQUAL (ADD1 (RT (SUB1 Y))) 0)
(EQUAL Y 0))
(NOT (LESSP Y (TIMES 0 0)))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))),
which simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and
unfolding the definitions of RT, TIMES, PLUS, NOT, and OR, to:
T.
Case 4. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))))
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))).
This simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, and
SQUARE-0, and unfolding the functions RT, TIMES, PLUS, NOT, OR, and LESSP,
to the following two new formulas:
Case 4.2.
(IMPLIES
(AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(NOT (EQUAL (RT (SUB1 Y)) 0))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))))
(NOT (LESSP Y
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))).
This again simplifies, using linear arithmetic, to:
T.
Case 4.1.
(IMPLIES
(AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y)
(NOT (EQUAL (ADD1 (RT (SUB1 Y))) 0))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))))
(NOT (LESSP (SUB1 Y) (SUB1 Y)))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y)))))
(LESSP Y
(ADD1 (PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))),
which simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0, and
opening up the functions RT, TIMES, PLUS, NOT, OR, ADD1, NUMBERP, EQUAL, and
LESSP, to the following three new goals:
Case 3.3.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL 1 Y)))
(LESSP (SUB1 Y)
(PLUS 0 0 (TIMES 0 0)))).
But this again simplifies, opening up the functions TIMES, PLUS, ADD1,
EQUAL, and LESSP, to the goal:
(IMPLIES (AND (EQUAL (RT (SUB1 Y)) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y))
(EQUAL 1 Y)).
Appealing to the lemma SUB1-ELIM, we now replace Y by (ADD1 X) to
eliminate (SUB1 Y). We employ the type restriction lemma noted when SUB1
was introduced to constrain the new variable. The result is the
conjecture:
(IMPLIES (AND (NUMBERP X)
(EQUAL (RT X) 0)
(NOT (EQUAL (ADD1 X) 0)))
(EQUAL 1 (ADD1 X))).
This further simplifies, applying ADD1-EQUAL, and unfolding the function
NUMBERP, to:
(IMPLIES (AND (NUMBERP X) (EQUAL (RT X) 0))
(EQUAL 0 X)),
which we will name *1.1.
Case 3.2.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(EQUAL (RT (SUB1 Y)) 0)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL 1 Y))
(LESSP (SUB1 Y)
(PLUS 1 1 (TIMES 1 1)))).
This again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES
(AND (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y)
(EQUAL (ADD1 (RT (SUB1 Y))) 0)
(NOT (EQUAL Y 0)))
(LESSP (SUB1 Y)
(PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(LESSP Y
(ADD1 (PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))),
which simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, and
SQUARE-0, and opening up the definitions of RT, TIMES, PLUS, NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (NUMBERP (TIMES (RT Y) (RT Y))))))
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))))
(LESSP Y
(ADD1 (PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))),
which simplifies, rewriting with the lemmas SUB1-ADD1, TIMES-ADD1, SQUARE-0,
and PLUS-ADD1, and expanding the definitions of RT, TIMES, PLUS, NOT, OR,
and LESSP, to two new formulas:
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(NOT (EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y))
(NOT (EQUAL (RT (SUB1 Y)) 0))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))))
(LESSP (SUB1 Y)
(PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y))
(RT (SUB1 Y)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL (ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
Y)
(NOT (EQUAL (ADD1 (RT (SUB1 Y))) 0))
(NOT (LESSP (SUB1 Y)
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y)))))
(LESSP (SUB1 Y)
(ADD1 (PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
(TIMES (RT (SUB1 Y)) (RT (SUB1 Y))))))
(NOT (EQUAL (SUB1 Y) 0))
(NOT (EQUAL (SUB1 (SUB1 Y)) 0)))
(LESSP (SUB1 (SUB1 (SUB1 Y)))
(PLUS (RT (SUB1 Y))
(RT (SUB1 Y))
Y))),
which again simplifies, using linear arithmetic, to:
T.
So next consider:
(IMPLIES (AND (NUMBERP X) (EQUAL (RT X) 0))
(EQUAL 0 X)),
named *1.1 above. We will try to prove it by induction. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X))
(IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(p (SUB1 X)))
(p X))
(IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X))
(p (SUB1 X)))
(p X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and SUB1-ADD1, and the definitions
of ZEROP, TIMES, and PLUS establish 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 five new formulas:
Case 5. (IMPLIES (AND (ZEROP X)
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)),
which simplifies, opening up the function ZEROP, to:
T.
Case 4. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(NOT (EQUAL (RT (SUB1 X)) 0))
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)),
which simplifies, rewriting with SUB1-ADD1 and TIMES-ADD1, and opening up
the definitions of ZEROP, TIMES, PLUS, and RT, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X)
(EQUAL 0 (SUB1 X))
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)).
This simplifies, using linear arithmetic, to the new formula:
(IMPLIES (AND (EQUAL (TIMES (ADD1 (RT 0)) (ADD1 (RT 0)))
1)
(NOT (ZEROP X))
(EQUAL 1 X)
(EQUAL 0 (SUB1 X))
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)),
which again simplifies, unfolding RT, ADD1, TIMES, EQUAL, ZEROP, SUB1, and
NUMBERP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X))
(NOT (EQUAL (RT (SUB1 X)) 0))
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)),
which simplifies, applying the lemmas SUB1-ADD1 and TIMES-ADD1, and
expanding ZEROP, TIMES, PLUS, and RT, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL (TIMES (ADD1 (RT (SUB1 X)))
(ADD1 (RT (SUB1 X))))
X))
(EQUAL 0 (SUB1 X))
(NUMBERP X)
(EQUAL (RT X) 0))
(EQUAL 0 X)),
which simplifies, applying SUB1-ADD1 and TIMES-ADD1, and expanding the
functions ZEROP, RT, ADD1, TIMES, and PLUS, to the following two new goals:
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL 1 X))
(EQUAL 0 (SUB1 X))
(NUMBERP X)
(NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X))
(EQUAL (RT (SUB1 X)) 0))
(EQUAL 0 X)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL 1 X))
(EQUAL 0 (SUB1 X))
(NUMBERP X)
(EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X)
(EQUAL (ADD1 (RT (SUB1 X))) 0))
(EQUAL 0 X)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1.1, which finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
SPEC-FOR-RT
(PROVE-LEMMA RT-IS-UNIQUE NIL
(IMPLIES (AND (NUMBERP A)
(LEQ (TIMES A A) Y)
(LESSP Y (TIMES (ADD1 A) (ADD1 A))))
(EQUAL A (RT Y)))
((USE (SPEC-FOR-RT)
(SQUARE-MONOTONIC (A (ADD1 A))
(B (RT Y)))
(SQUARE-MONOTONIC (A (ADD1 (RT Y)))
(B A)))))
This formula simplifies, rewriting with SUB1-ADD1, TIMES-ADD1, and SQUARE-0,
and opening up the definitions of LESSP, RT, EQUAL, NOT, TIMES, PLUS, IMPLIES,
ADD1, and NUMBERP, to 20 new conjectures:
Case 20.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP 0 (TIMES (RT 0) (RT 0))))
(LESSP (SUB1 0)
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0))))
(NOT (LESSP (SUB1 (TIMES (RT 0) (RT 0)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0)))))
(NUMBERP A)
(NOT (LESSP 0 (TIMES A A))))
(EQUAL A 0)).
This again simplifies, obviously, to:
T.
Case 19.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to two new conjectures:
Case 19.2.
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)),
which again simplifies, applying SQUARE-0, to:
T.
Case 19.1.
(IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y 0))
(LESSP (SUB1 Y)
(PLUS (RT Y) (RT Y) 0))
(NOT (LESSP (SUB1 0)
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y) (RT Y) 0)))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)).
But this again simplifies, appealing to the lemma SQUARE-0, to:
T.
Case 18.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 18.2.
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0)
(EQUAL (TIMES A A) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A 0)))
(NOT (LESSP (SUB1 0)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y 0))
(LESSP (SUB1 Y) (PLUS A A 0)))
(EQUAL A (RT Y))).
However this again simplifies, rewriting with SQUARE-0, and opening up the
functions EQUAL, LESSP, and PLUS, to:
T.
Case 18.1.
(IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y 0))
(LESSP (SUB1 Y)
(PLUS (RT Y) (RT Y) 0))
(NOT (LESSP (SUB1 0)
(PLUS A A (TIMES A A))))
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y) (RT Y) 0)))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
But this again simplifies, rewriting with SQUARE-0, and expanding the
functions EQUAL, LESSP, and PLUS, to:
T.
Case 17.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES (RT 0) (RT 0)) 0)
(NOT (LESSP 0 (TIMES (RT 0) (RT 0))))
(LESSP (SUB1 0)
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0))))
(NOT (LESSP (SUB1 (TIMES (RT 0) (RT 0)))
(PLUS A A (TIMES A A))))
(LESSP (SUB1 A) (RT 0))
(NUMBERP A)
(NOT (LESSP 0 (TIMES A A))))
(EQUAL A 0)).
This again simplifies, opening up the definitions of RT, TIMES, EQUAL, LESSP,
SUB1, and PLUS, to:
T.
Case 16.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)),
which again simplifies, applying SUB1-NNUMBERP, and expanding the
definitions of RT, TIMES, EQUAL, LESSP, and PLUS, to:
T.
Case 15.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
But this again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
However this again simplifies, rewriting with the lemma SQUARE-0, and
expanding the definitions of EQUAL, LESSP, and PLUS, to:
T.
Case 14.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS A A (TIMES A A))))
(EQUAL A 0)
(LESSP Y 1))
(EQUAL 0 (RT Y))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES (RT Y) (RT Y)) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(NOT (LESSP (SUB1 (TIMES (RT Y) (RT Y)))
(PLUS 0 0 (TIMES 0 0))))
(LESSP Y 1))
(EQUAL 0 (RT Y))).
But this again simplifies, rewriting with SQUARE-0, to:
T.
Case 13.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP 0 (TIMES (RT 0) (RT 0))))
(LESSP (SUB1 0)
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0))))
(LESSP (SUB1 (RT 0)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0)))))
(NUMBERP A)
(NOT (LESSP 0 (TIMES A A))))
(EQUAL A 0)).
This again simplifies, trivially, to:
T.
Case 12.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)).
But this again simplifies, rewriting with SQUARE-0, to:
T.
Case 11.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (TIMES A A) 0)
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(NOT (LESSP (SUB1 (TIMES A A))
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y)))))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))).
This again simplifies, applying the lemma SQUARE-0, and expanding EQUAL and
LESSP, to:
T.
Case 10.(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (LESSP 0 (TIMES (RT 0) (RT 0))))
(LESSP (SUB1 0)
(PLUS (RT 0)
(RT 0)
(TIMES (RT 0) (RT 0))))
(LESSP (SUB1 (RT 0)) (RT 0))
(LESSP (SUB1 (RT 0)) (RT 0))
(NUMBERP (RT 0))
(NOT (LESSP 0 (TIMES (RT 0) (RT 0)))))
(EQUAL (RT 0) 0)).
But this again simplifies, expanding RT, TIMES, LESSP, SUB1, and PLUS, to:
T.
Case 9. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) (RT Y))
(LESSP (SUB1 (RT Y)) (RT Y))
(NUMBERP (RT Y))
(NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(NOT (NUMBERP Y)))
(EQUAL (RT Y) 0)).
However this again simplifies, rewriting with the lemma SUB1-NNUMBERP, and
expanding the functions RT, TIMES, EQUAL, LESSP, and PLUS, to:
T.
Case 8. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(LESSP (SUB1 A) (RT Y))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A (RT Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(LESSP (SUB1 (RT Y)) A)
(EQUAL A 0)
(LESSP Y 1))
(EQUAL 0 (RT Y))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(LESSP A 1)
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(LESSP A 1)
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(LESSP A 1)
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(NOT (LESSP (TIMES A A) 1))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(EQUAL Y 0))
(EQUAL A 0)),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(NOT (LESSP (TIMES A A) 1))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(NOT (NUMBERP Y)))
(EQUAL A 0)),
which again simplifies, applying SUB1-NNUMBERP, and opening up the functions
TIMES, EQUAL, LESSP, and PLUS, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP Y (TIMES (RT Y) (RT Y))))
(LESSP (SUB1 Y)
(PLUS (RT Y)
(RT Y)
(TIMES (RT Y) (RT Y))))
(EQUAL (RT Y) 0)
(NOT (LESSP (TIMES A A) 1))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A 0)).
This again simplifies, using linear arithmetic, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP Y))
(NOT (LESSP Y (TIMES 0 0)))
(LESSP (SUB1 Y)
(PLUS 0 0 (TIMES 0 0)))
(EQUAL (RT Y) 0)
(NOT (LESSP (TIMES A A) 1))
(NUMBERP A)
(NOT (LESSP Y (TIMES A A)))
(LESSP (SUB1 Y)
(PLUS A A (TIMES A A))))
(EQUAL A 0)),
which again simplifies, rewriting with SUB1-NNUMBERP, and opening up TIMES,
EQUAL, LESSP, and PLUS, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP Y)
(NOT (LESSP (TIMES 0 0) (TIMES 0 0)))
(LESSP (SUB1 (TIMES 0 0))
(PLUS 0 0 (TIMES 0 0)))
(EQUAL (RT (TIMES 0 0)) 0)
(NOT (LESSP (TIMES A A) 1))
(NUMBERP A)
(NOT (LESSP (TIMES 0 0) (TIMES A A)))
(LESSP (SUB1 (TIMES 0 0))
(PLUS A A (TIMES A A))))
(EQUAL A 0)).
However this again simplifies, unfolding TIMES, LESSP, SUB1, and PLUS, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
RT-IS-UNIQUE
(PROVE-LEMMA NCONS-LEMMA
(REWRITE)
(EQUAL (RT (PLUS U
(TIMES (PLUS U V) (PLUS U V))))
(PLUS U V))
((USE (RT-IS-UNIQUE (Y (PLUS U
(TIMES (PLUS U V) (PLUS U V))))
(A (PLUS U V))))))
This formula simplifies, rewriting with the lemmas SUB1-ADD1 and TIMES-ADD1,
and expanding TIMES, PLUS, LESSP, AND, and IMPLIES, to two new conjectures:
Case 2. (IMPLIES (LESSP (PLUS U (TIMES (PLUS U V) (PLUS U V)))
(TIMES (PLUS U V) (PLUS U V)))
(EQUAL (RT (PLUS U
(TIMES (PLUS U V) (PLUS U V))))
(PLUS U V))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (PLUS U (TIMES (PLUS U V) (PLUS U V)))
0))
(NOT (LESSP (SUB1 (PLUS U
(TIMES (PLUS U V) (PLUS U V))))
(PLUS (PLUS U V)
(PLUS U V)
(TIMES (PLUS U V) (PLUS U V))))))
(EQUAL (RT (PLUS U
(TIMES (PLUS U V) (PLUS U V))))
(PLUS U V))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
NCONS-LEMMA
(DEFN NCAR
(X)
(DIFFERENCE X (TIMES (RT X) (RT X))))
Observe that (NUMBERP (NCAR X)) is a theorem.
[ 0.0 0.0 0.0 ]
NCAR
(DEFN NCDR
(X)
(DIFFERENCE (RT X) (NCAR X)))
Observe that (NUMBERP (NCDR X)) is a theorem.
[ 0.0 0.0 0.0 ]
NCDR
(DEFN NCONS
(I J)
(PLUS I
(TIMES (PLUS I J) (PLUS I J))))
Observe that (NUMBERP (NCONS I J)) is a theorem.
[ 0.0 0.0 0.0 ]
NCONS
(PROVE-LEMMA NCAR-NCONS NIL
(IMPLIES (NUMBERP I)
(EQUAL (NCAR (NCONS I J)) I)))
This conjecture simplifies, applying NCONS-LEMMA, and unfolding the functions
NCONS and NCAR, to the formula:
(IMPLIES (NUMBERP I)
(EQUAL (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J)))
I)).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J)))
(NUMBERP I))
(EQUAL (DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J)))
I)).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NCAR-NCONS
(PROVE-LEMMA NCDR-NCONS NIL
(IMPLIES (NUMBERP J)
(EQUAL (NCDR (NCONS I J)) J)))
This conjecture simplifies, applying NCONS-LEMMA, and unfolding the functions
NCONS, NCAR, and NCDR, to the formula:
(IMPLIES
(NUMBERP J)
(EQUAL (DIFFERENCE (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
J)).
This again simplifies, using linear arithmetic, to two new formulas:
Case 2. (IMPLIES
(AND (LESSP (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
(NUMBERP J))
(EQUAL (DIFFERENCE (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
J)),
which again simplifies, using linear arithmetic, to:
(IMPLIES
(AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J)))
(LESSP (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
(NUMBERP J))
(EQUAL (DIFFERENCE (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
J)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES
(AND (LESSP (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J)))
(NUMBERP J))
(EQUAL (DIFFERENCE (PLUS I J)
(DIFFERENCE (PLUS I (TIMES (PLUS I J) (PLUS I J)))
(TIMES (PLUS I J) (PLUS I J))))
J)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NCDR-NCONS
(DEFN NCADR (X) (NCAR (NCDR X)))
From the definition we can conclude that (NUMBERP (NCADR X)) is a theorem.
[ 0.0 0.0 0.0 ]
NCADR
(DEFN NCADDR
(X)
(NCAR (NCDR (NCDR X))))
Note that (NUMBERP (NCADDR X)) is a theorem.
[ 0.0 0.0 0.0 ]
NCADDR
(PROVE-LEMMA RT-LESSP
(REWRITE)
(IMPLIES (AND (NOT (ZEROP X))
(NOT (EQUAL X 1)))
(LESSP (RT X) X)))
WARNING: Note that the proposed lemma RT-LESSP 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 ZEROP, NOT, AND,
and IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)).
Name the above subgoal *1.
Perhaps we can prove it by induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (OR (EQUAL X 0) (NOT (NUMBERP X)))
(p X))
(IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X)))))
(p X))
(IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X)))))
(p (SUB1 X)))
(p X))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following five new goals:
Case 5. (IMPLIES (AND (OR (EQUAL X 0) (NOT (NUMBERP X)))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)).
This simplifies, opening up NOT and OR, to:
T.
Case 4. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X))))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)).
This simplifies, applying the lemmas SUB1-ADD1 and TIMES-ADD1, and expanding
the definitions of NOT, OR, RT, TIMES, PLUS, ADD1, EQUAL, and LESSP, to the
new formula:
(IMPLIES (AND (EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X)
(EQUAL (ADD1 (RT (SUB1 X))) 0)
(NOT (EQUAL X 0))
(NOT (EQUAL X 1)))
(LESSP (RT (SUB1 X)) X)),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X)))))
(EQUAL (SUB1 X) 0)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)),
which simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X)))))
(EQUAL (SUB1 X) 1)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)),
which simplifies, rewriting with the lemmas SUB1-ADD1 and TIMES-ADD1, and
expanding the definitions of NOT, OR, RT, TIMES, PLUS, and LESSP, to two new
goals:
Case 2.2.
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X))
(NOT (EQUAL (RT (SUB1 X)) 0))
(EQUAL (SUB1 X) 1)
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT (SUB1 X)) X)),
which again simplifies, opening up the definitions of RT, TIMES, PLUS,
ADD1, EQUAL, LESSP, SUB1, and NUMBERP, to:
T.
Case 2.1.
(IMPLIES
(AND (EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X)
(NOT (EQUAL (ADD1 (RT (SUB1 X))) 0))
(EQUAL (SUB1 X) 1)
(NOT (EQUAL X 0))
(NOT (EQUAL X 1)))
(LESSP (RT (SUB1 X)) 1)),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (OR (EQUAL (RT X) 0)
(NOT (NUMBERP (RT X)))))
(LESSP (RT (SUB1 X)) (SUB1 X))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT X) X)),
which simplifies, rewriting with SUB1-ADD1 and TIMES-ADD1, and unfolding NOT,
OR, RT, TIMES, PLUS, and LESSP, to the new formula:
(IMPLIES
(AND (NOT (EQUAL (ADD1 (PLUS (RT (SUB1 X))
(RT (SUB1 X))
(TIMES (RT (SUB1 X)) (RT (SUB1 X)))))
X))
(NOT (EQUAL (RT (SUB1 X)) 0))
(LESSP (RT (SUB1 X)) (SUB1 X))
(NOT (EQUAL X 0))
(NUMBERP X)
(NOT (EQUAL X 1)))
(LESSP (RT (SUB1 X)) X)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
RT-LESSP
(PROVE-LEMMA RT-LESSEQP
(REWRITE)
(NOT (LESSP X (RT X)))
((USE (RT-LESSP))))
WARNING: Note that the proposed lemma RT-LESSEQP is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
This simplifies, unfolding the definitions of ZEROP, NOT, AND, IMPLIES, RT,
LESSP, and EQUAL, to the new goal:
(IMPLIES (LESSP (RT X) X)
(NOT (LESSP X (RT X)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
RT-LESSEQP
(PROVE-LEMMA DIFFERENCE-0
(REWRITE)
(IMPLIES (LESSP X Y)
(EQUAL (DIFFERENCE X Y) 0)))
Give the conjecture the name *1.
We will try to prove it by induction. There are four plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
(p X Y))
(IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(OR (EQUAL X 0) (NOT (NUMBERP X))))
(p X Y))
(IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(p (SUB1 X) (SUB1 Y)))
(p X Y))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT inform us that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for Y. The above induction scheme
generates four new goals:
Case 4. (IMPLIES (AND (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which simplifies, expanding NOT, OR, EQUAL, and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(OR (EQUAL X 0) (NOT (NUMBERP X)))
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which simplifies, opening up the functions NOT, OR, EQUAL, LESSP, and
DIFFERENCE, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 Y)))
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which simplifies, using linear arithmetic, to the formula:
(IMPLIES (AND (LESSP X 1)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(NOT (LESSP (SUB1 X) (SUB1 Y)))
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)).
But this again simplifies, unfolding the functions SUB1, NUMBERP, EQUAL,
LESSP, NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
0)
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which simplifies, using linear arithmetic, to two new goals:
Case 1.2.
(IMPLIES (AND (LESSP (SUB1 X) (SUB1 Y))
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
0)
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which again simplifies, expanding NOT, OR, LESSP, DIFFERENCE, and EQUAL,
to:
T.
Case 1.1.
(IMPLIES (AND (LESSP X 1)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 X) (SUB1 Y))
0)
(LESSP X Y))
(EQUAL (DIFFERENCE X Y) 0)),
which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DIFFERENCE-0
(PROVE-LEMMA LESSP-DIFFERENCE-1
(REWRITE)
(EQUAL (LESSP (DIFFERENCE A B) C)
(IF (LESSP A B)
(LESSP 0 C)
(LESSP A (PLUS B C)))))
This conjecture simplifies, expanding the functions EQUAL and LESSP, to the
following three new formulas:
Case 3. (IMPLIES (NOT (LESSP A B))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))).
Call the above conjecture *1.
Case 2. (IMPLIES (AND (LESSP A B) (EQUAL C 0))
(EQUAL (LESSP (DIFFERENCE A B) C) F)).
This again simplifies, applying DIFFERENCE-0, and expanding the functions
LESSP and EQUAL, to:
T.
Case 1. (IMPLIES (AND (LESSP A B) (NOT (EQUAL C 0)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(NUMBERP C))).
However this again simplifies, rewriting with DIFFERENCE-0, and unfolding
EQUAL and LESSP, to:
T.
So let us turn our attention to:
(IMPLIES (NOT (LESSP A B))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))),
named *1 above. Perhaps we can prove it by induction. There are seven
plausible inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (OR (EQUAL B 0) (NOT (NUMBERP B)))
(p A B C))
(IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(OR (EQUAL A 0) (NOT (NUMBERP A))))
(p A B C))
(IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(p (SUB1 A) (SUB1 B) C))
(p A B C))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish 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 B. The above induction scheme
produces the following four new goals:
Case 4. (IMPLIES (AND (OR (EQUAL B 0) (NOT (NUMBERP B)))
(NOT (LESSP A B)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))).
This simplifies, opening up the definitions of NOT, OR, EQUAL, LESSP,
DIFFERENCE, and PLUS, to the following ten new conjectures:
Case 4.10.
(IMPLIES (AND (EQUAL B 0)
(NOT (NUMBERP C))
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP A C) (LESSP A 0))).
However this again simplifies, unfolding LESSP and EQUAL, to:
T.
Case 4.9.
(IMPLIES (AND (EQUAL B 0)
(NOT (NUMBERP C))
(EQUAL A 0))
(EQUAL (LESSP 0 C) (LESSP A 0))),
which again simplifies, unfolding LESSP and EQUAL, to:
T.
Case 4.8.
(IMPLIES (AND (EQUAL B 0)
(NOT (NUMBERP C))
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 C) (LESSP A 0))),
which again simplifies, expanding the functions LESSP and EQUAL, to:
T.
Case 4.7.
(IMPLIES (AND (EQUAL B 0)
(NUMBERP C)
(EQUAL A 0))
(EQUAL (LESSP 0 C) (LESSP A C))),
which again simplifies, clearly, to:
T.
Case 4.6.
(IMPLIES (AND (EQUAL B 0)
(NUMBERP C)
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 C) (LESSP A C))).
But this again simplifies, unfolding the definitions of EQUAL and LESSP,
to:
T.
Case 4.5.
(IMPLIES (AND (NOT (NUMBERP B))
(NOT (NUMBERP C))
(NOT (EQUAL A 0))
(NUMBERP A))
(EQUAL (LESSP A C) (LESSP A 0))),
which again simplifies, unfolding the functions LESSP and EQUAL, to:
T.
Case 4.4.
(IMPLIES (AND (NOT (NUMBERP B))
(NOT (NUMBERP C))
(EQUAL A 0))
(EQUAL (LESSP 0 C) (LESSP A 0))),
which again simplifies, expanding the functions LESSP and EQUAL, to:
T.
Case 4.3.
(IMPLIES (AND (NOT (NUMBERP B))
(NOT (NUMBERP C))
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 C) (LESSP A 0))),
which again simplifies, expanding LESSP and EQUAL, to:
T.
Case 4.2.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP C)
(EQUAL A 0))
(EQUAL (LESSP 0 C) (LESSP A C))),
which again simplifies, obviously, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (NUMBERP B))
(NUMBERP C)
(NOT (NUMBERP A)))
(EQUAL (LESSP 0 C) (LESSP A C))).
This again simplifies, unfolding EQUAL and LESSP, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(OR (EQUAL A 0) (NOT (NUMBERP A)))
(NOT (LESSP A B)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))),
which simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(LESSP (SUB1 A) (SUB1 B))
(NOT (LESSP A B)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))),
which simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP B 1)
(NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(LESSP (SUB1 A) (SUB1 B))
(NOT (LESSP A B)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))).
This again simplifies, expanding the functions SUB1, NUMBERP, EQUAL, LESSP,
NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL B 0) (NOT (NUMBERP B))))
(NOT (OR (EQUAL A 0) (NOT (NUMBERP A))))
(EQUAL (LESSP (DIFFERENCE (SUB1 A) (SUB1 B))
C)
(LESSP (SUB1 A) (PLUS (SUB1 B) C)))
(NOT (LESSP A B)))
(EQUAL (LESSP (DIFFERENCE A B) C)
(LESSP A (PLUS B C)))),
which simplifies, applying SUB1-ADD1, and expanding the definitions of NOT,
OR, LESSP, DIFFERENCE, and PLUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-DIFFERENCE-1
(PROVE-LEMMA NCAR-LESSEQP
(REWRITE)
(NOT (LESSP X (NCAR X))))
WARNING: Note that the linear lemma NCAR-LESSEQP is being stored under the
term (NCAR X), which is unusual because NCAR is a nonrecursive function symbol.
WARNING: Note that the proposed lemma NCAR-LESSEQP is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
This simplifies, expanding the function NCAR, to:
(NOT (LESSP X
(DIFFERENCE X
(TIMES (RT X) (RT X))))),
which again simplifies, using linear arithmetic, to the goal:
(IMPLIES (LESSP X (TIMES (RT X) (RT X)))
(NOT (LESSP X
(DIFFERENCE X
(TIMES (RT X) (RT X)))))).
This again simplifies, rewriting with DIFFERENCE-0, and expanding EQUAL and
LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NCAR-LESSEQP
(PROVE-LEMMA CROCK
(REWRITE)
(EQUAL (LESSP X (DIFFERENCE (RT X) D))
F)
NIL)
This conjecture simplifies, using linear arithmetic and applying RT-LESSEQP,
to:
(IMPLIES (LESSP (RT X) D)
(NOT (LESSP X (DIFFERENCE (RT X) D)))).
But this again simplifies, rewriting with DIFFERENCE-0, and unfolding the
definitions of EQUAL and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CROCK
(PROVE-LEMMA NCDR-LESSEQP
(REWRITE)
(NOT (LESSP X (NCDR X))))
WARNING: Note that the linear lemma NCDR-LESSEQP is being stored under the
term (NCDR X), which is unusual because NCDR is a nonrecursive function symbol.
WARNING: Note that the proposed lemma NCDR-LESSEQP is to be stored as zero
type prescription rules, zero compound recognizer rules, one linear rule, and
zero replacement rules.
This simplifies, applying CROCK, and opening up the definitions of NCAR and
NCDR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NCDR-LESSEQP
(PROVE-LEMMA NCDR-LESSP
(REWRITE)
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (NCAR FN) 0))
(NOT (EQUAL (NCAR FN) 1)))
(LESSP (NCDR FN) FN)))
WARNING: Note that the linear lemma NCDR-LESSP is being stored under the term
(NCDR FN), which is unusual because NCDR is a nonrecursive function symbol.
WARNING: Note that the proposed lemma NCDR-LESSP is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
This formula simplifies, rewriting with LESSP-DIFFERENCE-1, and opening up the
functions NCAR, NCDR, EQUAL, and LESSP, to the following two new goals:
Case 2. (IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
0))
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
1))
(NOT (LESSP (RT FN)
(DIFFERENCE FN
(TIMES (RT FN) (RT FN))))))
(LESSP (RT FN)
(PLUS (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
FN))).
However this again simplifies, using linear arithmetic, rewriting with
RT-LESSEQP and DIFFERENCE-0, and unfolding EQUAL, LESSP, and PLUS, to the
following two new goals:
Case 2.2.
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
0))
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
1))
(LESSP FN (TIMES (RT FN) (RT FN)))
(NOT (LESSP (RT FN)
(DIFFERENCE FN
(TIMES (RT FN) (RT FN))))))
(LESSP (RT FN) FN)).
This again simplifies, using linear arithmetic and appealing to the lemma
RT-LESSEQP, to the goal:
(IMPLIES (AND (EQUAL (RT FN) FN)
(NUMBERP FN)
(NOT (EQUAL (DIFFERENCE FN (TIMES FN FN))
0))
(NOT (EQUAL (DIFFERENCE FN (TIMES FN FN))
1))
(LESSP FN (TIMES FN FN))
(NOT (LESSP FN
(DIFFERENCE FN (TIMES FN FN)))))
(LESSP FN FN)).
However this again simplifies, applying DIFFERENCE-0, and expanding the
function EQUAL, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
0))
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
1))
(NOT (LESSP FN (TIMES (RT FN) (RT FN)))))
(LESSP (RT FN)
(PLUS (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
FN))).
But this again simplifies, using linear arithmetic and rewriting with
RT-LESSEQP, to:
T.
Case 1. (IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
0))
(NOT (EQUAL (DIFFERENCE FN
(TIMES (RT FN) (RT FN)))
1))
(LESSP (RT FN)
(DIFFERENCE FN
(TIMES (RT FN) (RT FN)))))
(NOT (EQUAL FN 0))).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP 0 (TIMES (RT 0) (RT 0)))
(NUMBERP 0)
(NOT (EQUAL (DIFFERENCE 0 (TIMES (RT 0) (RT 0)))
0))
(NOT (EQUAL (DIFFERENCE 0 (TIMES (RT 0) (RT 0)))
1)))
(NOT (LESSP (RT 0)
(DIFFERENCE 0
(TIMES (RT 0) (RT 0)))))).
But this again simplifies, expanding the definitions of RT, TIMES, and LESSP,
to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
NCDR-LESSP
(DISABLE NCAR)
[ 0.0 0.0 0.0 ]
NCAR-OFF
(DISABLE NCDR)
[ 0.0 0.0 0.0 ]
NCDR-OFF
(DEFN PR-APPLY
(FN ARG)
(IF (NOT (NUMBERP FN))
0
(IF (EQUAL (NCAR FN) 0)
0
(IF (EQUAL (NCAR FN) 1)
ARG
(IF (EQUAL (NCAR FN) 2)
(ADD1 ARG)
(IF (EQUAL (NCAR FN) 3)
(RT ARG)
(IF (EQUAL (NCAR FN) 4)
(IF (ZEROP ARG)
0
(PR-APPLY (NCDR FN)
(PR-APPLY FN (SUB1 ARG))))
(IF (EQUAL (NCAR FN) 5)
(PLUS (PR-APPLY (NCADR FN) ARG)
(PR-APPLY (NCADDR FN) ARG))
(IF (EQUAL (NCAR FN) 6)
(DIFFERENCE (PR-APPLY (NCADR FN) ARG)
(PR-APPLY (NCADDR FN) ARG))
(IF (EQUAL (NCAR FN) 7)
(TIMES (PR-APPLY (NCADR FN) ARG)
(PR-APPLY (NCADDR FN) ARG))
(IF (EQUAL (NCAR FN) 8)
(PR-APPLY (NCADR FN)
(PR-APPLY (NCADDR FN) ARG))
0))))))))))
((ORD-LESSP (CONS (ADD1 (COUNT FN))
(COUNT ARG)))))
Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, SUB1-ADD1, ADD1-EQUAL,
COUNT-NUMBERP, NCDR-LESSP, NCAR-LESSEQP, and NCDR-LESSEQP, and the definitions
of ORDINALP, LESSP, ORD-LESSP, ZEROP, EQUAL, NCADDR, and NCADR establish that
the measure (CONS (ADD1 (COUNT FN)) (COUNT ARG)) decreases according to the
well-founded relation ORD-LESSP in each recursive call. Hence, PR-APPLY is
accepted under the definitional principle. Observe that:
(OR (NUMBERP (PR-APPLY FN ARG))
(EQUAL (PR-APPLY FN ARG) ARG))
is a theorem.
[ 0.0 0.0 0.0 ]
PR-APPLY
(DEFN NON-PR-FN
(X)
(ADD1 (PR-APPLY X X)))
Observe that (NUMBERP (NON-PR-FN X)) is a theorem.
[ 0.0 0.0 0.0 ]
NON-PR-FN
(DEFN COUNTER-EXAMPLE-FOR (X) (FIX X))
Observe that (NUMBERP (COUNTER-EXAMPLE-FOR X)) is a theorem.
[ 0.0 0.0 0.0 ]
COUNTER-EXAMPLE-FOR
(PROVE-LEMMA NON-PR-FUNCTIONS-EXIST NIL
(NOT (EQUAL (NON-PR-FN (COUNTER-EXAMPLE-FOR FN))
(PR-APPLY FN
(COUNTER-EXAMPLE-FOR FN)))))
This formula simplifies, expanding the function COUNTER-EXAMPLE-FOR, to two
new conjectures:
Case 2. (IMPLIES (NOT (NUMBERP FN))
(NOT (EQUAL (NON-PR-FN 0)
(PR-APPLY FN 0)))),
which again simplifies, opening up the functions NON-PR-FN, PR-APPLY, and
EQUAL, to:
T.
Case 1. (IMPLIES (NUMBERP FN)
(NOT (EQUAL (NON-PR-FN FN)
(PR-APPLY FN FN)))),
which again simplifies, opening up the definition of NON-PR-FN, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
NON-PR-FUNCTIONS-EXIST
(PROVE-LEMMA COUNTER-EXAMPLE-FOR-NUMERIC
(REWRITE)
(NUMBERP (COUNTER-EXAMPLE-FOR X)))
This simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
COUNTER-EXAMPLE-FOR-NUMERIC
(DISABLE PR-APPLY)
[ 0.0 0.0 0.0 ]
PR-APPLY-OFF
(DEFN MAX2
(FN I)
(IF (ZEROP I)
(PR-APPLY FN I)
(MAX (PR-APPLY FN I)
(MAX2 FN (SUB1 I)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT I) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MAX2 is accepted under the
definitional principle. Note that:
(OR (NUMBERP (MAX2 FN I))
(EQUAL (MAX2 FN I) I))
is a theorem.
[ 0.0 0.0 0.0 ]
MAX2
(DEFN MAX1
(FN I)
(IF (ZEROP FN)
(MAX2 FN I)
(MAX (MAX2 FN I) (MAX1 (SUB1 FN) I))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT FN) decreases according to the well-founded
relation LESSP in each recursive call. Hence, MAX1 is accepted under the
definitional principle. Note that:
(OR (NUMBERP (MAX1 FN I))
(EQUAL (MAX1 FN I) I))
is a theorem.
[ 0.0 0.0 0.0 ]
MAX1
(PROVE-LEMMA MAX2-GTE
(REWRITE)
(NOT (LESSP (MAX2 I J) (PR-APPLY I J))))
WARNING: Note that the proposed lemma MAX2-GTE is to be stored as zero type
prescription rules, zero compound recognizer rules, two linear rules, and zero
replacement rules.
Name the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP J) (p I J))
(IMPLIES (AND (NOT (ZEROP J)) (p I (SUB1 J)))
(p I J))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT J) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme produces the following two new goals:
Case 2. (IMPLIES (ZEROP J)
(NOT (LESSP (MAX2 I J) (PR-APPLY I J)))).
This simplifies, expanding ZEROP, EQUAL, and MAX2, to the following two new
formulas:
Case 2.2.
(IMPLIES (EQUAL J 0)
(NOT (LESSP (PR-APPLY I 0)
(PR-APPLY I 0)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2.1.
(IMPLIES (NOT (NUMBERP J))
(NOT (LESSP (PR-APPLY I J)
(PR-APPLY I J)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP J))
(NOT (LESSP (MAX2 I (SUB1 J))
(PR-APPLY I (SUB1 J)))))
(NOT (LESSP (MAX2 I J) (PR-APPLY I J)))),
which simplifies, expanding ZEROP, MAX2, and MAX, to two new formulas:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX2 I (SUB1 J))
(PR-APPLY I (SUB1 J))))
(NOT (LESSP (PR-APPLY I J)
(MAX2 I (SUB1 J)))))
(NOT (LESSP (PR-APPLY I J)
(PR-APPLY I J)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX2 I (SUB1 J))
(PR-APPLY I (SUB1 J))))
(LESSP (PR-APPLY I J)
(MAX2 I (SUB1 J))))
(NOT (LESSP (MAX2 I (SUB1 J))
(PR-APPLY I J)))),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
MAX2-GTE
(DEFN EXCEED (J) (ADD1 (MAX1 J J)))
Observe that (NUMBERP (EXCEED J)) is a theorem.
[ 0.0 0.0 0.0 ]
EXCEED
(DEFN EXCEED-AT (I) I)
Note that (EQUAL (EXCEED-AT I) I) is a theorem.
[ 0.0 0.0 0.0 ]
EXCEED-AT
(PROVE-LEMMA MAX1-GTE1
(REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN) I)
(PR-APPLY FN I)))))
WARNING: Note that the proposed lemma MAX1-GTE1 is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
Name the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP J) (p J FN I))
(IMPLIES (AND (NOT (ZEROP J))
(p (SUB1 J) FN I))
(p J FN I))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP inform us that the measure (COUNT J) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following two new conjectures:
Case 2. (IMPLIES (AND (ZEROP J) (NUMBERP FN))
(NOT (LESSP (MAX1 (PLUS J FN) I)
(PR-APPLY FN I)))).
This simplifies, opening up ZEROP, EQUAL, and PLUS, to the following two new
conjectures:
Case 2.2.
(IMPLIES (AND (EQUAL J 0) (NUMBERP FN))
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))).
This again simplifies, trivially, to:
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))),
which we will name *1.1.
Case 2.1.
(IMPLIES (AND (NOT (NUMBERP J)) (NUMBERP FN))
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))).
Eliminate the irrelevant term. This produces:
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))),
which we will name *1.2.
Case 1. (IMPLIES (AND (NOT (ZEROP J))
(NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I)
(PR-APPLY FN I)))
(NUMBERP FN))
(NOT (LESSP (MAX1 (PLUS J FN) I)
(PR-APPLY FN I)))).
This simplifies, rewriting with SUB1-ADD1, and unfolding the definitions of
ZEROP, PLUS, MAX, and MAX1, to two new goals:
Case 1.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I)
(PR-APPLY FN I)))
(NUMBERP FN)
(NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)
(MAX1 (PLUS (SUB1 J) FN) I)))
(NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)))
(NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)
(PR-APPLY FN I)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I)
(PR-APPLY FN I)))
(NUMBERP FN)
(NOT (LESSP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)
(MAX1 (PLUS (SUB1 J) FN) I)))
(NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I))))
(NOT (LESSP 0 (PR-APPLY FN I)))),
which again simplifies, opening up LESSP and EQUAL, to two new conjectures:
Case 1.1.2.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I)
(PR-APPLY FN I)))
(NUMBERP FN)
(EQUAL (MAX1 (PLUS (SUB1 J) FN) I) 0)
(NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)))
(NOT (EQUAL (PR-APPLY FN I) 0)))
(NOT (NUMBERP (PR-APPLY FN I)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.1.
(IMPLIES (AND (NOT (EQUAL J 0))
(NUMBERP J)
(NOT (LESSP (MAX1 (PLUS (SUB1 J) FN) I)
(PR-APPLY FN I)))
(NUMBERP FN)
(NOT (NUMBERP (MAX1 (PLUS (SUB1 J) FN) I)))
(NOT (NUMBERP (MAX2 (ADD1 (PLUS (SUB1 J) FN)) I)))
(NOT (EQUAL (PR-APPLY FN I) 0)))
(NOT (NUMBERP (PR-APPLY FN I)))),
which again simplifies, expanding the function LESSP, to:
T.
So we now return to:
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))),
which is formula *1.2 above. This conjecture is subsumed by formula *1.1
above.
So let us turn our attention to:
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))),
named *1.1 above. We will try to prove it by induction. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP FN) (p FN I))
(IMPLIES (AND (NOT (ZEROP FN)) (p (SUB1 FN) I))
(p FN I))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT FN) decreases according to the well-founded
relation LESSP in each induction step of the scheme. The above induction
scheme leads to two new conjectures:
Case 2. (IMPLIES (AND (ZEROP FN) (NUMBERP FN))
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))),
which simplifies, opening up the functions ZEROP, NUMBERP, EQUAL, and MAX1,
to the conjecture:
(IMPLIES (EQUAL FN 0)
(NOT (LESSP (MAX2 0 I) (PR-APPLY 0 I)))).
However this again simplifies, using linear arithmetic and rewriting with
MAX2-GTE, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP FN))
(NOT (LESSP (MAX1 (SUB1 FN) I)
(PR-APPLY (SUB1 FN) I)))
(NUMBERP FN))
(NOT (LESSP (MAX1 FN I) (PR-APPLY FN I)))).
This simplifies, expanding ZEROP, MAX1, and MAX, to the following three new
conjectures:
Case 1.3.
(IMPLIES (AND (NOT (EQUAL FN 0))
(NOT (LESSP (MAX1 (SUB1 FN) I)
(PR-APPLY (SUB1 FN) I)))
(NUMBERP FN)
(NOT (LESSP (MAX2 FN I)
(MAX1 (SUB1 FN) I)))
(NUMBERP (MAX2 FN I)))
(NOT (LESSP (MAX2 FN I) (PR-APPLY FN I)))).
But this again simplifies, using linear arithmetic and rewriting with
MAX2-GTE, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL FN 0))
(NOT (LESSP (MAX1 (SUB1 FN) I)
(PR-APPLY (SUB1 FN) I)))
(NUMBERP FN)
(NOT (LESSP (MAX2 FN I)
(MAX1 (SUB1 FN) I)))
(NOT (NUMBERP (MAX2 FN I))))
(NOT (LESSP 0 (PR-APPLY FN I)))).
But this again simplifies, using linear arithmetic and rewriting with
MAX2-GTE, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL FN 0))
(NOT (LESSP (MAX1 (SUB1 FN) I)
(PR-APPLY (SUB1 FN) I)))
(NUMBERP FN)
(LESSP (MAX2 FN I)
(MAX1 (SUB1 FN) I)))
(NOT (LESSP (MAX1 (SUB1 FN) I)
(PR-APPLY FN I)))).
However this again simplifies, using linear arithmetic and applying
MAX2-GTE, to:
T.
That finishes the proof of *1.1, which, in turn, also finishes the proof
of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
MAX1-GTE1
(PROVE-LEMMA MAX1-GTE2
(REWRITE)
(IMPLIES (NUMBERP FN)
(NOT (LESSP (MAX1 (PLUS J FN) (PLUS J FN))
(PR-APPLY FN (PLUS J FN))))))
WARNING: Note that the proposed lemma MAX1-GTE2 is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
This formula simplifies, using linear arithmetic and applying the lemma
MAX1-GTE1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
MAX1-GTE2
(PROVE-LEMMA EXCEED-IS-BIGGER NIL
(IMPLIES (NUMBERP FN)
(LESSP (PR-APPLY FN (PLUS J (EXCEED-AT FN)))
(EXCEED (PLUS J (EXCEED-AT FN))))))
This formula can be simplified, using the abbreviations IMPLIES and EXCEED-AT,
to the new conjecture:
(IMPLIES (NUMBERP FN)
(LESSP (PR-APPLY FN (PLUS J FN))
(EXCEED (PLUS J FN)))),
which simplifies, applying SUB1-ADD1, and unfolding the functions EXCEED and
LESSP, to the new formula:
(IMPLIES (AND (NUMBERP FN)
(NOT (EQUAL (PR-APPLY FN (PLUS J FN)) 0)))
(LESSP (SUB1 (PR-APPLY FN (PLUS J FN)))
(MAX1 (PLUS J FN) (PLUS J FN)))),
which again simplifies, using linear arithmetic and applying the lemma
MAX1-GTE2, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EXCEED-IS-BIGGER