(NOTE-LIB "piton" T) Loading ./fm9001-piton/piton.lib Finished loading ./fm9001-piton/piton.lib Loading ./fm9001-piton/piton.o Loading ./fm9001-piton/0piton.o Finished loading ./fm9001-piton/0piton.o Loading ./fm9001-piton/1piton.o Finished loading ./fm9001-piton/1piton.o Loading ./fm9001-piton/2piton.o Finished loading ./fm9001-piton/2piton.o Loading ./fm9001-piton/3piton.o Finished loading ./fm9001-piton/3piton.o Loading ./fm9001-piton/4piton.o Finished loading ./fm9001-piton/4piton.o Loading ./fm9001-piton/5piton.o Finished loading ./fm9001-piton/5piton.o Finished loading ./fm9001-piton/piton.o (#./fm9001-piton/piton.lib #./fm9001-piton/piton) (ENABLE PLUS-0) [ 0.0 0.0 0.0 ] PLUS-0-ON5 (ENABLE COMMUTATIVITY-OF-PLUS) [ 0.0 0.0 0.0 ] COMMUTATIVITY-OF-PLUS-ON4 (ENABLE COMMUTATIVITY2-OF-PLUS) [ 0.0 0.0 0.0 ] COMMUTATIVITY2-OF-PLUS-ON2 (ENABLE ASSOCIATIVITY-OF-PLUS) [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-PLUS-ON5 (PROVE-LEMMA PLUS-ADD1-1 (REWRITE) (EQUAL (PLUS (ADD1 X) Y) (ADD1 (PLUS X Y)))) WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the newly proposed PLUS-ADD1-1 could! This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-ADD1-1 (PROVE-LEMMA PLUS-ADD1-2 (REWRITE) (EQUAL (PLUS X (ADD1 Y)) (ADD1 (PLUS X Y)))) WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the newly proposed PLUS-ADD1-2 could! This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] PLUS-ADD1-2 (ENABLE EQUAL-PLUS-0) [ 0.0 0.0 0.0 ] EQUAL-PLUS-0-ON2 (ENABLE TIMES-0) [ 0.0 0.0 0.0 ] TIMES-0-ON (ENABLE TIMES-ADD1) [ 0.0 0.0 0.0 ] TIMES-ADD1-ON1 (ENABLE TIMES-DISTRIBUTES-OVER-PLUS) [ 0.0 0.0 0.0 ] TIMES-DISTRIBUTES-OVER-PLUS-ON3 (ENABLE COMMUTATIVITY-OF-TIMES) [ 0.0 0.0 0.0 ] COMMUTATIVITY-OF-TIMES-ON1 (ENABLE COMMUTATIVITY2-OF-TIMES) [ 0.0 0.0 0.0 ] COMMUTATIVITY2-OF-TIMES-ON1 (ENABLE ASSOCIATIVITY-OF-TIMES) [ 0.0 0.0 0.0 ] ASSOCIATIVITY-OF-TIMES-ON3 (ENABLE EQUAL-TIMES-0) [ 0.0 0.0 0.0 ] EQUAL-TIMES-0-ON1 (ENABLE DIFFERENCE-ELIM) [ 0.0 0.0 0.0 ] DIFFERENCE-ELIM-ON3 (PROVE-LEMMA DIFFERENCE-ELIM-REWRITE1 (REWRITE) (IMPLIES (AND (NUMBERP X) (NOT (LESSP X Y))) (EQUAL (PLUS Y (DIFFERENCE X Y)) X))) WARNING: the previously added lemma, COMMUTATIVITY-OF-PLUS, could be applied whenever the newly proposed DIFFERENCE-ELIM-REWRITE1 could! This conjecture simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] DIFFERENCE-ELIM-REWRITE1 (ENABLE LESSP-REMAINDER) [ 0.0 0.0 0.0 ] LESSP-REMAINDER-ON1 (PROVE-LEMMA LESSP-REMAINDER-LINEAR (REWRITE) (IMPLIES (NOT (ZEROP Y)) (LESSP (REMAINDER X Y) Y))) WARNING: Note that the proposed lemma LESSP-REMAINDER-LINEAR is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL Y 0)) (NUMBERP Y)) (LESSP (REMAINDER X Y) Y)), which simplifies, appealing to the lemma LESSP-REMAINDER, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-REMAINDER-LINEAR (ENABLE REMAINDER-QUOTIENT-ELIM) [ 0.0 0.0 0.0 ] REMAINDER-QUOTIENT-ELIM-ON2 (ENABLE PLUS-REMAINDER-TIMES-QUOTIENT) [ 0.0 0.0 0.0 ] PLUS-REMAINDER-TIMES-QUOTIENT-ON (ENABLE LESSP-QUOTIENT) [ 0.0 0.0 0.0 ] LESSP-QUOTIENT-ON1 (PROVE-LEMMA LESSP-QUOTIENT-LINEAR (REWRITE) (IMPLIES (AND (NOT (ZEROP X)) (NOT (EQUAL Y 1))) (LESSP (QUOTIENT X Y) X))) WARNING: Note that the proposed lemma LESSP-QUOTIENT-LINEAR is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, AND, and IMPLIES, to the new conjecture: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X) (NOT (EQUAL Y 1))) (LESSP (QUOTIENT X Y) X)), which simplifies, applying LESSP-QUOTIENT, to: T. Q.E.D. [ 0.0 0.0 0.0 ] LESSP-QUOTIENT-LINEAR (ENABLE NOT-LESSP-QUOTIENT) [ 0.0 0.0 0.0 ] NOT-LESSP-QUOTIENT-ON1 (PROVE-LEMMA NOT-LESSP-TIMES (REWRITE) (IMPLIES (NOT (ZEROP X)) (NOT (LESSP (TIMES X Y) Y)))) WARNING: Note that the proposed lemma NOT-LESSP-TIMES is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This formula can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP (TIMES X Y) Y))), which we will name *1. We will appeal to induction. There are two plausible inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP X) (p X Y)) (IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y)) (p X Y))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP 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. The above induction scheme produces three new conjectures: Case 3. (IMPLIES (AND (ZEROP X) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP (TIMES X Y) Y))), which simplifies, opening up the definition of ZEROP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP X)) (EQUAL (SUB1 X) 0) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP (TIMES X Y) Y))), which simplifies, rewriting with EQUAL-TIMES-0 and PLUS-0, and opening up the functions ZEROP, TIMES, and EQUAL, to the following two new goals: Case 2.2. (IMPLIES (AND (EQUAL (SUB1 X) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NOT (NUMBERP Y))) (NOT (LESSP 0 Y))). However this again simplifies, opening up the definition of LESSP, to: T. Case 2.1. (IMPLIES (AND (EQUAL (SUB1 X) 0) (NOT (EQUAL X 0)) (NUMBERP X) (NUMBERP Y)) (NOT (LESSP Y Y))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP X)) (NOT (LESSP (TIMES (SUB1 X) Y) Y)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP (TIMES X Y) Y))), which simplifies, opening up the definitions of ZEROP and TIMES, to the conjecture: (IMPLIES (AND (NOT (LESSP (TIMES (SUB1 X) Y) Y)) (NOT (EQUAL X 0)) (NUMBERP X)) (NOT (LESSP (PLUS Y (TIMES (SUB1 X) Y)) Y))). But this again simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] NOT-LESSP-TIMES (DEFN NAT->BIGN (N BASE SIZE) (IF (ZEROP SIZE) NIL (CONS (TAG 'NAT (REMAINDER N BASE)) (NAT->BIGN (QUOTIENT N BASE) BASE (SUB1 SIZE))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each recursive call. Hence, NAT->BIGN is accepted under the principle of definition. From the definition we can conclude that: (OR (LITATOM (NAT->BIGN N BASE SIZE)) (LISTP (NAT->BIGN N BASE SIZE))) is a theorem. [ 0.0 0.0 0.0 ] NAT->BIGN (DEFN BIGN->NAT (A BASE) (IF (NLISTP A) 0 (PLUS (UNTAG (CAR A)) (TIMES BASE (BIGN->NAT (CDR A) BASE))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each recursive call. Hence, BIGN->NAT is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (BIGN->NAT A BASE)) is a theorem. [ 0.0 0.0 0.0 ] BIGN->NAT (DEFN BIGNP (A BASE) (IF (NLISTP A) (EQUAL A NIL) (AND (LISTP (CAR A)) (EQUAL (TYPE (CAR A)) 'NAT) (NUMBERP (UNTAG (CAR A))) (LESSP (UNTAG (CAR A)) BASE) (EQUAL (CDDR (CAR A)) NIL) (BIGNP (CDR A) BASE)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each recursive call. Hence, BIGNP is accepted under the definitional principle. Observe that: (OR (FALSEP (BIGNP A BASE)) (TRUEP (BIGNP A BASE))) is a theorem. [ 0.0 0.0 0.0 ] BIGNP (PROVE-LEMMA BIGNP-NAT->BIGN (REWRITE) (IMPLIES (NOT (ZEROP BASE)) (BIGNP (NAT->BIGN N BASE SIZE) BASE))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to: (IMPLIES (AND (NOT (EQUAL BASE 0)) (NUMBERP BASE)) (BIGNP (NAT->BIGN N BASE SIZE) BASE)). Give the above formula the name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP SIZE) (p N BASE SIZE)) (IMPLIES (AND (NOT (ZEROP SIZE)) (p (QUOTIENT N BASE) BASE (SUB1 SIZE))) (p N BASE SIZE))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for N. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (AND (ZEROP SIZE) (NOT (EQUAL BASE 0)) (NUMBERP BASE)) (BIGNP (NAT->BIGN N BASE SIZE) BASE)). This simplifies, expanding the functions ZEROP, EQUAL, NAT->BIGN, LISTP, and BIGNP, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP SIZE)) (BIGNP (NAT->BIGN (QUOTIENT N BASE) BASE (SUB1 SIZE)) BASE) (NOT (EQUAL BASE 0)) (NUMBERP BASE)) (BIGNP (NAT->BIGN N BASE SIZE) BASE)). This simplifies, applying LESSP-REMAINDER, CDR-CONS, and CAR-CONS, and opening up the definitions of ZEROP, NAT->BIGN, TAG, UNTAG, EQUAL, TYPE, and BIGNP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] BIGNP-NAT->BIGN (PROVE-LEMMA LENGTH-NAT->BIGN (REWRITE) (IMPLIES (NOT (ZEROP BASE)) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) (FIX SIZE)))) This conjecture can be simplified, using the abbreviations ZEROP, NOT, and IMPLIES, to the goal: (IMPLIES (AND (NOT (EQUAL BASE 0)) (NUMBERP BASE)) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) (FIX SIZE))). This simplifies, opening up the definition of FIX, to the following two new goals: Case 2. (IMPLIES (AND (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NOT (NUMBERP SIZE))) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) 0)). However this again simplifies, expanding NAT->BIGN, LENGTH, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NUMBERP SIZE)) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) SIZE)), which we will name *1. Perhaps we can prove it by induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP SIZE) (p N BASE SIZE)) (IMPLIES (AND (NOT (ZEROP SIZE)) (p (QUOTIENT N BASE) BASE (SUB1 SIZE))) (p N BASE SIZE))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for N. The above induction scheme produces the following two new goals: Case 2. (IMPLIES (AND (ZEROP SIZE) (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NUMBERP SIZE)) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) SIZE)). This simplifies, expanding the definitions of ZEROP, NUMBERP, EQUAL, NAT->BIGN, and LENGTH, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP SIZE)) (EQUAL (LENGTH (NAT->BIGN (QUOTIENT N BASE) BASE (SUB1 SIZE))) (SUB1 SIZE)) (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NUMBERP SIZE)) (EQUAL (LENGTH (NAT->BIGN N BASE SIZE)) SIZE)). This simplifies, appealing to the lemmas ADD1-SUB1 and CDR-CONS, and expanding the functions ZEROP, NAT->BIGN, TAG, and LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-NAT->BIGN (PROVE-LEMMA LESSP-QUOTIENT-TIMES (REWRITE) (IMPLIES (LESSP N (TIMES B E)) (EQUAL (LESSP (QUOTIENT N B) E) T))) . Appealing to the lemma REMAINDER-QUOTIENT-ELIM, we now replace N by (PLUS Z (TIMES B X)) to eliminate (QUOTIENT N B) and (REMAINDER N B). We employ LESSP-REMAINDER, the type restriction lemma noted when QUOTIENT was introduced, and the type restriction lemma noted when REMAINDER was introduced to constrain the new variables. The result is four new formulas: Case 4. (IMPLIES (AND (NOT (NUMBERP N)) (LESSP N (TIMES B E))) (LESSP (QUOTIENT N B) E)), which further simplifies, appealing to the lemma EQUAL-TIMES-0, and opening up the definitions of LESSP, QUOTIENT, and EQUAL, to: T. Case 3. (IMPLIES (AND (EQUAL B 0) (LESSP N (TIMES B E))) (LESSP (QUOTIENT N B) E)), which further simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NUMBERP B)) (LESSP N (TIMES B E))) (LESSP (QUOTIENT N B) E)), which further simplifies, expanding the definitions of TIMES, EQUAL, and LESSP, to: T. Case 1. (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (EQUAL (LESSP Z B) (NOT (ZEROP B))) (NUMBERP B) (NOT (EQUAL B 0)) (LESSP (PLUS Z (TIMES B X)) (TIMES B E))) (LESSP X E)), which further simplifies, expanding the functions ZEROP and NOT, to: (IMPLIES (AND (NUMBERP X) (NUMBERP Z) (LESSP Z B) (NUMBERP B) (NOT (EQUAL B 0)) (LESSP (PLUS Z (TIMES B X)) (TIMES B E))) (LESSP X E)), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (IMPLIES (LESSP N (TIMES B E)) (EQUAL (LESSP (QUOTIENT N B) E) T)), which we named *1 above. We will appeal to induction. There are four plausible inductions, two of which are unflawed. So we will choose the one suggested by the largest number of nonprimitive recursive functions. We will induct according to the following scheme: (AND (IMPLIES (ZEROP B) (p N B E)) (IMPLIES (AND (NOT (ZEROP B)) (LESSP N B)) (p N B E)) (IMPLIES (AND (NOT (ZEROP B)) (NOT (LESSP N B)) (p (DIFFERENCE N B) B E)) (p N B E))). Linear arithmetic, the lemmas COUNT-NUMBERP and COUNT-NOT-LESSP, and the definition of ZEROP can be used to 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 produces four new goals: Case 4. (IMPLIES (AND (ZEROP B) (LESSP N (TIMES B E))) (EQUAL (LESSP (QUOTIENT N B) E) T)), which simplifies, expanding the definitions of ZEROP, EQUAL, TIMES, and LESSP, to: T. Case 3. (IMPLIES (AND (NOT (ZEROP B)) (LESSP N B) (LESSP N (TIMES B E))) (EQUAL (LESSP (QUOTIENT N B) E) T)), which simplifies, expanding the definitions of ZEROP, QUOTIENT, EQUAL, and LESSP, to two new conjectures: Case 3.2. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (LESSP N B) (LESSP N (TIMES B E))) (NOT (EQUAL E 0))), which again simplifies, applying TIMES-0, and opening up the functions ZEROP, EQUAL, and LESSP, to: T. Case 3.1. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (LESSP N B) (LESSP N (TIMES B E))) (NUMBERP E)). But this again simplifies, applying the lemma TIMES-0, and expanding the definitions of ZEROP, EQUAL, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP B)) (NOT (LESSP N B)) (NOT (LESSP (DIFFERENCE N B) (TIMES B E))) (LESSP N (TIMES B E))) (EQUAL (LESSP (QUOTIENT N B) E) T)), which simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP B)) (NOT (LESSP N B)) (EQUAL (LESSP (QUOTIENT (DIFFERENCE N B) B) E) T) (LESSP N (TIMES B E))) (EQUAL (LESSP (QUOTIENT N B) E) T)), which simplifies, appealing to the lemma SUB1-ADD1, and expanding the definitions of ZEROP, QUOTIENT, and LESSP, to three new goals: Case 1.3. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (QUOTIENT (DIFFERENCE N B) B) E) (LESSP N (TIMES B E))) (NOT (EQUAL E 0))), which again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (QUOTIENT (DIFFERENCE N B) B) E) (LESSP N (TIMES B E))) (NUMBERP E)), which again simplifies, using linear arithmetic, rewriting with NOT-LESSP-TIMES and TIMES-0, and opening up ZEROP, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (QUOTIENT (DIFFERENCE N B) B) E) (LESSP N (TIMES B E))) (LESSP (QUOTIENT (DIFFERENCE N B) B) (SUB1 E))). This again simplifies, using linear arithmetic, to two new formulas: Case 1.1.2. (IMPLIES (AND (NOT (NUMBERP E)) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (QUOTIENT (DIFFERENCE N B) B) E) (LESSP N (TIMES B E))) (LESSP (QUOTIENT (DIFFERENCE N B) B) (SUB1 E))), which again simplifies, using linear arithmetic, applying NOT-LESSP-TIMES and TIMES-0, and unfolding the definition of ZEROP, to: T. Case 1.1.1. (IMPLIES (AND (NUMBERP E) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (QUOTIENT (DIFFERENCE N B) B) (PLUS 1 (QUOTIENT (DIFFERENCE N B) B))) (LESSP N (TIMES B (PLUS 1 (QUOTIENT (DIFFERENCE N B) B))))) (LESSP (QUOTIENT (DIFFERENCE N B) B) (SUB1 (PLUS 1 (QUOTIENT (DIFFERENCE N B) B))))). However this again simplifies, appealing to the lemmas PLUS-0, PLUS-ADD1-1, SUB1-ADD1, EQUAL-TIMES-0, COMMUTATIVITY-OF-TIMES, and TIMES-ADD1, and unfolding ZEROP, LESSP, PLUS, SUB1, NUMBERP, EQUAL, and TIMES, to: (IMPLIES (AND (NUMBERP E) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (SUB1 (QUOTIENT (DIFFERENCE N B) B)) (QUOTIENT (DIFFERENCE N B) B)) (LESSP N (PLUS B (TIMES B (QUOTIENT (DIFFERENCE N B) B))))) (LESSP (QUOTIENT (DIFFERENCE N B) B) (QUOTIENT (DIFFERENCE N B) B))). Appealing to the lemmas DIFFERENCE-ELIM, REMAINDER-QUOTIENT-ELIM, and SUB1-ELIM, we now replace N by (PLUS B X) to eliminate (DIFFERENCE N B), X by (PLUS V (TIMES B Z)) to eliminate (QUOTIENT X B) and (REMAINDER X B), and Z by (ADD1 X) to eliminate (SUB1 Z). We employ the type restriction lemma noted when DIFFERENCE was introduced, LESSP-REMAINDER, the type restriction lemma noted when QUOTIENT was introduced, the type restriction lemma noted when REMAINDER was introduced, and the type restriction lemma noted when SUB1 was introduced to constrain the new variables. The result is three new conjectures: Case 1.1.1.3. (IMPLIES (AND (NOT (NUMBERP N)) (NUMBERP E) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP N B)) (LESSP (SUB1 (QUOTIENT (DIFFERENCE N B) B)) (QUOTIENT (DIFFERENCE N B) B)) (LESSP N (PLUS B (TIMES B (QUOTIENT (DIFFERENCE N B) B))))) (LESSP (QUOTIENT (DIFFERENCE N B) B) (QUOTIENT (DIFFERENCE N B) B))), which further simplifies, opening up the function LESSP, to: T. Case 1.1.1.2. (IMPLIES (AND (EQUAL Z 0) (NUMBERP Z) (NUMBERP V) (EQUAL (LESSP V B) (NOT (ZEROP B))) (NUMBERP E) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP (PLUS B V (TIMES B Z)) B)) (LESSP (SUB1 Z) Z) (LESSP (PLUS B V (TIMES B Z)) (PLUS B (TIMES B Z)))) (LESSP Z Z)), which further simplifies, using linear arithmetic, to: T. Case 1.1.1.1. (IMPLIES (AND (NUMBERP X) (NOT (EQUAL (ADD1 X) 0)) (NUMBERP V) (EQUAL (LESSP V B) (NOT (ZEROP B))) (NUMBERP E) (NOT (EQUAL B 0)) (NUMBERP B) (NOT (LESSP (PLUS B V (TIMES B (ADD1 X))) B)) (LESSP X (ADD1 X)) (LESSP (PLUS B V (TIMES B (ADD1 X))) (PLUS B (TIMES B (ADD1 X))))) (LESSP (ADD1 X) (ADD1 X))), which further simplifies, using linear arithmetic, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.1 ] LESSP-QUOTIENT-TIMES (PROVE-LEMMA BIGN->NAT->BIGN (REWRITE) (IMPLIES (AND (NUMBERP N) (LESSP 1 BASE) (LESSP N (EXP BASE SIZE))) (EQUAL (BIGN->NAT (NAT->BIGN N BASE SIZE) BASE) N))) Call the conjecture *1. Let us appeal to the induction principle. Four inductions are suggested by terms in the conjecture. They merge into three likely candidate inductions. However, only one is unflawed. We will induct according to the following scheme: (AND (IMPLIES (ZEROP SIZE) (p N BASE SIZE)) (IMPLIES (AND (NOT (ZEROP SIZE)) (p (QUOTIENT N BASE) BASE (SUB1 SIZE))) (p N BASE SIZE))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT SIZE) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for N. The above induction scheme produces three new goals: Case 3. (IMPLIES (AND (ZEROP SIZE) (NUMBERP N) (LESSP 1 BASE) (LESSP N (EXP BASE SIZE))) (EQUAL (BIGN->NAT (NAT->BIGN N BASE SIZE) BASE) N)), which simplifies, unfolding the functions ZEROP, EQUAL, EXP, NAT->BIGN, LISTP, and BIGN->NAT, to two new goals: Case 3.2. (IMPLIES (AND (EQUAL SIZE 0) (NUMBERP N) (LESSP 1 BASE) (LESSP N 1)) (EQUAL 0 N)), which again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (NOT (NUMBERP SIZE)) (NUMBERP N) (LESSP 1 BASE) (LESSP N 1)) (EQUAL 0 N)), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (ZEROP SIZE)) (NOT (LESSP (QUOTIENT N BASE) (EXP BASE (SUB1 SIZE)))) (NUMBERP N) (LESSP 1 BASE) (LESSP N (EXP BASE SIZE))) (EQUAL (BIGN->NAT (NAT->BIGN N BASE SIZE) BASE) N)), which simplifies, applying CDR-CONS and CAR-CONS, and opening up the functions ZEROP, EXP, NAT->BIGN, TAG, UNTAG, and BIGN->NAT, to: (IMPLIES (AND (NOT (EQUAL SIZE 0)) (NUMBERP SIZE) (NOT (LESSP (QUOTIENT N BASE) (EXP BASE (SUB1 SIZE)))) (NUMBERP N) (LESSP 1 BASE) (LESSP N (TIMES BASE (EXP BASE (SUB1 SIZE))))) (EQUAL (PLUS (REMAINDER N BASE) (TIMES BASE (BIGN->NAT (NAT->BIGN (QUOTIENT N BASE) BASE (SUB1 SIZE)) BASE))) N)), which again simplifies, applying LESSP-QUOTIENT-TIMES, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP SIZE)) (EQUAL (BIGN->NAT (NAT->BIGN (QUOTIENT N BASE) BASE (SUB1 SIZE)) BASE) (QUOTIENT N BASE)) (NUMBERP N) (LESSP 1 BASE) (LESSP N (EXP BASE SIZE))) (EQUAL (BIGN->NAT (NAT->BIGN N BASE SIZE) BASE) N)). This simplifies, appealing to the lemmas PLUS-REMAINDER-TIMES-QUOTIENT, CDR-CONS, and CAR-CONS, and opening up the functions ZEROP, EXP, NAT->BIGN, TAG, UNTAG, and BIGN->NAT, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] BIGN->NAT->BIGN (DEFN TV->NAT (C) (IF C 1 0)) Note that (NUMBERP (TV->NAT C)) is a theorem. [ 0.0 0.0 0.0 ] TV->NAT (DEFN BIG-ADD-ARRAY (A B C BASE) (IF (NLISTP A) NIL (CONS (TAG 'NAT (REMAINDER (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each recursive call. Hence, BIG-ADD-ARRAY is accepted under the definitional principle. Observe that: (OR (LITATOM (BIG-ADD-ARRAY A B C BASE)) (LISTP (BIG-ADD-ARRAY A B C BASE))) is a theorem. [ 0.0 0.0 0.0 ] BIG-ADD-ARRAY (DEFN BIG-ADD-CARRY-OUT (A B C BASE) (IF (NLISTP A) (BOOL C) (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each recursive call. Hence, BIG-ADD-CARRY-OUT is accepted under the definitional principle. Note that: (LISTP (BIG-ADD-CARRY-OUT A B C BASE)) is a theorem. [ 0.0 0.0 0.0 ] BIG-ADD-CARRY-OUT (ENABLE DIFFERENCE-X-X) [ 0.0 0.0 0.0 ] DIFFERENCE-X-X-ON3 (PROVE-LEMMA REMAINDER-CARRYOUT1 (REWRITE) (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (ADD1 (PLUS I J)) BASE))) (EQUAL (REMAINDER (ADD1 (PLUS I J)) BASE) (DIFFERENCE (ADD1 (PLUS I J)) BASE))) ((EXPAND (REMAINDER (ADD1 (PLUS I J)) BASE) (REMAINDER (DIFFERENCE (PLUS I J) (SUB1 BASE)) BASE)))) This conjecture simplifies, appealing to the lemma SUB1-ADD1, and opening up LESSP, EQUAL, REMAINDER, and DIFFERENCE, to the formula: (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (PLUS I J) (SUB1 BASE))) (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NOT (LESSP (DIFFERENCE (PLUS I J) (SUB1 BASE)) BASE))) (EQUAL (REMAINDER (DIFFERENCE (DIFFERENCE (PLUS I J) (SUB1 BASE)) BASE) BASE) (DIFFERENCE (PLUS I J) (SUB1 BASE)))). This again simplifies, using linear arithmetic, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-CARRYOUT1 (PROVE-LEMMA REMAINDER-CARRYOUT0 (REWRITE) (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (PLUS I J) BASE))) (EQUAL (REMAINDER (PLUS I J) BASE) (DIFFERENCE (PLUS I J) BASE))) ((EXPAND (REMAINDER (PLUS I J) BASE) (REMAINDER (DIFFERENCE (PLUS I J) BASE) BASE)))) This conjecture simplifies, opening up the function REMAINDER, to three new formulas: Case 3. (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (PLUS I J) BASE)) (NOT (EQUAL BASE 0)) (NUMBERP BASE) (NOT (LESSP (DIFFERENCE (PLUS I J) BASE) BASE))) (EQUAL (REMAINDER (DIFFERENCE (DIFFERENCE (PLUS I J) BASE) BASE) BASE) (DIFFERENCE (PLUS I J) BASE))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (PLUS I J) BASE)) (EQUAL BASE 0)) (EQUAL (PLUS I J) (DIFFERENCE (PLUS I J) BASE))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (LESSP I BASE) (LESSP J BASE) (NOT (LESSP (PLUS I J) BASE)) (NOT (NUMBERP BASE))) (EQUAL (PLUS I J) (DIFFERENCE (PLUS I J) BASE))), which again simplifies, unfolding the function LESSP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] REMAINDER-CARRYOUT0 (PROVE-LEMMA INTERPRETATION-OF-BIG-ADD-RESULTS NIL (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))) ((DISABLE LESSP))) This conjecture can be simplified, using the abbreviations AND, IMPLIES, UNTAG, and TAG, to the formula: (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (LIST 'NAT (BOOL-TO-NAT (CADR (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))). This simplifies, applying COMMUTATIVITY-OF-PLUS and COMMUTATIVITY2-OF-PLUS, and opening up the functions BOOL-TO-NAT and TV->NAT, to four new formulas: Case 4. (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE) (NOT C) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B C BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) '((NAT 1))) BASE) (PLUS 0 (BIGN->NAT A BASE) (BIGN->NAT B BASE)))), which again simplifies, rewriting with the lemma PLUS-0, and expanding ZEROP, to the formula: (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE)))). Name the above subgoal *1. Case 3. (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE) (NOT C) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B C BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) '((NAT 0))) BASE) (PLUS 0 (BIGN->NAT A BASE) (BIGN->NAT B BASE)))). But this again simplifies, rewriting with PLUS-0, and expanding ZEROP, to: (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE)))), which we would normally push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us return to: (IMPLIES (AND (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))). We named this *1. We will try to prove it by induction. Eight 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 (NLISTP A) (p A B C BASE)) (IMPLIES (AND (NOT (NLISTP A)) (p (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) (p A B C BASE))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to establish that the measure (COUNT A) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instances chosen for B and C. The above induction scheme generates the following five new goals: Case 5. (IMPLIES (AND (NLISTP A) (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))). This simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, TIMES-0, and PLUS-0, and unfolding the functions NLISTP, BIGNP, TYPE, UNTAG, LENGTH, EQUAL, LISTP, BIG-ADD-ARRAY, BOOL, TAG, BIG-ADD-CARRY-OUT, BOOL-TO-NAT, APPEND, BIGN->NAT, ZEROP, and TV->NAT, to the following two new conjectures: Case 5.2. (IMPLIES (AND (NOT (LISTP A)) (EQUAL A NIL) (NOT (LISTP B)) (EQUAL B NIL) (NUMBERP BASE) (LESSP 1 BASE) (NOT C)) (EQUAL (CADR '(BOOL F)) 'F)). This again simplifies, opening up the functions LISTP, CDR, CAR, and EQUAL, to: T. Case 5.1. (IMPLIES (AND (NOT (LISTP A)) (EQUAL A NIL) (NOT (LISTP B)) (EQUAL B NIL) (NUMBERP BASE) (LESSP 1 BASE) C) (NOT (EQUAL (CADR '(BOOL T)) 'F))), which again simplifies, expanding LISTP, CDR, CAR, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP A)) (NOT (BIGNP (CDR A) BASE)) (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))), which simplifies, expanding NLISTP, BIGNP, TYPE, and UNTAG, to: T. Case 3. (IMPLIES (AND (NOT (NLISTP A)) (NOT (BIGNP (CDR B) BASE)) (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))), which simplifies, opening up the definitions of NLISTP, BIGNP, TYPE, UNTAG, and LENGTH, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP A)) (NOT (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B)))) (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))), which simplifies, applying ADD1-EQUAL, and expanding the functions NLISTP, BIGNP, TYPE, UNTAG, and LENGTH, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP A)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)))))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) (TV->NAT (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE))))) (BIGNP A BASE) (BIGNP B BASE) (EQUAL (LENGTH A) (LENGTH B)) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B C BASE) (LIST (TAG 'NAT (BOOL-TO-NAT (UNTAG (BIG-ADD-CARRY-OUT A B C BASE)))))) BASE) (PLUS (BIGN->NAT A BASE) (BIGN->NAT B BASE) (TV->NAT C)))). This simplifies, applying ADD1-EQUAL, PLUS-0, PLUS-ADD1-2, SUB1-ADD1, REMAINDER-CARRYOUT1, COMMUTATIVITY2-OF-PLUS, and ASSOCIATIVITY-OF-PLUS, and opening up the functions NLISTP, UNTAG, BOOL-TO-NAT, TAG, TV->NAT, NOT, BIGNP, TYPE, LENGTH, BIG-ADD-ARRAY, ZEROP, REMAINDER, DIFFERENCE, BIG-ADD-CARRY-OUT, and BIGN->NAT, to 32 new formulas: Case 1.32. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.31. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.30. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (EQUAL BASE 0)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.29. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, rewriting with PLUS-0, PLUS-ADD1-2, CDR-CONS, and CAR-CONS, and unfolding the functions ZEROP, APPEND, UNTAG, and BIGN->NAT, to the new formula: (IMPLIES (AND (LISTP A) C (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (PLUS (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (TIMES BASE (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which further simplifies, rewriting with PLUS-0, PLUS-ADD1-2, TIMES-DISTRIBUTES-OVER-PLUS, TIMES-ADD1, COMMUTATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and opening up UNTAG, TV->NAT, ZEROP, and NOT, to: (IMPLIES (AND (LISTP A) C (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (LISTP A) C (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). However this again simplifies, using linear arithmetic, to: T. Case 1.28. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (EQUAL BASE 0)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.27. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, appealing to the lemmas PLUS-0, PLUS-ADD1-2, CDR-CONS, and CAR-CONS, and unfolding the functions ZEROP, APPEND, UNTAG, and BIGN->NAT, to the conjecture: (IMPLIES (AND (LISTP A) C (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (PLUS (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (TIMES BASE (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). However this further simplifies, rewriting with the lemmas PLUS-0 and PLUS-ADD1-2, and expanding the functions UNTAG, TV->NAT, ZEROP, NOT, and EQUAL, to: T. Case 1.26. (IMPLIES (AND (LISTP A) (NOT C) (NOT (LESSP (PLUS (CADAR A) (CADAR B) 0) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 1))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, rewriting with PLUS-0 and PLUS-ADD1-2, and opening up the functions ZEROP, UNTAG, TV->NAT, and NOT, to the new goal: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 1))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, applying the lemmas PLUS-0, REMAINDER-CARRYOUT0, CDR-CONS, CAR-CONS, COMMUTATIVITY2-OF-PLUS, COMMUTATIVITY-OF-PLUS, TIMES-ADD1, and TIMES-DISTRIBUTES-OVER-PLUS, and expanding the definitions of ZEROP, TV->NAT, UNTAG, BIG-ADD-CARRY-OUT, TAG, BIG-ADD-ARRAY, APPEND, and BIGN->NAT, to the formula: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) BASE)) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))). This again simplifies, using linear arithmetic, to: T. Case 1.25. (IMPLIES (AND (LISTP A) (NOT C) (NOT (LESSP (PLUS (CADAR A) (CADAR B) 0) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 0))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, appealing to the lemmas PLUS-0 and PLUS-ADD1-2, and expanding ZEROP, UNTAG, TV->NAT, and NOT, to the goal: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 0))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))). But this again simplifies, rewriting with the lemma PLUS-0, and expanding ZEROP, TV->NAT, UNTAG, and BIG-ADD-CARRY-OUT, to: T. Case 1.24. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.23. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.22. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (EQUAL BASE 0)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, using linear arithmetic, to: T. Case 1.21. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, appealing to the lemmas PLUS-0, PLUS-ADD1-2, CDR-CONS, and CAR-CONS, and opening up the functions ZEROP, APPEND, UNTAG, and BIGN->NAT, to: (IMPLIES (AND (LISTP A) C (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F)) (NOT (EQUAL BASE 0))) (EQUAL (PLUS (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (TIMES BASE (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 1))) BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). This further simplifies, rewriting with PLUS-0 and PLUS-ADD1-2, and expanding the definitions of UNTAG, TV->NAT, ZEROP, and NOT, to: T. Case 1.20. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (EQUAL BASE 0)) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). This again simplifies, using linear arithmetic, to: T. Case 1.19. (IMPLIES (AND (LISTP A) C (NOT (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE)) '((NAT 0))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, applying PLUS-0, PLUS-ADD1-2, CDR-CONS, and CAR-CONS, and unfolding the definitions of ZEROP, APPEND, UNTAG, and BIGN->NAT, to the new conjecture: (IMPLIES (AND (LISTP A) C (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (PLUS (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (TIMES BASE (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which further simplifies, rewriting with the lemmas PLUS-0, PLUS-ADD1-2, TIMES-DISTRIBUTES-OVER-PLUS, TIMES-ADD1, COMMUTATIVITY-OF-PLUS, and COMMUTATIVITY2-OF-PLUS, and opening up UNTAG, TV->NAT, ZEROP, NOT, and EQUAL, to: (IMPLIES (AND (LISTP A) C (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP (PLUS (CADAR A) (CADAR B)) (SUB1 BASE)) (LISTP A) C (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (NOT (EQUAL BASE 0))) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) (SUB1 BASE))) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))). But this again simplifies, using linear arithmetic, to: T. Case 1.18. (IMPLIES (AND (LISTP A) (NOT C) (NOT (LESSP (PLUS (CADAR A) (CADAR B) 0) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 1))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, applying PLUS-0 and PLUS-ADD1-2, and unfolding the definitions of ZEROP, UNTAG, TV->NAT, and NOT, to the new formula: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 1))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, rewriting with PLUS-0, and opening up the definitions of ZEROP, TV->NAT, UNTAG, BIG-ADD-CARRY-OUT, and EQUAL, to: T. Case 1.17. (IMPLIES (AND (LISTP A) (NOT C) (NOT (LESSP (PLUS (CADAR A) (CADAR B) 0) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 0))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 1)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 0))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))). However this again simplifies, rewriting with PLUS-0 and PLUS-ADD1-2, and opening up the definitions of ZEROP, UNTAG, TV->NAT, and NOT, to the new goal: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (EQUAL (CADR (BIG-ADD-CARRY-OUT A B F BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY A B F BASE) '((NAT 0))) BASE) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, rewriting with PLUS-0, REMAINDER-CARRYOUT0, CDR-CONS, CAR-CONS, COMMUTATIVITY2-OF-PLUS, COMMUTATIVITY-OF-PLUS, TIMES-ADD1, and TIMES-DISTRIBUTES-OVER-PLUS, and expanding ZEROP, TV->NAT, UNTAG, BIG-ADD-CARRY-OUT, EQUAL, TAG, BIG-ADD-ARRAY, APPEND, and BIGN->NAT, to: (IMPLIES (AND (LISTP A) (NOT (LESSP (PLUS (CADAR A) (CADAR B)) BASE)) (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) T BASE)) 'F) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) T BASE) '((NAT 0))) BASE) (ADD1 (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE)))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE)) (EQUAL (PLUS BASE (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)) (DIFFERENCE (PLUS (CADAR A) (CADAR B)) BASE)) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))), which again simplifies, using linear arithmetic, to: T. Case 1.16. (IMPLIES (AND (LISTP A) C (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 0)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F))) (EQUAL (BIGN->NAT (APPEND (CONS (LIST 'NAT (ADD1 (PLUS (CADAR A) (CADAR B)))) (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE)) '((NAT 1))) BASE) (ADD1 (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE)))))), which again simplifies, rewriting with the lemmas PLUS-0, PLUS-ADD1-2, CDR-CONS, CAR-CONS, PLUS-ADD1-1, ASSOCIATIVITY-OF-PLUS, and ADD1-EQUAL, and unfolding ZEROP, APPEND, UNTAG, and BIGN->NAT, to: (IMPLIES (AND (LISTP A) C (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE))) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (LESSP 1 BASE) (LESSP (ADD1 (PLUS (CADAR A) (CADAR B))) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) F BASE)) 'F))) (EQUAL (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) F BASE) '((NAT 1))) BASE))) (PLUS (CADAR A) (CADAR B) (TIMES BASE (BIGN->NAT (CDR A) BASE)) (TIMES BASE (BIGN->NAT (CDR B) BASE))))). However this further simplifies, applying PLUS-0, PLUS-ADD1-2, and TIMES-DISTRIBUTES-OVER-PLUS, and unfolding the functions UNTAG, TV->NAT, ZEROP, and NOT, to: T. Case 1.15. (IMPLIES (AND (LISTP A) C (LESSP (PLUS (CADAR A) (CADAR B) 1) BASE) (NOT (EQUAL (CADR (BIG-ADD-CARRY-OUT (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE)) 'F)) (EQUAL (BIGN->NAT (APPEND (BIG-ADD-ARRAY (CDR A) (CDR B) (NOT (LESSP (PLUS (UNTAG (CAR A)) (UNTAG (CAR B)) (TV->NAT C)) BASE)) BASE) '((NAT 1))) BASE) (PLUS (BIGN->NAT (CDR A) BASE) (BIGN->NAT (CDR B) BASE) 0)) (LISTP (CAR A)) (EQUAL (CAAR A) 'NAT) (NUMBERP (CADAR A)) (LESSP (CADAR A) BASE) (EQUAL (CDDAR A) NIL) (BIGNP (CDR A) BASE) (LISTP B) (LISTP (CAR B)) (EQUAL (CAAR B) 'NAT) (NUMBERP (CADAR B)) (LESSP (CADAR B) BASE) (EQUAL (CDDAR B) NIL) (BIGNP (CDR B) BASE) (EQUAL (LENGTH (CDR A)) (LENGTH (CDR B))) (NUMBERP BASE) (