(NOTE-LIB "fortran" T)
Loading ./fortran-vcg/fortran.lib
Finished loading ./fortran-vcg/fortran.lib
Loading ./fortran-vcg/fortran.o
Finished loading ./fortran-vcg/fortran.o
(#./fortran-vcg/fortran.lib #./fortran-vcg/fortran)
(ADD-AXIOM FORTRAN NIL T)
[ 0.0 0.0 0.0 ]
FORTRAN
(DCL A$0 NIL)
[ 0.0 0.0 0.0 ]
A$0
(DCL BOOLE$0 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$0
(DCL BOOLE$1 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$1
(DCL BOOLE$2 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$2
(DCL BOOLE$3 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$3
(DCL BOOLE$4 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$4
(DCL BOOLE$5 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$5
(DCL BOOLE$6 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$6
(DCL BOOLE$7 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$7
(DCL BOOLE$8 NIL)
[ 0.0 0.0 0.0 ]
BOOLE$8
(DCL CAND$0 NIL)
[ 0.0 0.0 0.0 ]
CAND$0
(DCL CAND$1 NIL)
[ 0.0 0.0 0.0 ]
CAND$1
(DCL CAND$2 NIL)
[ 0.0 0.0 0.0 ]
CAND$2
(DCL CAND$3 NIL)
[ 0.0 0.0 0.0 ]
CAND$3
(DCL CAND$4 NIL)
[ 0.0 0.0 0.0 ]
CAND$4
(DCL CAND$5 NIL)
[ 0.0 0.0 0.0 ]
CAND$5
(DCL CAND$6 NIL)
[ 0.0 0.0 0.0 ]
CAND$6
(DCL CAND$7 NIL)
[ 0.0 0.0 0.0 ]
CAND$7
(DCL CAND$8 NIL)
[ 0.0 0.0 0.0 ]
CAND$8
(DCL I$0 NIL)
[ 0.0 0.0 0.0 ]
I$0
(DCL I$1 NIL)
[ 0.0 0.0 0.0 ]
I$1
(DCL I$2 NIL)
[ 0.0 0.0 0.0 ]
I$2
(DCL I$3 NIL)
[ 0.0 0.0 0.0 ]
I$3
(DCL I$4 NIL)
[ 0.0 0.0 0.0 ]
I$4
(DCL I$5 NIL)
[ 0.0 0.0 0.0 ]
I$5
(DCL I$6 NIL)
[ 0.0 0.0 0.0 ]
I$6
(DCL I$7 NIL)
[ 0.0 0.0 0.0 ]
I$7
(DCL I$8 NIL)
[ 0.0 0.0 0.0 ]
I$8
(DCL K$1 NIL)
[ 0.0 0.0 0.0 ]
K$1
(DCL K$2 NIL)
[ 0.0 0.0 0.0 ]
K$2
(DCL K$3 NIL)
[ 0.0 0.0 0.0 ]
K$3
(DCL K$4 NIL)
[ 0.0 0.0 0.0 ]
K$4
(DCL K$5 NIL)
[ 0.0 0.0 0.0 ]
K$5
(DCL K$6 NIL)
[ 0.0 0.0 0.0 ]
K$6
(DCL K$7 NIL)
[ 0.0 0.0 0.0 ]
K$7
(DCL K$8 NIL)
[ 0.0 0.0 0.0 ]
K$8
(DCL N$0 NIL)
[ 0.0 0.0 0.0 ]
N$0
(DEFN CNT
(X A I N)
(IF (OR (ZEROP N) (LESSP N I))
0
(IF (ZEQP X (ELT1 A N))
(ADD1 (CNT X A I (SUB1 N)))
(CNT X A I (SUB1 N)))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of ZEQP,
ZNORMALIZE, OR, and ZEROP can be used to prove that the measure (COUNT N)
decreases according to the well-founded relation LESSP in each recursive call.
Hence, CNT is accepted under the principle of definition. Note that
(NUMBERP (CNT X A I N)) is a theorem.
[ 0.0 0.0 0.0 ]
CNT
(ADD-AXIOM INPUT-CONDITIONS
(REWRITE)
(IMPLIES (AND (LESSP '0 J)
(AND (NOT (LESSP (N$0) J))
(NOT (NEGATIVEP (ELT1 A J)))))
(NUMBERP (ELT1 A J))))
[ 0.0 0.0 0.0 ]
INPUT-CONDITIONS
(DEFN GLOBAL-HYPS NIL
(AND (NOT (EQUAL (N$0) '0))
(AND (LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))))
From the definition we can conclude that:
(OR (FALSEP (GLOBAL-HYPS))
(TRUEP (GLOBAL-HYPS)))
is a theorem.
[ 0.0 0.0 0.0 ]
GLOBAL-HYPS
(PROVE-LEMMA PLUS-1
(REWRITE)
(EQUAL (PLUS 1 X) (ADD1 X)))
WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied
whenever the newly proposed PLUS-1 could!
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PLUS-1
(PROVE-LEMMA DIFFERENCE-0
(REWRITE)
(IMPLIES (NOT (LESSP X Y))
(EQUAL (DIFFERENCE Y X) 0)))
Name the conjecture *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest four 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 Y X))
(IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(OR (EQUAL X 0) (NOT (NUMBERP X))))
(p Y X))
(IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(p (SUB1 Y) (SUB1 X)))
(p Y X))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to show 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 leads to the following four new goals:
Case 4. (IMPLIES (AND (OR (EQUAL Y 0) (NOT (NUMBERP Y)))
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)).
This simplifies, expanding the definitions of NOT, OR, EQUAL, LESSP, and
DIFFERENCE, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(OR (EQUAL X 0) (NOT (NUMBERP X)))
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)).
This simplifies, unfolding NOT, OR, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(LESSP (SUB1 X) (SUB1 Y))
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)).
This simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP Y 1)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(LESSP (SUB1 X) (SUB1 Y))
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, opening up the definitions of 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 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which simplifies, using linear arithmetic, to three new conjectures:
Case 1.3.
(IMPLIES (AND (LESSP Y X)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 1.3.2.
(IMPLIES (AND (LESSP (SUB1 Y) (SUB1 X))
(LESSP Y X)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, unfolding the functions LESSP, NOT, OR,
DIFFERENCE, and EQUAL, to:
T.
Case 1.3.1.
(IMPLIES (AND (LESSP Y 1)
(LESSP Y X)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and
OR, to:
T.
Case 1.2.
(IMPLIES (AND (LESSP (SUB1 Y) (SUB1 X))
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, expanding the definitions of NOT, OR, LESSP,
DIFFERENCE, and EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (LESSP Y 1)
(NOT (OR (EQUAL Y 0) (NOT (NUMBERP Y))))
(NOT (OR (EQUAL X 0) (NOT (NUMBERP X))))
(EQUAL (DIFFERENCE (SUB1 Y) (SUB1 X))
0)
(NOT (LESSP X Y)))
(EQUAL (DIFFERENCE Y X) 0)),
which again simplifies, opening up the definitions of 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 DIFFERENCE-1
(REWRITE)
(EQUAL (DIFFERENCE X 1) (SUB1 X)))
This simplifies, using linear arithmetic, to:
(IMPLIES (LESSP X 1)
(EQUAL (DIFFERENCE X 1) (SUB1 X))).
However this again simplifies, using linear arithmetic and applying
DIFFERENCE-0, to:
(IMPLIES (LESSP X 1)
(EQUAL 0 (SUB1 X))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 Z) to eliminate (SUB1 X). We
rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We would thus like to prove the following three
new conjectures:
Case 3. (IMPLIES (AND (EQUAL X 0) (LESSP X 1))
(EQUAL 0 (SUB1 X))).
But this further simplifies, unfolding the functions LESSP, SUB1, and EQUAL,
to:
T.
Case 2. (IMPLIES (AND (NOT (NUMBERP X)) (LESSP X 1))
(EQUAL 0 (SUB1 X))),
which further simplifies, rewriting with SUB1-NNUMBERP, and expanding the
definitions of NUMBERP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NOT (EQUAL (ADD1 Z) 0))
(LESSP (ADD1 Z) 1))
(EQUAL 0 Z)).
This further simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DIFFERENCE-1
(PROVE-LEMMA LESSP-X-1
(REWRITE)
(EQUAL (LESSP X 1) (ZEROP X)))
This simplifies, rewriting with EQUAL-LESSP, and unfolding ZEROP, to the
following three new conjectures:
Case 3. (IMPLIES (NOT (LESSP X 1))
(NUMBERP X)).
However this again simplifies, expanding the definitions of NUMBERP, EQUAL,
and LESSP, to:
T.
Case 2. (IMPLIES (NOT (LESSP X 1))
(NOT (EQUAL X 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP X 1) (NOT (EQUAL X 0)))
(NOT (NUMBERP X))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-X-1
(PROVE-LEMMA LESSP-REMAINDER2
(REWRITE GENERALIZE)
(EQUAL (LESSP (REMAINDER X Y) Y)
(NOT (ZEROP Y))))
This conjecture simplifies, applying EQUAL-LESSP, and unfolding the functions
ZEROP and NOT, to three new goals:
Case 3. (IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))),
which we will name *1.
Case 2. (IMPLIES (LESSP (REMAINDER X Y) Y)
(NUMBERP Y)).
This again simplifies, expanding REMAINDER and LESSP, to:
T.
Case 1. (IMPLIES (LESSP (REMAINDER X Y) Y)
(NOT (EQUAL Y 0))),
which again simplifies, using linear arithmetic, to:
T.
So let us turn our attention to:
(IMPLIES (AND (NOT (LESSP (REMAINDER X Y) Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))),
which we named *1 above. We will try to prove it by induction. There are two
plausible inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP Y) (p Y X))
(IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
(p Y X))
(IMPLIES (AND (NOT (ZEROP Y))
(NOT (LESSP X Y))
(p Y (DIFFERENCE X Y)))
(p Y X))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, 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 leads to three new goals:
Case 3. (IMPLIES (AND (ZEROP Y)
(NOT (LESSP (REMAINDER X Y) Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))),
which simplifies, opening up ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP Y))
(LESSP X Y)
(NOT (LESSP (REMAINDER X Y) Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))),
which simplifies, unfolding the functions ZEROP and REMAINDER, to:
(IMPLIES (AND (LESSP X Y)
(NOT (NUMBERP X))
(NOT (LESSP 0 Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))).
However this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(NOT (LESSP X Y))
(LESSP (REMAINDER (DIFFERENCE X Y) Y)
Y)
(NOT (LESSP (REMAINDER X Y) Y))
(NOT (EQUAL Y 0)))
(NOT (NUMBERP Y))),
which simplifies, expanding the functions ZEROP and REMAINDER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-REMAINDER2
(PROVE-LEMMA REMAINDER-QUOTIENT-ELIM
(ELIM)
(IMPLIES (AND (NOT (ZEROP Y)) (NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)))
This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and
IMPLIES, to:
(IMPLIES (AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)),
which we will name *1.
We will appeal to induction. The recursive terms in the conjecture
suggest three inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (ZEROP Y) (p X Y))
(IMPLIES (AND (NOT (ZEROP Y)) (LESSP X Y))
(p X Y))
(IMPLIES (AND (NOT (ZEROP Y))
(NOT (LESSP X Y))
(p (DIFFERENCE X Y) Y))
(p X Y))).
Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the
definition of ZEROP can be used to 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 three new goals:
Case 3. (IMPLIES (AND (ZEROP Y)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)),
which simplifies, opening up the definition of ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP Y))
(LESSP X Y)
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)),
which simplifies, rewriting with COMMUTATIVITY-OF-TIMES and
COMMUTATIVITY-OF-PLUS, and unfolding ZEROP, REMAINDER, QUOTIENT, EQUAL,
TIMES, and PLUS, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(NOT (LESSP X Y))
(EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
(TIMES Y
(QUOTIENT (DIFFERENCE X Y) Y)))
(DIFFERENCE X Y))
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (PLUS (REMAINDER X Y)
(TIMES Y (QUOTIENT X Y)))
X)).
This simplifies, rewriting with TIMES-ADD1 and COMMUTATIVITY2-OF-PLUS, and
opening up the definitions of ZEROP, REMAINDER, and QUOTIENT, to the goal:
(IMPLIES (AND (NOT (LESSP X Y))
(EQUAL (PLUS (REMAINDER (DIFFERENCE X Y) Y)
(TIMES Y
(QUOTIENT (DIFFERENCE X Y) Y)))
(DIFFERENCE X Y))
(NOT (EQUAL Y 0))
(NUMBERP Y)
(NUMBERP X))
(EQUAL (PLUS Y (DIFFERENCE X Y)) X)).
However this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
REMAINDER-QUOTIENT-ELIM
(PROVE-LEMMA QUOTIENT-BY-2-BOUND
(REWRITE)
(NOT (LESSP X (QUOTIENT X 2))))
WARNING: Note that the proposed lemma QUOTIENT-BY-2-BOUND is to be stored as
zero type prescription rules, zero compound recognizer rules, one linear rule,
and zero replacement rules.
.
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace X by
(PLUS V (TIMES 2 Z)) to eliminate (QUOTIENT X 2) and (REMAINDER X 2). We
employ LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was introduced
to constrain the new variables. We must thus prove four new formulas:
Case 4. (IMPLIES (NOT (NUMBERP X))
(NOT (LESSP X (QUOTIENT X 2)))),
which simplifies, expanding the definitions of LESSP, NUMBERP, EQUAL, and
QUOTIENT, to:
T.
Case 3. (IMPLIES (EQUAL 2 0)
(NOT (LESSP X (QUOTIENT X 2)))),
which simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (NOT (NUMBERP 2))
(NOT (LESSP X (QUOTIENT X 2)))),
which simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NUMBERP Z)
(NUMBERP V)
(EQUAL (LESSP V 2) (NOT (ZEROP 2)))
(NOT (EQUAL 2 0)))
(NOT (LESSP (PLUS V (TIMES 2 Z)) Z))).
However this simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
QUOTIENT-BY-2-BOUND
(PROVE-LEMMA LESSP-QUOTIENT-REWRITE
(REWRITE)
(EQUAL (LESSP (QUOTIENT N 2) M)
(LESSP N (PLUS M M))))
This formula simplifies, appealing to the lemma EQUAL-LESSP, to the following
two new goals:
Case 2. (IMPLIES (NOT (LESSP (QUOTIENT N 2) M))
(NOT (LESSP N (PLUS M M)))).
Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace N by
(PLUS Z (TIMES 2 X)) to eliminate (QUOTIENT N 2) and (REMAINDER N 2). We
use LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was
introduced to constrain the new variables. This generates four new formulas:
Case 2.4.
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (LESSP (QUOTIENT N 2) M)))
(NOT (LESSP N (PLUS M M)))),
which further simplifies, applying PLUS-NON-NUMBERP, and unfolding the
definitions of LESSP, NUMBERP, EQUAL, QUOTIENT, and PLUS, to:
T.
Case 2.3.
(IMPLIES (AND (EQUAL 2 0)
(NOT (LESSP (QUOTIENT N 2) M)))
(NOT (LESSP N (PLUS M M)))).
This further simplifies, using linear arithmetic, to:
T.
Case 2.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(NOT (LESSP (QUOTIENT N 2) M)))
(NOT (LESSP N (PLUS M M)))),
which further simplifies, clearly, to:
T.
Case 2.1.
(IMPLIES (AND (NUMBERP X)
(NUMBERP Z)
(EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
(NOT (EQUAL 2 0))
(NOT (LESSP X M)))
(NOT (LESSP (PLUS Z (TIMES 2 X))
(PLUS M M)))).
But this further simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (LESSP (QUOTIENT N 2) M)
(LESSP N (PLUS M M))).
Applying the lemma REMAINDER-QUOTIENT-ELIM, replace N by
(PLUS Z (TIMES 2 X)) to eliminate (QUOTIENT N 2) and (REMAINDER N 2). We
employ LESSP-REMAINDER2, the type restriction lemma noted when QUOTIENT was
introduced, and the type restriction lemma noted when REMAINDER was
introduced to restrict the new variables. We thus obtain the following four
new goals:
Case 1.4.
(IMPLIES (AND (NOT (NUMBERP N))
(LESSP (QUOTIENT N 2) M))
(LESSP N (PLUS M M))).
But this further simplifies, opening up the functions LESSP, NUMBERP,
EQUAL, and QUOTIENT, to the goal:
(IMPLIES (AND (NOT (NUMBERP N))
(NOT (EQUAL M 0))
(NUMBERP M))
(NOT (EQUAL (PLUS M M) 0))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL 2 0)
(LESSP (QUOTIENT N 2) M))
(LESSP N (PLUS M M))),
which further simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (NUMBERP 2))
(LESSP (QUOTIENT N 2) M))
(LESSP N (PLUS M M))),
which further simplifies, obviously, to:
T.
Case 1.1.
(IMPLIES (AND (NUMBERP X)
(NUMBERP Z)
(EQUAL (LESSP Z 2) (NOT (ZEROP 2)))
(NOT (EQUAL 2 0))
(LESSP X M))
(LESSP (PLUS Z (TIMES 2 X))
(PLUS M M))).
But this further simplifies, applying LESSP-X-1, and opening up the
definitions of SUB1, NUMBERP, EQUAL, LESSP, ZEROP, NOT, and PLUS, to the
following two new formulas:
Case 1.1.2.
(IMPLIES (AND (NUMBERP X)
(NUMBERP Z)
(EQUAL Z 0)
(LESSP X M))
(LESSP (TIMES 2 X) (PLUS M M))).
This again simplifies, using linear arithmetic, to:
T.
Case 1.1.1.
(IMPLIES (AND (NUMBERP X)
(NUMBERP Z)
(EQUAL (SUB1 Z) 0)
(LESSP X M))
(LESSP (PLUS Z (TIMES 2 X))
(PLUS M M))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LESSP-QUOTIENT-REWRITE
(PROVE-LEMMA ZNORMALIZE-ZERO
(REWRITE)
(IMPLIES (NUMBERP X)
(EQUAL (EQUAL (ZNORMALIZE X) 0)
(EQUAL X 0))))
This formula simplifies, expanding ZNORMALIZE, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ZNORMALIZE-ZERO
(DISABLE ZNORMALIZE)
[ 0.0 0.0 0.0 ]
ZNORMALIZE-OFF
(PROVE-LEMMA CNT-BOUND
(REWRITE)
(NOT (LESSP N (CNT X A 1 N))))
WARNING: Note that the proposed lemma CNT-BOUND is to be stored as zero type
prescription rules, zero compound recognizer rules, one linear rule, and zero
replacement rules.
Give the conjecture the name *1.
Let us appeal to the induction principle. Two 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 (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N))))
(p N X A))
(IMPLIES (AND (NOT (OR (EQUAL (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N)))))
(OR (EQUAL N 0) (NOT (NUMBERP N))))
(p N X A))
(IMPLIES (AND (NOT (OR (EQUAL (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N)))))
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(p (SUB1 N) X A))
(p N X A))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates three new conjectures:
Case 3. (IMPLIES (OR (EQUAL (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N))))
(NOT (LESSP N (CNT X A 1 N)))),
which simplifies, applying LESSP-X-1, and opening up CNT, ZEQP, NOT, OR,
EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N)))))
(OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (LESSP N (CNT X A 1 N)))).
This simplifies, applying the lemma LESSP-X-1, and unfolding the functions
CNT, ZEQP, NOT, and OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL (CNT X A 1 N) 0)
(NOT (NUMBERP (CNT X A 1 N)))))
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (LESSP (SUB1 N)
(CNT X A 1 (SUB1 N)))))
(NOT (LESSP N (CNT X A 1 N)))).
This simplifies, rewriting with LESSP-X-1 and SUB1-ADD1, and opening up the
functions CNT, ZEQP, NOT, OR, and LESSP, to the conjecture:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A N))))
(NOT (EQUAL (CNT X A 1 (SUB1 N)) 0))
(NOT (LESSP (SUB1 N)
(CNT X A 1 (SUB1 N)))))
(NOT (LESSP N (CNT X A 1 (SUB1 N))))).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CNT-BOUND
(PROVE-LEMMA INPUT-DEFINEDNESS NIL
(IMPLIES (GLOBAL-HYPS) '*1*TRUE))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS and
IMPLIES, to:
T.
This simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-DEFINEDNESS
(ADD-AXIOM INPUT NIL T)
[ 0.0 0.0 0.0 ]
INPUT
(ADD-AXIOM ASSIGNMENT
(REWRITE)
(AND (EQUAL (BOOLE$1) (BOOLE$0))
(AND (EQUAL (CAND$1) (CAND$0))
(AND (EQUAL (I$1) (I$0))
(EQUAL (K$1) '0)))))
WARNING: Note that the proposed lemma ASSIGNMENT is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and
four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT
(ADD-AXIOM LOGICAL-IF-F NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F
(ADD-AXIOM ASSIGNMENT1
(REWRITE)
(AND (EQUAL (BOOLE$2) (BOOLE$1))
(AND (EQUAL (CAND$2) (CAND$1))
(AND (EQUAL (I$2) '1)
(EQUAL (K$2) (K$1))))))
WARNING: Note that the proposed lemma ASSIGNMENT1 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT1
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(ADD-AXIOM EFFECTS-OF-UNDEFINER
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(EQUAL (K$3) (K$2)))))
WARNING: Note that the proposed lemma EFFECTS-OF-UNDEFINER is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
[ 0.0 0.0 0.0 ]
EFFECTS-OF-UNDEFINER
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(ADD-AXIOM ASSIGNMENT2
(REWRITE)
(AND (EQUAL (BOOLE$4) '*1*FALSE)
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) (K$3))))))
WARNING: Note that the proposed lemma ASSIGNMENT2 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT2
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZEQP (K$3) '0)
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))
(AND (OR (EQUAL (BOOLE$4) '*1*TRUE)
(EQUAL (BOOLE$4) '*1*FALSE))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$4))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$4) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, AND,
IMPLIES, ASSIGNMENT2, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER,
and ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0))
(NOT F)
(ZLESSP (N$0) 1)
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$0))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$0) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))),
which simplifies, rewriting with LESSP-X-1, and unfolding ZNORMALIZE, EQUAL,
NEGATIVEP, and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F1
(ADD-AXIOM ASSIGNMENT2
(REWRITE)
(AND (EQUAL (BOOLE$4) '*1*TRUE)
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) (K$3))))))
WARNING: Note that the proposed lemma ASSIGNMENT2 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT2
(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT NIL
(IMPLIES (AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))
(AND (NOT (ZEQP '2 '0))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) '2)))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, NOT, AND,
IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER, and ZEQP,
to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT F)
(ZLESSP (N$0) 1)
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) 2)))),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZQUOTIENT
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS)))))
(AND (OR (EQUAL (BOOLE$4) '*1*TRUE)
(EQUAL (BOOLE$4) '*1*FALSE))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$4))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$4) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, ZEQP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER, ASSIGNMENT2,
and ZGREATERP, to the formula:
(IMPLIES (AND (ZLESSP (ZQUOTIENT (N$0) 2) 0)
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT F)
(ZLESSP (N$0) 1)
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$0))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$0) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F2 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F2
(ADD-AXIOM ASSIGNMENT3
(REWRITE)
(AND (EQUAL (BOOLE$5) (BOOLE$4))
(AND (EQUAL (CAND$5) (CAND$4))
(AND (EQUAL (I$5) (I$4))
(EQUAL (K$5) '0)))))
WARNING: Note that the proposed lemma ASSIGNMENT3 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT3
(ADD-AXIOM LOGICAL-IF-F3 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F3
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$6) (BOOLE$5))
(AND (EQUAL (CAND$6) (CAND$5))
(AND (EQUAL (I$6) '1)
(EQUAL (K$6) (K$5))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(ADD-AXIOM EFFECTS-OF-UNDEFINER1
(REWRITE)
(AND (EQUAL (BOOLE$7) (BOOLE$6))
(AND (EQUAL (CAND$7) (CAND$6))
(EQUAL (K$7) (K$6)))))
WARNING: Note that the proposed lemma EFFECTS-OF-UNDEFINER1 is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
[ 0.0 0.0 0.0 ]
EFFECTS-OF-UNDEFINER1
(ADD-AXIOM ASSIGNMENT5
(REWRITE)
(AND (EQUAL (BOOLE$8) '*1*FALSE)
(AND (EQUAL (CAND$8) (CAND$7))
(AND (EQUAL (I$8) (I$7))
(EQUAL (K$8) (K$7))))))
WARNING: Note that the proposed lemma ASSIGNMENT5 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT5
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (I$6)
(AND (ZGREATERP (I$6) (N$0))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS)))))))
(AND (OR (EQUAL (BOOLE$8) '*1*TRUE)
(EQUAL (BOOLE$8) '*1*FALSE))
(IF (BOOLE$8)
(AND (ZNUMBERP (CAND$8))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$8) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, ASSIGNMENT3, EFFECTS-OF-UNDEFINER1, ASSIGNMENT5, ZEQP,
ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ZGREATERP, and
ASSIGNMENT4, to:
(IMPLIES (AND (NOT F)
(ZLESSP (N$0) 1)
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) 0))
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (OR (EQUAL (BOOLE$8) T)
(EQUAL (BOOLE$8) F))
(IF (BOOLE$8)
(AND (ZNUMBERP (CAND$0))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$0) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))).
This simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F4 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F4
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))))
(AND (LESSP '0 (I$6))
(NOT (LESSP (N$0) (I$6))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, ZEQP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER, ASSIGNMENT2,
ASSIGNMENT4, and ZGREATERP, to:
T.
This simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A
(PROVE-LEMMA DEFINEDNESS NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))))
(ZNUMBERP (CAND$6))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
NOT, AND, IMPLIES, ASSIGNMENT3, ZEQP, ASSIGNMENT, ASSIGNMENT1,
EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ASSIGNMENT4, and ZGREATERP, to:
T,
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS
(PROVE-LEMMA DEFINEDNESS1 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))))
(ZNUMBERP (ELT1 (A$0) (I$6)))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
NOT, AND, IMPLIES, ZEQP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER,
ASSIGNMENT2, ASSIGNMENT4, and ZGREATERP, to:
T,
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS1
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA PHASE2-INVRT NIL
(IMPLIES
(AND (ZNEQP (CAND$6) (ELT1 (A$0) (I$6)))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS)))))))
(AND
(AND
(NUMBERP (I$6))
(AND
(NOT (EQUAL (I$6) '0))
(AND
(EQUAL (BOOLE$6) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$6)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$6)))
(NUMBERP (CAND$6)))
(AND (IMPLIES (ZNEQP X (CAND$6))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$6) (A$0) '1 (I$6)))))
(EQUAL (K$6)
(CNT (CAND$6) (A$0) '1 (I$6))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$6))
'NIL)
(CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
ZNEQP, AND, IMPLIES, DIFFERENCE-1, ZEQP, ZGREATERP, ASSIGNMENT, ASSIGNMENT1,
EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ASSIGNMENT3, and ASSIGNMENT4, to:
T.
This simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE2-INVRT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F5 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F5
(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS)))))))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$6) '1))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, ZNEQP,
NOT, AND, IMPLIES, ZEQP, ZGREATERP, ASSIGNMENT, ASSIGNMENT1,
EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ASSIGNMENT3, and ASSIGNMENT4, to:
T.
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS
(ADD-AXIOM ASSIGNMENT5
(REWRITE)
(AND (EQUAL (BOOLE$7) (BOOLE$6))
(AND (EQUAL (CAND$7) (CAND$6))
(AND (EQUAL (I$7) (I$6))
(EQUAL (K$7) (ZPLUS (K$6) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT5 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT5
(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT1 NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS)))))))
(AND (NOT (ZEQP '2 '0))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) '2)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, ZNEQP,
NOT, AND, IMPLIES, ZEQP, ZGREATERP, ASSIGNMENT, ASSIGNMENT1,
EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ASSIGNMENT3, and ASSIGNMENT4, to:
T.
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZQUOTIENT1
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZGREATERP (K$7)
(ZQUOTIENT (N$0) '2))
(AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))))))
(AND (OR (EQUAL (BOOLE$7) '*1*TRUE)
(EQUAL (BOOLE$7) '*1*FALSE))
(IF (BOOLE$7)
(AND (ZNUMBERP (CAND$7))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$7) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, ZNEQP,
NOT, AND, IMPLIES, ZEQP, ASSIGNMENT, ASSIGNMENT1, EFFECTS-OF-UNDEFINER,
ASSIGNMENT2, ASSIGNMENT3, ASSIGNMENT4, ASSIGNMENT5, and ZGREATERP, to the new
goal:
T,
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F6 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F6
(PROVE-LEMMA PHASE2-INVRT NIL
(IMPLIES
(AND (NOT (ZGREATERP (K$7)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(GLOBAL-HYPS))))))))
(AND
(AND
(NUMBERP (I$7))
(AND
(NOT (EQUAL (I$7) '0))
(AND
(EQUAL (BOOLE$7) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$7)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$7)))
(NUMBERP (CAND$7)))
(AND (IMPLIES (ZNEQP X (CAND$7))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$7) (A$0) '1 (I$7)))))
(EQUAL (K$7)
(CNT (CAND$7) (A$0) '1 (I$7))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$7))
'NIL)
(CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
'NIL)))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, ZNEQP,
NOT, AND, IMPLIES, DIFFERENCE-1, ZEQP, ASSIGNMENT, ASSIGNMENT1,
EFFECTS-OF-UNDEFINER, ASSIGNMENT2, ASSIGNMENT3, ASSIGNMENT4, ASSIGNMENT5, and
ZGREATERP, to:
T,
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE2-INVRT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F1
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A NIL
(IMPLIES (AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(AND (LESSP '0 (I$2))
(NOT (LESSP (N$0) (I$2))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, NOT, AND,
IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (LESSP 0 1)
(NOT (LESSP (N$0) 1)))),
which simplifies, applying LESSP-X-1 and SUB1-ADD1, and unfolding the
functions ZNORMALIZE, EQUAL, NEGATIVEP, ZLESSP, LESSP, NOT, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A
(PROVE-LEMMA DEFINEDNESS NIL
(IMPLIES (AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(ZNUMBERP (ELT1 (A$0) (I$2)))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP,
to the formula:
(IMPLIES (AND (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NOT (NEGATIVEP (ELT1 (A$0) 1))))
(NUMBERP (ELT1 (A$0) 1))).
This simplifies, using linear arithmetic, rewriting with LESSP-X-1, SUB1-ADD1,
and INPUT-CONDITIONS, and expanding the functions ZNORMALIZE, EQUAL, NEGATIVEP,
ZLESSP, and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS
(ADD-AXIOM ASSIGNMENT2
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (ELT1 (A$0) (I$2)))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3) (K$2))))))
WARNING: Note that the proposed lemma ASSIGNMENT2 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT2
(ADD-AXIOM ASSIGNMENT3
(REWRITE)
(AND (EQUAL (BOOLE$4) (BOOLE$3))
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) '1)))))
WARNING: Note that the proposed lemma ASSIGNMENT3 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT3
(PROVE-LEMMA PHASE1-INVRT NIL
(IMPLIES
(AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(AND
(AND
(NUMBERP (I$4))
(AND
(NOT (EQUAL (I$4) '0))
(AND
(NUMBERP (K$4))
(AND
(NOT (LESSP (I$4) (K$4)))
(AND
(NOT (LESSP (N$0) (I$4)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$4)))
(NUMBERP (CAND$4)))
(AND
(NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
(K$4)))
(AND
(IMPLIES (ZEQP X (CAND$4))
(NOT (LESSP (PLUS (I$4) (K$4))
(TIMES '2 (CNT X (A$0) '1 (I$4))))))
(IMPLIES
(ZNEQP X (CAND$4))
(NOT (LESSP (I$4)
(PLUS (K$4)
(TIMES '2
(CNT X (A$0) '1 (I$4)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$4))))
'NIL)
(CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, DIFFERENCE-1, PLUS-1, ASSIGNMENT2, ASSIGNMENT3, ZGREATERP,
ASSIGNMENT, ASSIGNMENT1, and ZEQP, to:
(IMPLIES
(AND (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (AND (NUMBERP 1)
(NOT (EQUAL 1 0))
(NUMBERP 1)
(NOT (LESSP 1 1))
(NOT (LESSP (N$0) 1))
(IMPLIES (NOT (NEGATIVEP (ELT1 (A$0) 1)))
(NUMBERP (ELT1 (A$0) 1)))
(NOT (LESSP (CNT (ELT1 (A$0) 1) (A$0) 1 1)
1))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP 2
(TIMES 2 (CNT X (A$0) 1 1)))))
(IMPLIES (ZNEQP X (ELT1 (A$0) 1))
(NOT (LESSP 1
(ADD1 (TIMES 2 (CNT X (A$0) 1 1)))))))
(LEX (LIST (ADD1 (PLUS (N$0) (SUB1 (ADD1 (N$0))))))
(LIST (ADD1 (ADD1 (PLUS (N$0) (N$0)))))))).
This simplifies, applying LESSP-X-1, SUB1-ADD1, EQUAL-TIMES-0, ADD1-EQUAL, and
CAR-CONS, and unfolding the functions ZNORMALIZE, EQUAL, NEGATIVEP, ZLESSP,
LESSP, NUMBERP, NOT, IMPLIES, SUB1, ZEQP, CNT, ADD1, ZNEQP, AND, and LEX, to
three new goals:
Case 3. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NOT (NEGATIVEP (ELT1 (A$0) 1))))
(NUMBERP (ELT1 (A$0) 1))),
which again simplifies, using linear arithmetic, applying INPUT-CONDITIONS,
and expanding LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP 2 (TIMES 2 1)))).
But this again simplifies, unfolding the definitions of TIMES and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NOT (EQUAL (PLUS (N$0) (N$0)) 0)))
(LESSP (SUB1 (PLUS (N$0) (N$0)))
(PLUS (N$0) (N$0)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE1-INVRT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F2 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F2
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(AND (LESSP '0 (I$2))
(NOT (LESSP (N$0) (I$2))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, NOT, AND,
IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP, to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (LESSP 0 1)
(NOT (LESSP (N$0) 1)))),
which simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A
(PROVE-LEMMA DEFINEDNESS NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(ZNUMBERP (CAND$2))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP,
to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NOT (NEGATIVEP (CAND$0))))
(NUMBERP (CAND$0))).
This simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS
(PROVE-LEMMA DEFINEDNESS1 NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS)))
(ZNUMBERP (ELT1 (A$0) (I$2)))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP,
to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NOT (NEGATIVEP (ELT1 (A$0) 1))))
(NUMBERP (ELT1 (A$0) 1))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS1
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
(IMPLIES (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS))))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$2) '1))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, NOT, AND,
IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$0))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS 0 1))),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS
(ADD-AXIOM ASSIGNMENT2
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3) (ZPLUS (K$2) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT2 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT2
(PROVE-LEMMA PHASE1-INVRT NIL
(IMPLIES
(AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (K$3))
(AND
(NOT (LESSP (I$3) (K$3)))
(AND
(NOT (LESSP (N$0) (I$3)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$3)))
(NUMBERP (CAND$3)))
(AND
(NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
(K$3)))
(AND
(IMPLIES (ZEQP X (CAND$3))
(NOT (LESSP (PLUS (I$3) (K$3))
(TIMES '2 (CNT X (A$0) '1 (I$3))))))
(IMPLIES
(ZNEQP X (CAND$3))
(NOT (LESSP (I$3)
(PLUS (K$3)
(TIMES '2
(CNT X (A$0) '1 (I$3)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$3))))
'NIL)
(CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, DIFFERENCE-1, PLUS-1, ASSIGNMENT2, ZGREATERP, ASSIGNMENT,
ASSIGNMENT1, and ZEQP, to the formula:
(IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$0))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (AND (NUMBERP 1)
(NOT (EQUAL 1 0))
(NUMBERP (ZPLUS 0 1))
(NOT (LESSP 1 (ZPLUS 0 1)))
(NOT (LESSP (N$0) 1))
(IMPLIES (NOT (NEGATIVEP (CAND$0)))
(NUMBERP (CAND$0)))
(NOT (LESSP (CNT (CAND$0) (A$0) 1 1)
(ZPLUS 0 1)))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$0)))
(NOT (LESSP (ADD1 (ZPLUS 0 1))
(TIMES 2 (CNT X (A$0) 1 1)))))
(IMPLIES (ZNEQP X (CAND$0))
(NOT (LESSP 1
(PLUS (ZPLUS 0 1)
(TIMES 2 (CNT X (A$0) 1 1)))))))
(LEX (LIST (ADD1 (PLUS (N$0) (SUB1 (ADD1 (N$0))))))
(LIST (ADD1 (ADD1 (PLUS (N$0) (N$0)))))))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE1-INVRT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F3 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F3
(PROVE-LEMMA INPUT-COND-OF-ZDIFFERENCE NIL
(IMPLIES (AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS))))
(EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE (K$2) '1))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, NOT, AND,
IMPLIES, ZGREATERP, ASSIGNMENT, ASSIGNMENT1, and ZEQP, to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$0))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE 0 1))),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZDIFFERENCE
(ADD-AXIOM ASSIGNMENT2
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3)
(ZDIFFERENCE (K$2) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT2 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT2
(PROVE-LEMMA PHASE1-INVRT NIL
(IMPLIES
(AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(GLOBAL-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (K$3))
(AND
(NOT (LESSP (I$3) (K$3)))
(AND
(NOT (LESSP (N$0) (I$3)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$3)))
(NUMBERP (CAND$3)))
(AND
(NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
(K$3)))
(AND
(IMPLIES (ZEQP X (CAND$3))
(NOT (LESSP (PLUS (I$3) (K$3))
(TIMES '2 (CNT X (A$0) '1 (I$3))))))
(IMPLIES
(ZNEQP X (CAND$3))
(NOT (LESSP (I$3)
(PLUS (K$3)
(TIMES '2
(CNT X (A$0) '1 (I$3)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$3))))
'NIL)
(CONS (ADD1 (ADD1 (PLUS (N$0) (N$0))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS, NOT,
AND, IMPLIES, DIFFERENCE-1, PLUS-1, ASSIGNMENT2, ZGREATERP, ASSIGNMENT,
ASSIGNMENT1, and ZEQP, to the conjecture:
(IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$0))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (EQUAL (ZNORMALIZE 0) (ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0)))
(AND (AND (NUMBERP 1)
(NOT (EQUAL 1 0))
(NUMBERP (ZDIFFERENCE 0 1))
(NOT (LESSP 1 (ZDIFFERENCE 0 1)))
(NOT (LESSP (N$0) 1))
(IMPLIES (NOT (NEGATIVEP (CAND$0)))
(NUMBERP (CAND$0)))
(NOT (LESSP (CNT (CAND$0) (A$0) 1 1)
(ZDIFFERENCE 0 1)))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$0)))
(NOT (LESSP (ADD1 (ZDIFFERENCE 0 1))
(TIMES 2 (CNT X (A$0) 1 1)))))
(IMPLIES (ZNEQP X (CAND$0))
(NOT (LESSP 1
(PLUS (ZDIFFERENCE 0 1)
(TIMES 2 (CNT X (A$0) 1 1)))))))
(LEX (LIST (ADD1 (PLUS (N$0) (SUB1 (ADD1 (N$0))))))
(LIST (ADD1 (ADD1 (PLUS (N$0) (N$0)))))))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE1-INVRT
(UBT INPUT)
INPUT
(ADD-AXIOM PATHS-FROM-PHASE1-INVRT
(REWRITE)
(AND (IMPLIES (ZEQP X (CAND$1))
(NOT (LESSP (PLUS (I$1) (K$1))
(TIMES '2 (CNT X (A$0) '1 (I$1))))))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (I$1)
(PLUS (K$1)
(TIMES '2
(CNT X (A$0) '1 (I$1)))))))))
WARNING: Note that the proposed lemma PATHS-FROM-PHASE1-INVRT is to be stored
as zero type prescription rules, zero compound recognizer rules, two linear
rules, and zero replacement rules.
[ 0.0 0.0 0.0 ]
PATHS-FROM-PHASE1-INVRT
(DEFN PATH-HYPS NIL
(AND (GLOBAL-HYPS)
(AND (NUMBERP (I$1))
(AND (NOT (EQUAL (I$1) '0))
(AND (NUMBERP (K$1))
(AND (NOT (LESSP (I$1) (K$1)))
(AND (NOT (LESSP (N$0) (I$1)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (CNT (CAND$1) (A$0) '1 (I$1))
(K$1)))))))))))
From the definition we can conclude that:
(OR (FALSEP (PATH-HYPS))
(TRUEP (PATH-HYPS)))
is a theorem.
[ 0.0 0.0 0.0 ]
PATH-HYPS
(PROVE-LEMMA DEFINEDNESS2 NIL
(IMPLIES (PATH-HYPS)
(ZNUMBERP (I$1))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to:
T,
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS2
(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
(IMPLIES (PATH-HYPS)
(EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) '1))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to the conjecture:
(IMPLIES (AND (NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) 1))).
This simplifies, applying SUB1-ADD1, COMMUTATIVITY-OF-PLUS, and PLUS-1, and
unfolding the definitions of LESSP, NEGATIVEP, ZPLUS, ZLESSP, and
EXPRESSIBLE-ZNUMBERP, to two new goals:
Case 2. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS
(ADD-AXIOM ASSIGNMENT3
(REWRITE)
(AND (EQUAL (BOOLE$2) (BOOLE$1))
(AND (EQUAL (CAND$2) (CAND$1))
(AND (EQUAL (I$2) (ZPLUS (I$1) '1))
(EQUAL (K$2) (K$1))))))
WARNING: Note that the proposed lemma ASSIGNMENT3 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT3
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(ADD-AXIOM EFFECTS-OF-UNDEFINER
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(EQUAL (K$3) (K$2)))))
WARNING: Note that the proposed lemma EFFECTS-OF-UNDEFINER is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
[ 0.0 0.0 0.0 ]
EFFECTS-OF-UNDEFINER
(PROVE-LEMMA DEFINEDNESS3 NIL
(IMPLIES (AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))
(ZNUMBERP (K$3))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, AND, IMPLIES, EFFECTS-OF-UNDEFINER, ZGREATERP, and ASSIGNMENT3, to:
T,
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS3
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$4) '*1*FALSE)
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) (K$3))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA COMPOUND-INVRT
(REWRITE)
(IMPLIES (EQUAL (K$1) 0)
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1))))))
((USE (PATHS-FROM-PHASE1-INVRT))))
WARNING: Note that the proposed lemma COMPOUND-INVRT 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 NOT, IMPLIES, AND,
and ZEQP, to:
(IMPLIES
(AND (IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (LESSP (PLUS (I$1) (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (I$1)
(PLUS (K$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))))
(EQUAL (K$1) 0))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
This simplifies, appealing to the lemma COMMUTATIVITY-OF-PLUS, and unfolding
EQUAL, PLUS, SUB1, NUMBERP, TIMES, NOT, IMPLIES, ZEQP, ZNEQP, CNT, and LESSP,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
COMPOUND-INVRT
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZEQP (K$3) '0)
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))
(AND (OR (EQUAL (BOOLE$4) '*1*TRUE)
(EQUAL (BOOLE$4) '*1*FALSE))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$4))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$4) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
AND, IMPLIES, ASSIGNMENT4, ZGREATERP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER, and
ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))),
which simplifies, rewriting with ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS,
PLUS-1, SUB1-ADD1, and LESSP-QUOTIENT-REWRITE, and unfolding ZNORMALIZE,
NEGATIVEP, ZPLUS, LESSP, ZLESSP, NUMBERP, EQUAL, OR, NOT, and AND, to the
following two new formulas:
Case 2. (IMPLIES (AND (EQUAL (K$1) 0)
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1)))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
However this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(EQUAL (K$1) 0)
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1)))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic and rewriting with
COMPOUND-INVRT, to:
T.
Case 1. (IMPLIES (AND (EQUAL (K$1) 0)
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
But this again simplifies, using linear arithmetic, to the goal:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(EQUAL (K$1) 0)
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
This again simplifies, using linear arithmetic and rewriting with the lemma
COMPOUND-INVRT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F4 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F4
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$4) '*1*TRUE)
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) (K$3))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT NIL
(IMPLIES (AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))
(AND (NOT (ZEQP '2 '0))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) '2)))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER, and ZEQP, to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) 2)))),
which simplifies, rewriting with the lemmas ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and LESSP-QUOTIENT-REWRITE, and
expanding the functions ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, ZLESSP, EQUAL,
NOT, ZQUOTIENT, EXPRESSIBLE-ZNUMBERP, and AND, to four new conjectures:
Case 4. (IMPLIES
(AND (NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZQUOTIENT
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))))
(AND (OR (EQUAL (BOOLE$4) '*1*TRUE)
(EQUAL (BOOLE$4) '*1*FALSE))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$4))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$4) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ZEQP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER,
ASSIGNMENT4, and ZGREATERP, to the formula:
(IMPLIES (AND (ZLESSP (ZQUOTIENT (N$0) 2) (K$1))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))).
This simplifies, applying the lemmas LESSP-QUOTIENT-REWRITE, ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and unfolding the functions
NEGATIVEP, ZQUOTIENT, ZLESSP, ZNORMALIZE, ZPLUS, LESSP, OR, ZNUMBERP, and AND,
to the following two new formulas:
Case 2. (IMPLIES (AND (LESSP (N$0) (PLUS (K$1) (K$1)))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (I$1) (PLUS (K$1) (K$1)))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))).
This again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LESSP (N$0) (PLUS (K$1) (K$1)))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (I$1) (PLUS (K$1) (K$1)))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F5 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F5
(ADD-AXIOM ASSIGNMENT5
(REWRITE)
(AND (EQUAL (BOOLE$5) (BOOLE$4))
(AND (EQUAL (CAND$5) (CAND$4))
(AND (EQUAL (I$5) (I$4))
(EQUAL (K$5) '0)))))
WARNING: Note that the proposed lemma ASSIGNMENT5 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT5
(ADD-AXIOM LOGICAL-IF-F6 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F6
(ADD-AXIOM ASSIGNMENT6
(REWRITE)
(AND (EQUAL (BOOLE$6) (BOOLE$5))
(AND (EQUAL (CAND$6) (CAND$5))
(AND (EQUAL (I$6) '1)
(EQUAL (K$6) (K$5))))))
WARNING: Note that the proposed lemma ASSIGNMENT6 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT6
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(ADD-AXIOM EFFECTS-OF-UNDEFINER1
(REWRITE)
(AND (EQUAL (BOOLE$7) (BOOLE$6))
(AND (EQUAL (CAND$7) (CAND$6))
(EQUAL (K$7) (K$6)))))
WARNING: Note that the proposed lemma EFFECTS-OF-UNDEFINER1 is to be stored
as zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
[ 0.0 0.0 0.0 ]
EFFECTS-OF-UNDEFINER1
(ADD-AXIOM ASSIGNMENT7
(REWRITE)
(AND (EQUAL (BOOLE$8) '*1*FALSE)
(AND (EQUAL (CAND$8) (CAND$7))
(AND (EQUAL (I$8) (I$7))
(EQUAL (K$8) (K$7))))))
WARNING: Note that the proposed lemma ASSIGNMENT7 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT7
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (I$6)
(AND (ZGREATERP (I$6) (N$0))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))))))
(AND (OR (EQUAL (BOOLE$8) '*1*TRUE)
(EQUAL (BOOLE$8) '*1*FALSE))
(IF (BOOLE$8)
(AND (ZNUMBERP (CAND$8))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$8) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT5, EFFECTS-OF-UNDEFINER1, ASSIGNMENT7,
ZEQP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ZGREATERP, and
ASSIGNMENT6, to:
(IMPLIES (AND (NOT F)
(ZLESSP (N$0) 1)
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$8) T)
(EQUAL (BOOLE$8) F))
(IF (BOOLE$8)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))).
This simplifies, rewriting with LESSP-X-1, and opening up the functions
NEGATIVEP and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F7 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F7
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A1 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))))
(AND (LESSP '0 (I$6))
(NOT (LESSP (N$0) (I$6))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ZEQP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER,
ASSIGNMENT4, ASSIGNMENT6, and ZGREATERP, to:
(IMPLIES (AND (NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (LESSP 0 1)
(NOT (LESSP (N$0) 1)))).
This simplifies, appealing to the lemmas LESSP-X-1, LESSP-QUOTIENT-REWRITE,
ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and expanding
NEGATIVEP, ZLESSP, ZQUOTIENT, ZNORMALIZE, ZPLUS, LESSP, NOT, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A1
(PROVE-LEMMA DEFINEDNESS4 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))))
(ZNUMBERP (CAND$6))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT5, ZEQP, ASSIGNMENT3,
EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ASSIGNMENT6, and ZGREATERP, to:
(IMPLIES (AND (NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F))
(NOT (NEGATIVEP (CAND$1))))
(NUMBERP (CAND$1))),
which simplifies, rewriting with LESSP-X-1, LESSP-QUOTIENT-REWRITE,
ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and opening up
NEGATIVEP, ZLESSP, ZQUOTIENT, ZNORMALIZE, ZPLUS, and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS4
(PROVE-LEMMA DEFINEDNESS5 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))))
(ZNUMBERP (ELT1 (A$0) (I$6)))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ZEQP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER,
ASSIGNMENT4, ASSIGNMENT6, and ZGREATERP, to:
(IMPLIES (AND (NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F))
(NOT (NEGATIVEP (ELT1 (A$0) 1))))
(NUMBERP (ELT1 (A$0) 1))),
which simplifies, using linear arithmetic, rewriting with LESSP-X-1,
LESSP-QUOTIENT-REWRITE, ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1,
SUB1-ADD1, and INPUT-CONDITIONS, and unfolding the functions NEGATIVEP, ZLESSP,
ZQUOTIENT, ZNORMALIZE, ZPLUS, and LESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS5
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA PHASE2-INVRT NIL
(IMPLIES
(AND (ZNEQP (CAND$6) (ELT1 (A$0) (I$6)))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))))))
(AND
(AND
(NUMBERP (I$6))
(AND
(NOT (EQUAL (I$6) '0))
(AND
(EQUAL (BOOLE$6) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$6)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$6)))
(NUMBERP (CAND$6)))
(AND (IMPLIES (ZNEQP X (CAND$6))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$6) (A$0) '1 (I$6)))))
(EQUAL (K$6)
(CNT (CAND$6) (A$0) '1 (I$6))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$6))
'NIL)
(CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, ZNEQP, AND, IMPLIES, DIFFERENCE-1, ZEQP, ZGREATERP,
ASSIGNMENT3, EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ASSIGNMENT5, and ASSIGNMENT6,
to the conjecture:
(IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (AND (NUMBERP 1)
(NOT (EQUAL 1 0))
(EQUAL (BOOLE$4) T)
(NOT (LESSP (N$0) 1))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES 2 (CNT X (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(TIMES 2 (CNT (CAND$1) (A$0) 1 1))))
(EQUAL 0 (CNT (CAND$1) (A$0) 1 1)))
(LEX (LIST (SUB1 (ADD1 (N$0))))
(LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1)))))))).
This simplifies, rewriting with LESSP-X-1, LESSP-QUOTIENT-REWRITE,
ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, CDR-CONS, and
CAR-CONS, and expanding the functions NEGATIVEP, ZLESSP, ZQUOTIENT, ZNORMALIZE,
ZPLUS, LESSP, NUMBERP, EQUAL, NOT, IMPLIES, ZEQP, ZNEQP, SUB1, TIMES, PLUS,
CNT, AND, DIFFERENCE, and LEX, to four new formulas:
Case 4. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (I$1) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic, applying
PATHS-FROM-PHASE1-INVRT, and expanding the definitions of ZEQP and ZNEQP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (N$0))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (I$1) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic, applying
PATHS-FROM-PHASE1-INVRT, and expanding ZEQP and ZNEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1))))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (N$0))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PHASE2-INVRT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F8 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F8
(PROVE-LEMMA INPUT-COND-OF-ZPLUS1 NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))))))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$6) '1))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, ZNEQP, NOT, AND, IMPLIES, ZEQP, ZGREATERP, ASSIGNMENT3,
EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ASSIGNMENT5, and ASSIGNMENT6, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS 0 1))).
This simplifies, rewriting with LESSP-X-1, LESSP-QUOTIENT-REWRITE,
ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and expanding
the functions NEGATIVEP, ZLESSP, ZQUOTIENT, ZNORMALIZE, ZPLUS, LESSP, EQUAL,
NUMBERP, and EXPRESSIBLE-ZNUMBERP, to two new goals:
Case 2. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP 1
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP 1
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS1
(ADD-AXIOM ASSIGNMENT7
(REWRITE)
(AND (EQUAL (BOOLE$7) (BOOLE$6))
(AND (EQUAL (CAND$7) (CAND$6))
(AND (EQUAL (I$7) (I$6))
(EQUAL (K$7) (ZPLUS (K$6) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT7 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT7
(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT1 NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))))))
(AND (NOT (ZEQP '2 '0))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) '2)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, ZNEQP, NOT, AND, IMPLIES, ZEQP, ZGREATERP, ASSIGNMENT3,
EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ASSIGNMENT5, and ASSIGNMENT6, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) 2)))).
This simplifies, applying LESSP-X-1, LESSP-QUOTIENT-REWRITE, ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and expanding NEGATIVEP, ZLESSP,
ZQUOTIENT, ZNORMALIZE, ZPLUS, LESSP, EQUAL, NOT, EXPRESSIBLE-ZNUMBERP, and AND,
to four new formulas:
Case 4. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and rewriting with
INTEGER-SIZE, to:
T.
Case 3. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZQUOTIENT1
(ADD-AXIOM LOGICAL-IF-T1 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T1
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZGREATERP (K$7)
(ZQUOTIENT (N$0) '2))
(AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))))))
(AND (OR (EQUAL (BOOLE$7) '*1*TRUE)
(EQUAL (BOOLE$7) '*1*FALSE))
(IF (BOOLE$7)
(AND (ZNUMBERP (CAND$7))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$7) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
ZNEQP, NOT, AND, IMPLIES, ZEQP, ASSIGNMENT3, EFFECTS-OF-UNDEFINER, ASSIGNMENT4,
ASSIGNMENT5, ASSIGNMENT6, ASSIGNMENT7, and ZGREATERP, to the new goal:
(IMPLIES (AND (ZLESSP (ZQUOTIENT (N$0) 2)
(ZPLUS 0 1))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))),
which simplifies, appealing to the lemmas LESSP-QUOTIENT-REWRITE and LESSP-X-1,
and expanding the functions NEGATIVEP, ZQUOTIENT, ZPLUS, LESSP, EQUAL, NUMBERP,
SUB1, PLUS, ZLESSP, QUOTIENT, and ZNORMALIZE, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T1)
LOGICAL-IF-T1
(ADD-AXIOM LOGICAL-IF-F9 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F9
(PROVE-LEMMA PHASE2-INVRT NIL
(IMPLIES
(AND (NOT (ZGREATERP (K$7)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZNEQP (CAND$6) (ELT1 (A$0) (I$6))))
(AND (NOT (ZGREATERP (I$6) (N$0)))
(AND (NOT (ZGREATERP (K$4)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZEQP (K$3) '0))
(AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS))))))))
(AND
(AND
(NUMBERP (I$7))
(AND
(NOT (EQUAL (I$7) '0))
(AND
(EQUAL (BOOLE$7) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$7)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$7)))
(NUMBERP (CAND$7)))
(AND (IMPLIES (ZNEQP X (CAND$7))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$7) (A$0) '1 (I$7)))))
(EQUAL (K$7)
(CNT (CAND$7) (A$0) '1 (I$7))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$7))
'NIL)
(CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1))))
'NIL)))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
ZNEQP, NOT, AND, IMPLIES, DIFFERENCE-1, ZEQP, ASSIGNMENT3,
EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ASSIGNMENT5, ASSIGNMENT6, ASSIGNMENT7, and
ZGREATERP, to:
(IMPLIES
(AND (NOT (ZLESSP (ZQUOTIENT (N$0) 2)
(ZPLUS 0 1)))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (ZLESSP (N$0) 1))
(NOT (ZLESSP (ZQUOTIENT (N$0) 2) (K$1)))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (AND (NUMBERP 1)
(NOT (EQUAL 1 0))
(EQUAL (BOOLE$4) T)
(NOT (LESSP (N$0) 1))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES 2 (CNT X (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(TIMES 2 (CNT (CAND$1) (A$0) 1 1))))
(EQUAL (ZPLUS 0 1)
(CNT (CAND$1) (A$0) 1 1)))
(LEX (LIST (SUB1 (ADD1 (N$0))))
(LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1)))))))),
which simplifies, rewriting with the lemmas LESSP-QUOTIENT-REWRITE, LESSP-X-1,
ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, CDR-CONS, and
CAR-CONS, and expanding the functions NEGATIVEP, ZQUOTIENT, ZPLUS, LESSP,
EQUAL, NUMBERP, SUB1, PLUS, ZLESSP, ZNORMALIZE, NOT, IMPLIES, ZEQP, ZNEQP,
TIMES, CNT, ADD1, AND, DIFFERENCE, and LEX, to four new goals:
Case 4. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(NOT (EQUAL (SUB1 (I$1)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (I$1) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic, applying
PATHS-FROM-PHASE1-INVRT, and expanding the functions ZEQP and ZNEQP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (N$0))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(NOT (EQUAL (SUB1 (I$1)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (I$1) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic, applying
PATHS-FROM-PHASE1-INVRT, and opening up the definitions of ZEQP and ZNEQP,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) 1)))
(NOT (LESSP (N$0) (PLUS (K$1) (K$1))))
(NOT (EQUAL (K$1) 0))
(LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (N$0))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
This again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PHASE2-INVRT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F4 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F4
(PROVE-LEMMA DEFINEDNESS3 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))
(ZNUMBERP (K$2))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT3, and ZGREATERP, to the new
conjecture:
T,
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS3
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A1 NIL
(IMPLIES (AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(AND (LESSP '0 (I$2))
(NOT (LESSP (N$0) (I$2))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (LESSP 0 (ZPLUS (I$1) 1))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1))))),
which simplifies, applying ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, and
SUB1-ADD1, and unfolding the functions ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP,
ZLESSP, NUMBERP, EQUAL, NOT, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A1
(PROVE-LEMMA DEFINEDNESS4 NIL
(IMPLIES (AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(ZNUMBERP (ELT1 (A$0) (I$2)))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, PATH-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP,
to the formula:
(IMPLIES (AND (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F))
(NOT (NEGATIVEP (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NUMBERP (ELT1 (A$0) (ZPLUS (I$1) 1)))).
This simplifies, using linear arithmetic, rewriting with ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and INPUT-CONDITIONS, and expanding
the functions ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, ZLESSP, NUMBERP, and EQUAL,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS4
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (ELT1 (A$0) (I$2)))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3) (K$2))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(ADD-AXIOM ASSIGNMENT5
(REWRITE)
(AND (EQUAL (BOOLE$4) (BOOLE$3))
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) '1)))))
WARNING: Note that the proposed lemma ASSIGNMENT5 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT5
(PROVE-LEMMA COMPOUND-INVRT
(REWRITE)
(IMPLIES (EQUAL (K$1) 0)
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1))))))
((USE (PATHS-FROM-PHASE1-INVRT))))
WARNING: Note that the proposed lemma COMPOUND-INVRT 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 NOT, IMPLIES, AND,
and ZEQP, to:
(IMPLIES
(AND (IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (LESSP (PLUS (I$1) (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (I$1)
(PLUS (K$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))))
(EQUAL (K$1) 0))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
This simplifies, appealing to the lemma COMMUTATIVITY-OF-PLUS, and unfolding
EQUAL, PLUS, SUB1, NUMBERP, TIMES, NOT, IMPLIES, ZEQP, ZNEQP, CNT, and LESSP,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
COMPOUND-INVRT
(PROVE-LEMMA PHASE1-INVRT1 NIL
(IMPLIES
(AND (ZEQP (K$2) '0)
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(AND
(AND
(NUMBERP (I$4))
(AND
(NOT (EQUAL (I$4) '0))
(AND
(NUMBERP (K$4))
(AND
(NOT (LESSP (I$4) (K$4)))
(AND
(NOT (LESSP (N$0) (I$4)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$4)))
(NUMBERP (CAND$4)))
(AND
(NOT (LESSP (CNT (CAND$4) (A$0) '1 (I$4))
(K$4)))
(AND
(IMPLIES (ZEQP X (CAND$4))
(NOT (LESSP (PLUS (I$4) (K$4))
(TIMES '2 (CNT X (A$0) '1 (I$4))))))
(IMPLIES
(ZNEQP X (CAND$4))
(NOT (LESSP (I$4)
(PLUS (K$4)
(TIMES '2
(CNT X (A$0) '1 (I$4)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$4))))
'NIL)
(CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, PLUS-1, ASSIGNMENT4, ASSIGNMENT5, ZGREATERP,
ASSIGNMENT3, and ZEQP, to:
(IMPLIES
(AND (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND
(AND
(NUMBERP (ZPLUS (I$1) 1))
(NOT (EQUAL (ZPLUS (I$1) 1) 0))
(NUMBERP 1)
(NOT (LESSP (ZPLUS (I$1) 1) 1))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1)))
(IMPLIES (NOT (NEGATIVEP (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NUMBERP (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (LESSP (CNT (ELT1 (A$0) (ZPLUS (I$1) 1))
(A$0)
1
(ZPLUS (I$1) 1))
1))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (LESSP (PLUS (ZPLUS (I$1) 1) 1)
(TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))
(IMPLIES
(ZNEQP X (ELT1 (A$0) (ZPLUS (I$1) 1)))
(NOT (LESSP (ZPLUS (I$1) 1)
(ADD1 (TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))))
(LEX (LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0))
(ZPLUS (I$1) 1)))))
(LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1)))))))).
This simplifies, applying ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1,
SUB1-ADD1, LESSP-X-1, EQUAL-TIMES-0, CDR-CONS, ADD1-EQUAL, and CAR-CONS, and
expanding the functions ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, ZLESSP, NUMBERP,
EQUAL, NOT, IMPLIES, ZEQP, CNT, ZNEQP, AND, DIFFERENCE, and LEX, to eight new
formulas:
Case 8. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (NEGATIVEP (ELT1 (A$0) (ADD1 (I$1))))))
(NUMBERP (ELT1 (A$0) (ADD1 (I$1))))),
which again simplifies, using linear arithmetic and applying
INPUT-CONDITIONS, to:
T.
Case 7. (IMPLIES
(AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0))
(NOT (EQUAL (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (I$1)
(SUB1 (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))).
But this again simplifies, applying PLUS-1, TIMES-ADD1, and SUB1-ADD1, and
expanding the functions SUB1, NUMBERP, EQUAL, and PLUS, to the new
conjecture:
(IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))),
which again simplifies, using linear arithmetic and applying COMPOUND-INVRT,
to:
T.
Case 6. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
This again simplifies, using linear arithmetic and applying the lemma
COMPOUND-INVRT, to:
T.
Case 5. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1)))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (NEGATIVEP (ELT1 (A$0) (ADD1 (I$1))))))
(NUMBERP (ELT1 (A$0) (ADD1 (I$1))))),
which again simplifies, using linear arithmetic and rewriting with
INPUT-CONDITIONS, to:
T.
Case 3. (IMPLIES
(AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0))
(NOT (EQUAL (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (I$1)
(SUB1 (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))).
This again simplifies, appealing to the lemmas PLUS-1, TIMES-ADD1, and
SUB1-ADD1, and expanding SUB1, NUMBERP, EQUAL, and PLUS, to:
(IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
This again simplifies, using linear arithmetic and rewriting with
COMPOUND-INVRT, to:
T.
Case 2. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))))
(NOT (LESSP (I$1)
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
However this again simplifies, using linear arithmetic and rewriting with
COMPOUND-INVRT, to:
T.
Case 1. (IMPLIES (AND (EQUAL (K$1) 0)
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1)))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PHASE1-INVRT1
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F5 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F5
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A1 NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(AND (LESSP '0 (I$2))
(NOT (LESSP (N$0) (I$2))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP, to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND (LESSP 0 (ZPLUS (I$1) 1))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1))))),
which simplifies, applying ZNORMALIZE-ZERO, COMMUTATIVITY-OF-PLUS, PLUS-1, and
SUB1-ADD1, and expanding ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, ZLESSP, EQUAL,
NOT, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A1
(PROVE-LEMMA DEFINEDNESS4 NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(ZNUMBERP (CAND$2))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, PATH-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP,
to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F))
(NOT (NEGATIVEP (CAND$1))))
(NUMBERP (CAND$1))).
This simplifies, rewriting with the lemmas ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and opening up the functions
ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS4
(PROVE-LEMMA DEFINEDNESS5 NIL
(IMPLIES (AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(ZNUMBERP (ELT1 (A$0) (I$2)))))
This conjecture can be simplified, using the abbreviations ZNUMBERP,
GLOBAL-HYPS, PATH-HYPS, NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP,
to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F))
(NOT (NEGATIVEP (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NUMBERP (ELT1 (A$0) (ZPLUS (I$1) 1)))).
This simplifies, using linear arithmetic, applying the lemmas ZNORMALIZE-ZERO,
COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and INPUT-CONDITIONS, and opening up
ZNORMALIZE, NEGATIVEP, ZPLUS, LESSP, and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS5
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA INPUT-COND-OF-ZPLUS1 NIL
(IMPLIES (AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$2) '1))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$1) 1))),
which simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS, PLUS-1,
ZNORMALIZE-ZERO, and SUB1-ADD1, and unfolding NEGATIVEP, ZPLUS, ZNORMALIZE,
LESSP, ZLESSP, and EXPRESSIBLE-ZNUMBERP, to two new conjectures:
Case 2. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (K$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (K$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS1
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3) (ZPLUS (K$2) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA PHASE1-INVRT1 NIL
(IMPLIES
(AND (ZEQP (CAND$2) (ELT1 (A$0) (I$2)))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (K$3))
(AND
(NOT (LESSP (I$3) (K$3)))
(AND
(NOT (LESSP (N$0) (I$3)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$3)))
(NUMBERP (CAND$3)))
(AND
(NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
(K$3)))
(AND
(IMPLIES (ZEQP X (CAND$3))
(NOT (LESSP (PLUS (I$3) (K$3))
(TIMES '2 (CNT X (A$0) '1 (I$3))))))
(IMPLIES
(ZNEQP X (CAND$3))
(NOT (LESSP (I$3)
(PLUS (K$3)
(TIMES '2
(CNT X (A$0) '1 (I$3)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$3))))
'NIL)
(CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT4, ZGREATERP, ASSIGNMENT3, and ZEQP,
to:
(IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND
(AND
(NUMBERP (ZPLUS (I$1) 1))
(NOT (EQUAL (ZPLUS (I$1) 1) 0))
(NUMBERP (ZPLUS (K$1) 1))
(NOT (LESSP (ZPLUS (I$1) 1)
(ZPLUS (K$1) 1)))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1)))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (ZPLUS (I$1) 1))
(ZPLUS (K$1) 1)))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (LESSP (PLUS (ZPLUS (I$1) 1) (ZPLUS (K$1) 1))
(TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))
(IMPLIES
(ZNEQP X (CAND$1))
(NOT (LESSP (ZPLUS (I$1) 1)
(PLUS (ZPLUS (K$1) 1)
(TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))))
(LEX (LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0))
(ZPLUS (I$1) 1)))))
(LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1)))))))).
This simplifies, appealing to the lemmas COMMUTATIVITY-OF-PLUS, PLUS-1,
ZNORMALIZE-ZERO, SUB1-ADD1, LESSP-X-1, PLUS-ADD1, EQUAL-TIMES-0, CDR-CONS,
ADD1-EQUAL, and CAR-CONS, and opening up NEGATIVEP, ZPLUS, ZNORMALIZE, LESSP,
ZLESSP, NOT, IMPLIES, ZEQP, CNT, NUMBERP, EQUAL, ZNEQP, PLUS, AND, DIFFERENCE,
and LEX, to the following six new conjectures:
Case 6. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0))
(NOT (EQUAL (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (PLUS (I$1) (K$1))
(SUB1 (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))).
But this again simplifies, appealing to the lemmas PLUS-1, TIMES-ADD1, and
SUB1-ADD1, and opening up the definitions of SUB1, NUMBERP, EQUAL, and PLUS,
to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(NOT (LESSP (PLUS (I$1) (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
But this again simplifies, using linear arithmetic, applying
PATHS-FROM-PHASE1-INVRT, and opening up the definition of ZEQP, to:
T.
Case 5. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (K$1)
(TIMES 2 (CNT X (A$0) 1 (I$1))))))).
This again simplifies, using linear arithmetic, appealing to the lemma
PATHS-FROM-PHASE1-INVRT, and opening up the definitions of ZEQP and ZNEQP,
to:
T.
Case 4. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0))
(NOT (EQUAL (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (PLUS (I$1) (K$1))
(SUB1 (SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))),
which again simplifies, appealing to the lemmas PLUS-1, TIMES-ADD1, and
SUB1-ADD1, and unfolding the definitions of SUB1, NUMBERP, EQUAL, and PLUS,
to the formula:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(NOT (LESSP (PLUS (I$1) (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1)))))).
This again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE1-INVRT, and expanding the definition of ZEQP, to:
T.
Case 2. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (I$1)
(PLUS (K$1)
(TIMES 2 (CNT X (A$0) 1 (I$1))))))).
This again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE1-INVRT, and unfolding the definitions of ZEQP and ZNEQP, to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.4 0.0 ]
PHASE1-INVRT1
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F6 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F6
(PROVE-LEMMA INPUT-COND-OF-ZDIFFERENCE1 NIL
(IMPLIES (AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE (K$2) '1))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
NOT, AND, IMPLIES, ZGREATERP, ASSIGNMENT3, and ZEQP, to:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZDIFFERENCE (K$1) 1))),
which simplifies, rewriting with the lemmas COMMUTATIVITY-OF-PLUS, PLUS-1,
ZNORMALIZE-ZERO, SUB1-ADD1, DIFFERENCE-1, and LESSP-X-1, and expanding the
functions NEGATIVEP, ZPLUS, ZNORMALIZE, LESSP, ZLESSP, ZDIFFERENCE, and
EXPRESSIBLE-ZNUMBERP, to four new conjectures:
Case 4. (IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (SUB1 (K$1)) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (K$1))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (SUB1 (K$1)) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (SUB1 (K$1))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZDIFFERENCE1
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3)
(ZDIFFERENCE (K$2) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA PHASE1-INVRT1 NIL
(IMPLIES
(AND (NOT (ZEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZEQP (K$2) '0))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(NUMBERP (K$3))
(AND
(NOT (LESSP (I$3) (K$3)))
(AND
(NOT (LESSP (N$0) (I$3)))
(AND
(IMPLIES (NOT (NEGATIVEP (CAND$3)))
(NUMBERP (CAND$3)))
(AND
(NOT (LESSP (CNT (CAND$3) (A$0) '1 (I$3))
(K$3)))
(AND
(IMPLIES (ZEQP X (CAND$3))
(NOT (LESSP (PLUS (I$3) (K$3))
(TIMES '2 (CNT X (A$0) '1 (I$3))))))
(IMPLIES
(ZNEQP X (CAND$3))
(NOT (LESSP (I$3)
(PLUS (K$3)
(TIMES '2
(CNT X (A$0) '1 (I$3)))))))))))))))
(LEX (CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$3))))
'NIL)
(CONS (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1))))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT4, ZGREATERP, ASSIGNMENT3, and ZEQP,
to:
(IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NOT (EQUAL (ZNORMALIZE (K$1))
(ZNORMALIZE 0)))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))
F T))
(T F)))
(AND
(AND
(NUMBERP (ZPLUS (I$1) 1))
(NOT (EQUAL (ZPLUS (I$1) 1) 0))
(NUMBERP (ZDIFFERENCE (K$1) 1))
(NOT (LESSP (ZPLUS (I$1) 1)
(ZDIFFERENCE (K$1) 1)))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1)))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (ZPLUS (I$1) 1))
(ZDIFFERENCE (K$1) 1)))
(IMPLIES (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (LESSP (PLUS (ZPLUS (I$1) 1)
(ZDIFFERENCE (K$1) 1))
(TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))
(IMPLIES
(ZNEQP X (CAND$1))
(NOT (LESSP (ZPLUS (I$1) 1)
(PLUS (ZDIFFERENCE (K$1) 1)
(TIMES 2
(CNT X (A$0) 1 (ZPLUS (I$1) 1))))))))
(LEX (LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0))
(ZPLUS (I$1) 1)))))
(LIST (ADD1 (PLUS (N$0)
(DIFFERENCE (ADD1 (N$0)) (I$1)))))))).
This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1, ZNORMALIZE-ZERO,
SUB1-ADD1, DIFFERENCE-1, LESSP-X-1, EQUAL-TIMES-0, CDR-CONS, ADD1-EQUAL, and
CAR-CONS, and opening up NEGATIVEP, ZPLUS, ZNORMALIZE, LESSP, ZLESSP, NOT,
ZDIFFERENCE, IMPLIES, ZEQP, CNT, PLUS, NUMBERP, EQUAL, ZNEQP, AND, DIFFERENCE,
and LEX, to 14 new conjectures:
Case 14.(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (SUB1 (K$1)) 0)))
(NOT (LESSP (I$1) (SUB1 (SUB1 (K$1)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 13.(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(SUB1 (K$1))))),
which again simplifies, using linear arithmetic, to:
T.
Case 12.(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (CNT X (A$0) 1 (I$1)) 0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2 (CNT X (A$0) 1 (I$1))))))),
which again simplifies, using linear arithmetic, appealing to the lemma
PATHS-FROM-PHASE1-INVRT, and unfolding the function ZEQP, to:
(IMPLIES (AND (EQUAL (TIMES 2 (CNT X (A$0) 1 (I$1)))
0)
(NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (CNT X (A$0) 1 (I$1)) 0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2 (CNT X (A$0) 1 (I$1))))))).
This again simplifies, using linear arithmetic, to:
T.
Case 11.(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))))),
which again simplifies, trivially, to:
T.
Case 10.(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))
0)))
(NOT (LESSP (I$1)
(SUB1 (PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1)))))))).
This again simplifies, using linear arithmetic, rewriting with the lemma
PATHS-FROM-PHASE1-INVRT, and expanding PLUS, ZEQP, and ZNEQP, to:
T.
Case 9. (IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (PLUS (SUB1 (K$1))
(TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (I$1)
(SUB1 (PLUS (SUB1 (K$1))
(TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))),
which again simplifies, rewriting with PLUS-1, TIMES-ADD1, PLUS-ADD1, and
SUB1-ADD1, and unfolding the functions SUB1, NUMBERP, EQUAL, PLUS, and LESSP,
to the new goal:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (I$1))
(PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))))),
which again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE1-INVRT, and opening up the functions PLUS, ZEQP, and ZNEQP,
to:
T.
Case 8. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))).
However this again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (SUB1 (K$1)) 0)))
(NOT (LESSP (I$1) (SUB1 (SUB1 (K$1)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(SUB1 (K$1))))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (CNT X (A$0) 1 (I$1)) 0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2 (CNT X (A$0) 1 (I$1))))))),
which again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE1-INVRT, and unfolding ZEQP, to the new conjecture:
(IMPLIES (AND (EQUAL (TIMES 2 (CNT X (A$0) 1 (I$1)))
0)
(NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (CNT X (A$0) 1 (I$1)) 0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2 (CNT X (A$0) 1 (I$1))))))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (ADD1 (CNT X (A$0) 1 (I$1)))
0)))
(NOT (LESSP (PLUS (I$1) (SUB1 (K$1)))
(SUB1 (TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))))),
which again simplifies, obviously, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))
0)))
(NOT (LESSP (I$1)
(SUB1 (PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1)))))))).
But this again simplifies, using linear arithmetic, applying the lemma
PATHS-FROM-PHASE1-INVRT, and unfolding the definitions of PLUS, ZEQP, and
ZNEQP, to:
T.
Case 2. (IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1))))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (EQUAL (PLUS (SUB1 (K$1))
(TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1)))))
0)))
(NOT (LESSP (I$1)
(SUB1 (PLUS (SUB1 (K$1))
(TIMES 2
(ADD1 (CNT X (A$0) 1 (I$1))))))))),
which again simplifies, applying PLUS-1, TIMES-ADD1, PLUS-ADD1, and
SUB1-ADD1, and opening up the definitions of SUB1, NUMBERP, EQUAL, PLUS, and
LESSP, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (I$1))
(PLUS (SUB1 (K$1))
(TIMES 2 (CNT X (A$0) 1 (I$1))))))),
which again simplifies, using linear arithmetic, rewriting with the lemma
PATHS-FROM-PHASE1-INVRT, and expanding PLUS, ZEQP, and ZNEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (EQUAL (K$1) 0))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NUMBERP (K$1))
(NOT (LESSP (I$1) (K$1)))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(K$1))))
(LESSP (PLUS (N$0) (DIFFERENCE (N$0) (I$1)))
(PLUS (N$0)
(DIFFERENCE (N$0) (SUB1 (I$1)))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
PHASE1-INVRT1
(UBT PATHS-FROM-PHASE1-INVRT)
PATHS-FROM-PHASE1-INVRT
(ADD-AXIOM PATHS-FROM-PHASE2-INVRT
(REWRITE)
(AND (EQUAL (BOOLE$1) '*1*TRUE)
(AND (IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(EQUAL (K$1)
(CNT (CAND$1) (A$0) '1 (I$1))))))
WARNING: Note that the proposed lemma PATHS-FROM-PHASE2-INVRT is to be stored
as one type prescription rule, zero compound recognizer rules, one linear rule,
and one replacement rule.
[ 0.0 0.0 0.0 ]
PATHS-FROM-PHASE2-INVRT
(DEFN PATH-HYPS NIL
(AND (GLOBAL-HYPS)
(AND (NUMBERP (I$1))
(AND (NOT (EQUAL (I$1) '0))
(AND (NOT (LESSP (N$0) (I$1)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$1)
(A$0)
'1
(I$1)))))))))))
From the definition we can conclude that:
(OR (FALSEP (PATH-HYPS))
(TRUEP (PATH-HYPS)))
is a theorem.
[ 0.0 0.0 0.0 ]
PATH-HYPS
(PROVE-LEMMA DEFINEDNESS2 NIL
(IMPLIES (PATH-HYPS)
(ZNUMBERP (I$1))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to:
T,
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS2
(PROVE-LEMMA INPUT-COND-OF-ZPLUS NIL
(IMPLIES (PATH-HYPS)
(EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) '1))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, and IMPLIES, to the conjecture:
(IMPLIES (AND (NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (I$1) 1))).
This simplifies, applying SUB1-ADD1, COMMUTATIVITY-OF-PLUS, and PLUS-1, and
unfolding the definitions of LESSP, SUB1, NUMBERP, EQUAL, TIMES, PLUS,
NEGATIVEP, ZPLUS, ZLESSP, and EXPRESSIBLE-ZNUMBERP, to two new goals:
Case 2. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS
(ADD-AXIOM ASSIGNMENT3
(REWRITE)
(AND (EQUAL (BOOLE$2) (BOOLE$1))
(AND (EQUAL (CAND$2) (CAND$1))
(AND (EQUAL (I$2) (ZPLUS (I$1) '1))
(EQUAL (K$2) (K$1))))))
WARNING: Note that the proposed lemma ASSIGNMENT3 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT3
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(ADD-AXIOM EFFECTS-OF-UNDEFINER
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(EQUAL (K$3) (K$2)))))
WARNING: Note that the proposed lemma EFFECTS-OF-UNDEFINER is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
[ 0.0 0.0 0.0 ]
EFFECTS-OF-UNDEFINER
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$4) '*1*FALSE)
(AND (EQUAL (CAND$4) (CAND$3))
(AND (EQUAL (I$4) (I$3))
(EQUAL (K$4) (K$3))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as one type
prescription rule, zero compound recognizer rules, zero linear rules, and
three replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1
(REWRITE)
(IMPLIES (EQUAL (ZNORMALIZE X) (ZNORMALIZE Y))
(NOT (LESSP (CNT X A I J) (CNT Y A I J)))))
WARNING: When the linear lemma ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1 is
stored under (CNT Y A I J) it contains the free variable X which will be
chosen by instantiating the hypothesis (EQUAL (ZNORMALIZE X) (ZNORMALIZE Y)).
WARNING: When the linear lemma ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1 is
stored under (CNT X A I J) it contains the free variable Y which will be
chosen by instantiating the hypothesis (EQUAL (ZNORMALIZE X) (ZNORMALIZE Y)).
WARNING: Note that the proposed lemma:
ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1
is to be stored as zero type prescription rules, zero compound recognizer
rules, two linear rules, and zero replacement rules.
Give the conjecture the name *1.
We will appeal to induction. Two 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 (ZEROP J) (LESSP J I))
(p X A I J Y))
(IMPLIES (AND (NOT (OR (ZEROP J) (LESSP J I)))
(ZEQP X (ELT1 A J))
(p X A I (SUB1 J) Y))
(p X A I J Y))
(IMPLIES (AND (NOT (OR (ZEROP J) (LESSP J I)))
(NOT (ZEQP X (ELT1 A J)))
(p X A I (SUB1 J) Y))
(p X A I J Y))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of ZEQP,
ZNORMALIZE, OR, and ZEROP can be used to 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 leads to three new goals:
Case 3. (IMPLIES (AND (OR (ZEROP J) (LESSP J I))
(EQUAL (ZNORMALIZE X) (ZNORMALIZE Y)))
(NOT (LESSP (CNT X A I J) (CNT Y A I J)))),
which simplifies, unfolding the functions ZEROP, OR, EQUAL, CNT, and LESSP,
to:
T.
Case 2. (IMPLIES (AND (NOT (OR (ZEROP J) (LESSP J I)))
(ZEQP X (ELT1 A J))
(NOT (LESSP (CNT X A I (SUB1 J))
(CNT Y A I (SUB1 J))))
(EQUAL (ZNORMALIZE X) (ZNORMALIZE Y)))
(NOT (LESSP (CNT X A I J) (CNT Y A I J)))),
which simplifies, rewriting with the lemma SUB1-ADD1, and opening up ZEROP,
OR, ZEQP, CNT, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (ZEROP J) (LESSP J I)))
(NOT (ZEQP X (ELT1 A J)))
(NOT (LESSP (CNT X A I (SUB1 J))
(CNT Y A I (SUB1 J))))
(EQUAL (ZNORMALIZE X) (ZNORMALIZE Y)))
(NOT (LESSP (CNT X A I J) (CNT Y A I J)))),
which simplifies, opening up ZEROP, OR, ZEQP, and CNT, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1
(PROVE-LEMMA PHASE-2-HINT
(REWRITE)
(IMPLIES (NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0))))))
((USE (PATHS-FROM-PHASE2-INVRT))))
WARNING: Note that the proposed lemma PHASE-2-HINT 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 NOT, IMPLIES, AND,
and PATHS-FROM-PHASE2-INVRT, to:
(IMPLIES (AND (EQUAL (BOOLE$1) T)
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES 2 (CNT X (A$0) 1 (N$0))))))
(EQUAL (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
This simplifies, unfolding the definitions of ZEQP, ZNEQP, SUB1, NUMBERP,
EQUAL, TIMES, NOT, and IMPLIES, to the following two new conjectures:
Case 2. (IMPLIES (AND (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
However this again simplifies, using linear arithmetic and rewriting with
ZEQP-IS-A-CONGRUENCE-RELATION-WRT-CNT-ARG-1, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(TIMES 1 (CNT X (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PHASE-2-HINT
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (I$2)
(AND (ZGREATERP (I$2) (N$0))
(PATH-HYPS)))
(AND (OR (EQUAL (BOOLE$4) '*1*TRUE)
(EQUAL (BOOLE$4) '*1*FALSE))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$4))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$4) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, AND, IMPLIES, EFFECTS-OF-UNDEFINER, ASSIGNMENT4, ZGREATERP, and
ASSIGNMENT3, to:
(IMPLIES (AND (ZPLUS (I$1) 1)
(ZLESSP (N$0) (ZPLUS (I$1) 1))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$4) T)
(EQUAL (BOOLE$4) F))
(IF (BOOLE$4)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))).
This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and
LESSP-QUOTIENT-REWRITE, and expanding the functions NEGATIVEP, ZPLUS, LESSP,
ZLESSP, SUB1, NUMBERP, EQUAL, TIMES, PLUS, OR, NOT, and AND, to two new
formulas:
Case 2. (IMPLIES (AND (LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
This again simplifies, clearly, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
We use the above equality hypothesis by substituting (N$0) for (I$1) and
keeping the equality hypothesis. The result is the conjecture:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (N$0)) (N$0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NOT (EQUAL (N$0) 0))
(NOT (LESSP (N$0) (N$0)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
However this further simplifies, using linear arithmetic and rewriting with
PHASE-2-HINT, to:
T.
Case 1. (IMPLIES (AND (LESSP (SUB1 (N$0)) (I$1))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
This again simplifies, using linear arithmetic, to:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
This again simplifies, clearly, to the new conjecture:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (I$1)) (I$1))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (I$1)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (I$1) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (I$1)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(NOT (LESSP (I$1)
(PLUS (CNT X (A$0) 1 (I$1))
(CNT X (A$0) 1 (I$1)))))).
We now use the above equality hypothesis by substituting (N$0) for (I$1) and
keeping the equality hypothesis. This generates:
(IMPLIES (AND (EQUAL (N$0) (I$1))
(LESSP (SUB1 (N$0)) (N$0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NOT (EQUAL (N$0) 0))
(NOT (LESSP (N$0) (N$0)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
But this further simplifies, using linear arithmetic and applying
PHASE-2-HINT, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F4 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F4
(PROVE-LEMMA ARRAY-BOUNDS-CHECK-FOR-A1 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))
(AND (LESSP '0 (I$2))
(NOT (LESSP (N$0) (I$2))))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT3, and ZGREATERP, to the formula:
(IMPLIES (AND (NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (LESSP 0 (ZPLUS (I$1) 1))
(NOT (LESSP (N$0) (ZPLUS (I$1) 1))))).
This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1,
and expanding the functions NEGATIVEP, ZPLUS, LESSP, ZLESSP, SUB1, NUMBERP,
EQUAL, TIMES, PLUS, NOT, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ARRAY-BOUNDS-CHECK-FOR-A1
(PROVE-LEMMA DEFINEDNESS3 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))
(ZNUMBERP (CAND$2))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT3, and ZGREATERP, to the new
conjecture:
(IMPLIES (AND (NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F))
(NOT (NEGATIVEP (CAND$1))))
(NUMBERP (CAND$1))),
which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1,
and opening up NEGATIVEP, ZPLUS, LESSP, and ZLESSP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS3
(PROVE-LEMMA DEFINEDNESS4 NIL
(IMPLIES (AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))
(ZNUMBERP (ELT1 (A$0) (I$2)))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, NOT, AND, IMPLIES, ASSIGNMENT3, and ZGREATERP, to:
(IMPLIES (AND (NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F))
(NOT (NEGATIVEP (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NUMBERP (ELT1 (A$0) (ZPLUS (I$1) 1)))),
which simplifies, using linear arithmetic, rewriting with
COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and INPUT-CONDITIONS, and expanding
the functions NEGATIVEP, ZPLUS, LESSP, ZLESSP, SUB1, NUMBERP, EQUAL, TIMES,
and PLUS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS4
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA PHASE2-INVRT1 NIL
(IMPLIES
(AND (ZNEQP (CAND$2) (ELT1 (A$0) (I$2)))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(AND
(AND
(NUMBERP (I$2))
(AND
(NOT (EQUAL (I$2) '0))
(AND
(EQUAL (BOOLE$2) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$2)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$2)))
(NUMBERP (CAND$2)))
(AND (IMPLIES (ZNEQP X (CAND$2))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$2) (A$0) '1 (I$2)))))
(EQUAL (K$2)
(CNT (CAND$2) (A$0) '1 (I$2))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$2))
'NIL)
(CONS (DIFFERENCE (ADD1 (N$0)) (I$1))
'NIL)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, NOT, ZEQP, ZNEQP, AND, IMPLIES, PATHS-FROM-PHASE2-INVRT, ZGREATERP,
and ASSIGNMENT3, to:
(IMPLIES
(AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1)))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (AND (NUMBERP (ZPLUS (I$1) 1))
(NOT (EQUAL (ZPLUS (I$1) 1) 0))
(EQUAL (BOOLE$1) T)
(NOT (LESSP (N$0) (ZPLUS (I$1) 1)))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES 2 (CNT X (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(TIMES 2
(CNT (CAND$1)
(A$0)
1
(ZPLUS (I$1) 1)))))
(EQUAL (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1)
(A$0)
1
(ZPLUS (I$1) 1))))
(LEX (LIST (DIFFERENCE (ADD1 (N$0))
(ZPLUS (I$1) 1)))
(LIST (DIFFERENCE (ADD1 (N$0)) (I$1)))))).
This simplifies, applying the lemmas COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1,
LESSP-X-1, CDR-CONS, and CAR-CONS, and opening up the definitions of NEGATIVEP,
ZPLUS, LESSP, ZLESSP, SUB1, NUMBERP, EQUAL, TIMES, PLUS, NOT, IMPLIES, ZEQP,
ZNEQP, CNT, AND, DIFFERENCE, and LEX, to the following four new conjectures:
Case 4. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
This again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE2-INVRT and COMMUTATIVITY-OF-PLUS, and opening up the
definitions of PLUS, TIMES, EQUAL, NUMBERP, SUB1, ZEQP, and ZNEQP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (DIFFERENCE (N$0) (I$1))
(DIFFERENCE (N$0) (SUB1 (I$1))))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, applying the lemmas
PATHS-FROM-PHASE2-INVRT and COMMUTATIVITY-OF-PLUS, and unfolding the
definitions of PLUS, TIMES, EQUAL, NUMBERP, SUB1, ZEQP, and ZNEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1))))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (DIFFERENCE (N$0) (I$1))
(DIFFERENCE (N$0) (SUB1 (I$1))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PHASE2-INVRT1
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F5 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F5
(PROVE-LEMMA DEFINEDNESS5 NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(ZNUMBERP (K$2))))
This formula can be simplified, using the abbreviations ZNUMBERP, GLOBAL-HYPS,
PATH-HYPS, ZEQP, ZNEQP, NOT, AND, IMPLIES, PATHS-FROM-PHASE2-INVRT, ZGREATERP,
and ASSIGNMENT3, to the new formula:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F))
(NOT (NEGATIVEP (CNT (CAND$1) (A$0) 1 (I$1)))))
(NUMBERP (CNT (CAND$1) (A$0) 1 (I$1)))),
which simplifies, obviously, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DEFINEDNESS5
(PROVE-LEMMA INPUT-COND-OF-ZPLUS1 NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (K$2) '1))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, ZEQP, ZNEQP, NOT, AND, IMPLIES, PATHS-FROM-PHASE2-INVRT, ZGREATERP,
and ASSIGNMENT3, to the formula:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(EXPRESSIBLE-ZNUMBERP (ZPLUS (CNT (CAND$1) (A$0) 1 (I$1))
1))).
This simplifies, applying COMMUTATIVITY-OF-PLUS, PLUS-1, and SUB1-ADD1, and
opening up the functions NEGATIVEP, ZPLUS, LESSP, ZLESSP, SUB1, NUMBERP, EQUAL,
TIMES, PLUS, and EXPRESSIBLE-ZNUMBERP, to two new conjectures:
Case 2. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (CNT (CAND$1) (A$0) 1 (I$1))
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZPLUS1
(ADD-AXIOM ASSIGNMENT4
(REWRITE)
(AND (EQUAL (BOOLE$3) (BOOLE$2))
(AND (EQUAL (CAND$3) (CAND$2))
(AND (EQUAL (I$3) (I$2))
(EQUAL (K$3) (ZPLUS (K$2) '1))))))
WARNING: Note that the proposed lemma ASSIGNMENT4 is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and four replacement rules.
[ 0.0 0.0 0.0 ]
ASSIGNMENT4
(PROVE-LEMMA CNT-GROWS
(REWRITE)
(IMPLIES (AND (LESSP (I$1) N)
(ZEQP X (ELT1 A (ADD1 (I$1)))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 N)))
((INDUCT (PLUS N I))))
WARNING: When the linear lemma CNT-GROWS is stored under (CNT X A 1 (I$1)) it
contains the free variable N which will be chosen by instantiating the
hypothesis (LESSP (I$1) N).
WARNING: Note that the proposed lemma CNT-GROWS is to be stored as zero type
prescription rules, zero compound recognizer rules, two linear rules, and zero
replacement rules.
This formula can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, AND, and ZEQP, to the following two new goals:
Case 2. (IMPLIES (AND (ZEROP N)
(LESSP (I$1) N)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1))))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 N))).
This simplifies, opening up ZEROP, EQUAL, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES (AND (LESSP (I$1) (SUB1 N))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1))))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 (SUB1 N))))
(LESSP (I$1) N)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1))))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 N))).
This simplifies, applying LESSP-X-1, and unfolding the functions AND,
IMPLIES, ZEQP, and CNT, to three new formulas:
Case 1.3.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP (I$1) (SUB1 N)))
(LESSP (I$1) N)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A N)))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 (SUB1 N)))),
which again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (NOT (EQUAL (PLUS 1 (I$1)) 0))
(NUMBERP (PLUS 1 (I$1)))
(NOT (LESSP (I$1) (SUB1 (PLUS 1 (I$1)))))
(LESSP (I$1) (PLUS 1 (I$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (PLUS 1 (I$1)))))))
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 (SUB1 (PLUS 1 (I$1)))))).
But this again simplifies, applying PLUS-1, SUB1-ADD1,
SUB1-TYPE-RESTRICTION, and LESSP-X-1, and opening up the definitions of
LESSP, ADD1, and PLUS, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (LESSP (I$1) (SUB1 N)))
(LESSP (I$1) N)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A N))))
(LESSP (CNT X A 1 (I$1))
(ADD1 (CNT X A 1 (SUB1 N))))).
But this again simplifies, using linear arithmetic, to:
(IMPLIES (AND (NOT (EQUAL (PLUS 1 (I$1)) 0))
(NUMBERP (PLUS 1 (I$1)))
(NOT (LESSP (I$1) (SUB1 (PLUS 1 (I$1)))))
(LESSP (I$1) (PLUS 1 (I$1)))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (PLUS 1 (I$1))))))
(LESSP (CNT X A 1 (I$1))
(ADD1 (CNT X A 1 (SUB1 (PLUS 1 (I$1))))))).
This again simplifies, rewriting with PLUS-1, SUB1-ADD1,
SUB1-TYPE-RESTRICTION, and LESSP-X-1, and expanding CNT, SUB1, EQUAL, ADD1,
LESSP, and PLUS, to the new conjecture:
(IMPLIES (AND (NUMBERP (I$1))
(NOT (LESSP (I$1) (I$1)))
(LESSP (SUB1 (I$1)) (I$1))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(NOT (EQUAL (CNT X A 1 (I$1)) 0)))
(LESSP (SUB1 (CNT X A 1 (I$1)))
(CNT X A 1 (I$1)))),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(LESSP (CNT X A 1 (I$1))
(CNT X A 1 (SUB1 N)))
(LESSP (I$1) N)
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A (ADD1 (I$1)))))
(EQUAL (ZNORMALIZE X)
(ZNORMALIZE (ELT1 A N))))
(LESSP (CNT X A 1 (I$1))
(ADD1 (CNT X A 1 (SUB1 N))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNT-GROWS
(PROVE-LEMMA INPUT-COND-OF-ZQUOTIENT NIL
(IMPLIES (AND (NOT (ZNEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS)))
(AND (NOT (ZEQP '2 '0))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) '2)))))
This conjecture can be simplified, using the abbreviations GLOBAL-HYPS,
PATH-HYPS, ZNEQP, NOT, AND, IMPLIES, ZEQP, ZGREATERP, and ASSIGNMENT3, to:
(IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (NOT (EQUAL (ZNORMALIZE 2) (ZNORMALIZE 0)))
(EXPRESSIBLE-ZNUMBERP (ZQUOTIENT (N$0) 2)))).
This simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1, SUB1-ADD1, and
LESSP-QUOTIENT-REWRITE, and unfolding NEGATIVEP, ZPLUS, LESSP, ZLESSP, SUB1,
NUMBERP, EQUAL, TIMES, PLUS, ZNORMALIZE, NOT, ZQUOTIENT, EXPRESSIBLE-ZNUMBERP,
and AND, to four new formulas:
Case 4. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and applying INTEGER-SIZE,
to:
T.
Case 3. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
But this again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES
(AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (NEGATIVE-GUTS (GREATEST-INEXPRESSIBLE-NEGATIVE-INTEGER))
0))
(NOT (EQUAL (QUOTIENT (N$0) 2) 0))),
which again simplifies, using linear arithmetic and rewriting with
INTEGER-SIZE, to:
T.
Case 1. (IMPLIES (AND (EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (N$0)
(PLUS (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INPUT-COND-OF-ZQUOTIENT
(ADD-AXIOM LOGICAL-IF-T NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-T
(PROVE-LEMMA OUTPUT NIL
(IMPLIES (AND (ZGREATERP (K$3)
(ZQUOTIENT (N$0) '2))
(AND (NOT (ZNEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(AND (OR (EQUAL (BOOLE$3) '*1*TRUE)
(EQUAL (BOOLE$3) '*1*FALSE))
(IF (BOOLE$3)
(AND (ZNUMBERP (CAND$3))
(LESSP (QUOTIENT (N$0) '2)
(CNT (CAND$3) (A$0) '1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) '2)
(CNT X (A$0) '1 (N$0))))))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
ZEQP, ZNEQP, NOT, AND, IMPLIES, PATHS-FROM-PHASE2-INVRT, ASSIGNMENT3,
ASSIGNMENT4, and ZGREATERP, to:
(IMPLIES (AND (ZLESSP (ZQUOTIENT (N$0) 2)
(ZPLUS (CNT (CAND$1) (A$0) 1 (I$1))
1))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (OR (EQUAL (BOOLE$1) T)
(EQUAL (BOOLE$1) F))
(IF (BOOLE$1)
(AND (ZNUMBERP (CAND$1))
(LESSP (QUOTIENT (N$0) 2)
(CNT (CAND$1) (A$0) 1 (N$0))))
(NOT (LESSP (QUOTIENT (N$0) 2)
(CNT X (A$0) 1 (N$0))))))),
which simplifies, applying COMMUTATIVITY-OF-PLUS, PLUS-1,
LESSP-QUOTIENT-REWRITE, SUB1-ADD1, and PLUS-ADD1, and expanding the
definitions of NEGATIVEP, ZQUOTIENT, ZPLUS, LESSP, ZLESSP, EQUAL, SUB1,
NUMBERP, TIMES, PLUS, OR, ZNUMBERP, and AND, to the following two new
conjectures:
Case 2. (IMPLIES (AND (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))).
But this again simplifies, using linear arithmetic, rewriting with CNT-GROWS,
and unfolding ZEQP, to:
T.
Case 1. (IMPLIES (AND (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (N$0))
(CNT (CAND$1) (A$0) 1 (N$0))))).
But this again simplifies, using linear arithmetic, rewriting with the lemma
CNT-GROWS, and opening up ZEQP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OUTPUT
(UBT LOGICAL-IF-T)
LOGICAL-IF-T
(ADD-AXIOM LOGICAL-IF-F6 NIL T)
[ 0.0 0.0 0.0 ]
LOGICAL-IF-F6
(PROVE-LEMMA PHASE2-INVRT1 NIL
(IMPLIES
(AND (NOT (ZGREATERP (K$3)
(ZQUOTIENT (N$0) '2)))
(AND (NOT (ZNEQP (CAND$2) (ELT1 (A$0) (I$2))))
(AND (NOT (ZGREATERP (I$2) (N$0)))
(PATH-HYPS))))
(AND
(AND
(NUMBERP (I$3))
(AND
(NOT (EQUAL (I$3) '0))
(AND
(EQUAL (BOOLE$3) '*1*TRUE)
(AND
(NOT (LESSP (N$0) (I$3)))
(AND (IMPLIES (NOT (NEGATIVEP (CAND$3)))
(NUMBERP (CAND$3)))
(AND (IMPLIES (ZNEQP X (CAND$3))
(NOT (LESSP (N$0)
(TIMES '2 (CNT X (A$0) '1 (N$0))))))
(AND (NOT (LESSP (N$0)
(TIMES '2
(CNT (CAND$3) (A$0) '1 (I$3)))))
(EQUAL (K$3)
(CNT (CAND$3) (A$0) '1 (I$3))))))))))
(LEX (CONS (DIFFERENCE (ADD1 (N$0)) (I$3))
'NIL)
(CONS (DIFFERENCE (ADD1 (N$0)) (I$1))
'NIL)))))
This formula can be simplified, using the abbreviations GLOBAL-HYPS, PATH-HYPS,
ZEQP, ZNEQP, NOT, AND, IMPLIES, PATHS-FROM-PHASE2-INVRT, ASSIGNMENT3,
ASSIGNMENT4, and ZGREATERP, to the new formula:
(IMPLIES
(AND (NOT (ZLESSP (ZQUOTIENT (N$0) 2)
(ZPLUS (CNT (CAND$1) (A$0) 1 (I$1))
1)))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ZPLUS (I$1) 1))))
(NOT (ZLESSP (N$0) (ZPLUS (I$1) 1)))
(NOT (EQUAL (N$0) 0))
(LESSP (ADD1 (N$0))
(LEAST-INEXPRESSIBLE-POSITIVE-INTEGER))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(COND ((NEGATIVEP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
((NUMBERP (CAND$1))
(IF (LESSP (N$0)
(TIMES 2
(CNT (CAND$1) (A$0) 1 (I$1))))
F T))
(T F)))
(AND (AND (NUMBERP (ZPLUS (I$1) 1))
(NOT (EQUAL (ZPLUS (I$1) 1) 0))
(EQUAL (BOOLE$1) T)
(NOT (LESSP (N$0) (ZPLUS (I$1) 1)))
(IMPLIES (NOT (NEGATIVEP (CAND$1)))
(NUMBERP (CAND$1)))
(IMPLIES (ZNEQP X (CAND$1))
(NOT (LESSP (N$0)
(TIMES 2 (CNT X (A$0) 1 (N$0))))))
(NOT (LESSP (N$0)
(TIMES 2
(CNT (CAND$1)
(A$0)
1
(ZPLUS (I$1) 1)))))
(EQUAL (ZPLUS (CNT (CAND$1) (A$0) 1 (I$1)) 1)
(CNT (CAND$1)
(A$0)
1
(ZPLUS (I$1) 1))))
(LEX (LIST (DIFFERENCE (ADD1 (N$0))
(ZPLUS (I$1) 1)))
(LIST (DIFFERENCE (ADD1 (N$0)) (I$1)))))),
which simplifies, rewriting with COMMUTATIVITY-OF-PLUS, PLUS-1,
LESSP-QUOTIENT-REWRITE, SUB1-ADD1, PLUS-ADD1, LESSP-X-1, TIMES-ADD1, CDR-CONS,
and CAR-CONS, and opening up NEGATIVEP, ZQUOTIENT, ZPLUS, LESSP, ZLESSP, SUB1,
NUMBERP, EQUAL, TIMES, PLUS, NOT, IMPLIES, ZEQP, ZNEQP, CNT, AND, DIFFERENCE,
and LEX, to the following four new formulas:
Case 4. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(NOT (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))).
This again simplifies, using linear arithmetic, rewriting with
PATHS-FROM-PHASE2-INVRT and COMMUTATIVITY-OF-PLUS, and opening up the
definitions of PLUS, TIMES, EQUAL, NUMBERP, SUB1, ZEQP, and ZNEQP, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(NOT (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NUMBERP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (DIFFERENCE (N$0) (I$1))
(DIFFERENCE (N$0) (SUB1 (I$1))))).
This again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(NOT (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(NOT (EQUAL (ZNORMALIZE X)
(ZNORMALIZE (CAND$1)))))
(NOT (LESSP (N$0)
(PLUS (CNT X (A$0) 1 (N$0))
(CNT X (A$0) 1 (N$0)))))),
which again simplifies, using linear arithmetic, rewriting with the lemmas
PATHS-FROM-PHASE2-INVRT and COMMUTATIVITY-OF-PLUS, and expanding PLUS, TIMES,
EQUAL, NUMBERP, SUB1, ZEQP, and ZNEQP, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (SUB1 (N$0)) 0))
(NOT (LESSP (SUB1 (SUB1 (N$0)))
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1)))))
(EQUAL (ZNORMALIZE (CAND$1))
(ZNORMALIZE (ELT1 (A$0) (ADD1 (I$1)))))
(NOT (LESSP (SUB1 (N$0)) (I$1)))
(NOT (EQUAL (N$0) 0))
(NOT (EQUAL (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)
0))
(LESSP (N$0)
(SUB1 (LEAST-INEXPRESSIBLE-POSITIVE-INTEGER)))
(NUMBERP (N$0))
(NUMBERP (I$1))
(NOT (EQUAL (I$1) 0))
(NOT (LESSP (N$0) (I$1)))
(NEGATIVEP (CAND$1))
(NOT (LESSP (N$0)
(PLUS (CNT (CAND$1) (A$0) 1 (I$1))
(CNT (CAND$1) (A$0) 1 (I$1))))))
(LESSP (DIFFERENCE (N$0) (I$1))
(DIFFERENCE (N$0) (SUB1 (I$1))))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PHASE2-INVRT1
(UBT PATHS-FROM-PHASE2-INVRT)
PATHS-FROM-PHASE2-INVRT
(UBT FORTRAN)
FORTRAN