(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