(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)