(NOTE-LIB "mlp" T) Loading ./bronstein/mlp.lib Finished loading ./bronstein/mlp.lib Loading ./bronstein/mlp.o Finished loading ./bronstein/mlp.o (#./bronstein/mlp.lib #./bronstein/mlp) (DEFN INC (U) (ADD1 U)) Observe that (NUMBERP (INC U)) is a theorem. [ 0.0 0.0 0.0 ] INC (DEFN S-INC (X) (IF (EMPTY X) (E) (A (S-INC (P X)) (INC (L X))))) Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, S-INC is accepted under the definitional principle. Note that (STRINGP (S-INC X)) is a theorem. [ 0.0 0.0 0.0 ] S-INC (PROVE-LEMMA A2-EMPTY-S-INC (REWRITE) (EQUAL (EMPTY (S-INC X)) (EMPTY X)) ((DISABLE INC))) Give the conjecture the name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (EMPTY (S-INC X)) (EMPTY X))). This simplifies, expanding the functions S-INC, EMPTY, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (S-INC (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (S-INC X)) (EMPTY X))). This simplifies, rewriting with the lemma STR-NOT-EMPTY-A, and opening up S-INC and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-S-INC (PROVE-LEMMA A2-E-S-INC (REWRITE) (EQUAL (EQUAL (S-INC X) (E)) (EMPTY X)) ((DISABLE S-INC A2-EMPTY-S-INC) (ENABLE EMPTY) (USE (A2-EMPTY-S-INC)))) This simplifies, unfolding the definitions of EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-S-INC (PROVE-LEMMA A2-LP-S-INC (REWRITE) (EQUAL (LEN (S-INC X)) (LEN X)) ((DISABLE INC) (ENABLE LEN))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (LEN (S-INC X)) (LEN X))). This simplifies, expanding the functions S-INC, LEN, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (S-INC (P X))) (LEN (P X)))) (EQUAL (LEN (S-INC X)) (LEN X))). This simplifies, rewriting with the lemmas P-A and STR-NOT-EMPTY-A, and opening up S-INC and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-S-INC (PROVE-LEMMA A2-LPE-S-INC (REWRITE) (EQLEN (S-INC X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN S-INC))) This formula can be simplified, using the abbreviations A2-LP-S-INC and EQLEN-IS-EQUAL-LEN, to the new formula: (EQUAL (LEN X) (LEN X)), which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-S-INC (PROVE-LEMMA A2-IC-S-INC (REWRITE) (EQUAL (S-INC (I C_X X)) (I (INC C_X) (S-INC X))) ((ENABLE I) (DISABLE STR-A-I INC))) Call the conjecture *1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p C_X X)) (IMPLIES (AND (NOT (EMPTY X)) (p C_X (P X))) (p C_X X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT can be used to prove 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 two new goals: Case 2. (IMPLIES (EMPTY X) (EQUAL (S-INC (I C_X X)) (I (INC C_X) (S-INC X)))), which simplifies, applying the lemmas L-A, P-A, STR-NOT-EMPTY-A, and STR-I-E, and opening up the definitions of I, S-INC, and STRINGP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (S-INC (I C_X (P X))) (I (INC C_X) (S-INC (P X))))) (EQUAL (S-INC (I C_X X)) (I (INC C_X) (S-INC X)))), which simplifies, rewriting with L-A, P-A, and STR-NOT-EMPTY-A, and opening up the functions I and S-INC, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-IC-S-INC (PROVE-LEMMA A2-LC-S-INC (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (L (S-INC X)) (INC (L X)))) ((DISABLE INC) (EXPAND (S-INC X)))) This simplifies, appealing to the lemma L-A, and opening up the definition of S-INC, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LC-S-INC (PROVE-LEMMA A2-PC-S-INC (REWRITE) (EQUAL (P (S-INC X)) (S-INC (P X))) ((DISABLE INC))) This conjecture simplifies, opening up the function S-INC, to the following two new goals: Case 2. (IMPLIES (NOT (EMPTY X)) (EQUAL (P (A (S-INC (P X)) (INC (L X)))) (S-INC (P X)))). But this again simplifies, applying P-A, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (P (E)) (S-INC (P X)))). However this again simplifies, rewriting with STR-EMPTY-P, and unfolding P, S-INC, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-PC-S-INC (PROVE-LEMMA A2-HC-S-INC (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (H (S-INC X)) (INC (H X)))) ((DISABLE INC S-INC) (ENABLE H))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (AND (EMPTY (P X)) (NOT (EMPTY X))) (EQUAL (H (S-INC X)) (INC (H X)))), which simplifies, appealing to the lemmas A2-LC-S-INC, A2-PC-S-INC, and A2-EMPTY-S-INC, and unfolding H, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EQUAL (H (S-INC (P X))) (INC (H (P X)))) (NOT (EMPTY X))) (EQUAL (H (S-INC X)) (INC (H X)))), which simplifies, rewriting with the lemmas A2-PC-S-INC and A2-EMPTY-S-INC, and expanding the function H, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-HC-S-INC (PROVE-LEMMA A2-BC-S-INC (REWRITE) (EQUAL (B (S-INC X)) (S-INC (B X))) ((DISABLE INC) (ENABLE B))) Name the conjecture *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT 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 the following three new goals: Case 3. (IMPLIES (EMPTY X) (EQUAL (B (S-INC X)) (S-INC (B X)))). This simplifies, expanding S-INC, B, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (B (S-INC X)) (S-INC (B X)))). This simplifies, rewriting with A2-EMPTY-S-INC, P-A, and STR-NOT-EMPTY-A, and unfolding the definitions of S-INC, B, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (EQUAL (B (S-INC (P X))) (S-INC (B (P X))))) (EQUAL (B (S-INC X)) (S-INC (B X)))), which simplifies, rewriting with L-A, A2-EMPTY-S-INC, P-A, and STR-NOT-EMPTY-A, and expanding the definitions of S-INC and B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BC-S-INC (PROVE-LEMMA A2-BNC-S-INC (REWRITE) (EQUAL (BN N (S-INC X)) (S-INC (BN N X))) ((DISABLE INC S-INC))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N X)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) X)) (p N X))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us 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 the following two new formulas: Case 2. (IMPLIES (ZEROP N) (EQUAL (BN N (S-INC X)) (S-INC (BN N X)))). This simplifies, expanding the definitions of ZEROP, EQUAL, and BN, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (BN (SUB1 N) (S-INC X)) (S-INC (BN (SUB1 N) X)))) (EQUAL (BN N (S-INC X)) (S-INC (BN N X)))). This simplifies, expanding the definitions of ZEROP and BN, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (BN (SUB1 N) (S-INC X)) (S-INC (BN (SUB1 N) X)))) (EQUAL (B (BN (SUB1 N) (S-INC X))) (S-INC (B (BN (SUB1 N) X))))). Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new conjecture: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (BN Z (S-INC X)) (S-INC (BN Z X)))) (EQUAL (B (BN Z (S-INC X))) (S-INC (B (BN Z X))))), which further simplifies, obviously, to the new goal: (IMPLIES (AND (NUMBERP Z) (EQUAL (BN Z (S-INC X)) (S-INC (BN Z X)))) (EQUAL (B (BN Z (S-INC X))) (S-INC (B (BN Z X))))). We now use the above equality hypothesis by substituting (S-INC (BN Z X)) for (BN Z (S-INC X)) and throwing away the equality. We must thus prove: (IMPLIES (NUMBERP Z) (EQUAL (B (S-INC (BN Z X))) (S-INC (B (BN Z X))))). This further simplifies, applying A2-BC-S-INC, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BNC-S-INC (DCL UP (U)) [ 0.0 0.0 0.0 ] UP (DEFN S-UP (X) (IF (EMPTY X) (E) (A (S-UP (P X)) (UP (L X))))) Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, S-UP is accepted under the definitional principle. Note that (STRINGP (S-UP X)) is a theorem. [ 0.0 0.0 0.0 ] S-UP (PROVE-LEMMA A2-EMPTY-S-UP (REWRITE) (EQUAL (EMPTY (S-UP X)) (EMPTY X)) ((DISABLE UP))) Give the conjecture the name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (EMPTY (S-UP X)) (EMPTY X))). This simplifies, expanding the functions S-UP, EMPTY, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (S-UP (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (S-UP X)) (EMPTY X))). This simplifies, rewriting with the lemma STR-NOT-EMPTY-A, and opening up S-UP and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-S-UP (PROVE-LEMMA A2-E-S-UP (REWRITE) (EQUAL (EQUAL (S-UP X) (E)) (EMPTY X)) ((DISABLE S-UP A2-EMPTY-S-UP) (ENABLE EMPTY) (USE (A2-EMPTY-S-UP)))) This simplifies, unfolding the definitions of EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-S-UP (PROVE-LEMMA A2-LP-S-UP (REWRITE) (EQUAL (LEN (S-UP X)) (LEN X)) ((DISABLE UP) (ENABLE LEN))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (LEN (S-UP X)) (LEN X))). This simplifies, expanding the functions S-UP, LEN, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (S-UP (P X))) (LEN (P X)))) (EQUAL (LEN (S-UP X)) (LEN X))). This simplifies, rewriting with the lemmas P-A and STR-NOT-EMPTY-A, and opening up S-UP and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-S-UP (PROVE-LEMMA A2-LPE-S-UP (REWRITE) (EQLEN (S-UP X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN S-UP))) This formula can be simplified, using the abbreviations A2-LP-S-UP and EQLEN-IS-EQUAL-LEN, to the new formula: (EQUAL (LEN X) (LEN X)), which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-S-UP (PROVE-LEMMA A2-IC-S-UP (REWRITE) (EQUAL (S-UP (I C_X X)) (I (UP C_X) (S-UP X))) ((ENABLE I) (DISABLE STR-A-I UP))) Call the conjecture *1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p C_X X)) (IMPLIES (AND (NOT (EMPTY X)) (p C_X (P X))) (p C_X X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT can be used to prove 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 two new goals: Case 2. (IMPLIES (EMPTY X) (EQUAL (S-UP (I C_X X)) (I (UP C_X) (S-UP X)))), which simplifies, applying the lemmas L-A, P-A, STR-NOT-EMPTY-A, and STR-I-E, and opening up the definitions of I, S-UP, and STRINGP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (S-UP (I C_X (P X))) (I (UP C_X) (S-UP (P X))))) (EQUAL (S-UP (I C_X X)) (I (UP C_X) (S-UP X)))), which simplifies, rewriting with L-A, P-A, and STR-NOT-EMPTY-A, and opening up the functions I and S-UP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-IC-S-UP (PROVE-LEMMA A2-LC-S-UP (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (L (S-UP X)) (UP (L X)))) ((DISABLE UP) (EXPAND (S-UP X)))) This simplifies, appealing to the lemma L-A, and opening up the definition of S-UP, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LC-S-UP (PROVE-LEMMA A2-PC-S-UP (REWRITE) (EQUAL (P (S-UP X)) (S-UP (P X))) ((DISABLE UP))) This conjecture simplifies, opening up the function S-UP, to the following two new goals: Case 2. (IMPLIES (NOT (EMPTY X)) (EQUAL (P (A (S-UP (P X)) (UP (L X)))) (S-UP (P X)))). But this again simplifies, applying P-A, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (P (E)) (S-UP (P X)))). However this again simplifies, rewriting with STR-EMPTY-P, and unfolding P, S-UP, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-PC-S-UP (PROVE-LEMMA A2-HC-S-UP (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (H (S-UP X)) (UP (H X)))) ((DISABLE UP S-UP) (ENABLE H))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (AND (EMPTY (P X)) (NOT (EMPTY X))) (EQUAL (H (S-UP X)) (UP (H X)))), which simplifies, appealing to the lemmas A2-LC-S-UP, A2-PC-S-UP, and A2-EMPTY-S-UP, and unfolding H, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EQUAL (H (S-UP (P X))) (UP (H (P X)))) (NOT (EMPTY X))) (EQUAL (H (S-UP X)) (UP (H X)))), which simplifies, rewriting with the lemmas A2-PC-S-UP and A2-EMPTY-S-UP, and expanding the function H, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-HC-S-UP (PROVE-LEMMA A2-BC-S-UP (REWRITE) (EQUAL (B (S-UP X)) (S-UP (B X))) ((DISABLE UP) (ENABLE B))) Name the conjecture *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT 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 the following three new goals: Case 3. (IMPLIES (EMPTY X) (EQUAL (B (S-UP X)) (S-UP (B X)))). This simplifies, expanding S-UP, B, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (B (S-UP X)) (S-UP (B X)))). This simplifies, rewriting with A2-EMPTY-S-UP, P-A, and STR-NOT-EMPTY-A, and unfolding the definitions of S-UP, B, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (EQUAL (B (S-UP (P X))) (S-UP (B (P X))))) (EQUAL (B (S-UP X)) (S-UP (B X)))), which simplifies, rewriting with L-A, A2-EMPTY-S-UP, P-A, and STR-NOT-EMPTY-A, and expanding the definitions of S-UP and B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BC-S-UP (PROVE-LEMMA A2-BNC-S-UP (REWRITE) (EQUAL (BN N (S-UP X)) (S-UP (BN N X))) ((DISABLE UP S-UP))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N X)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) X)) (p N X))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us 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 the following two new formulas: Case 2. (IMPLIES (ZEROP N) (EQUAL (BN N (S-UP X)) (S-UP (BN N X)))). This simplifies, expanding the definitions of ZEROP, EQUAL, and BN, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (BN (SUB1 N) (S-UP X)) (S-UP (BN (SUB1 N) X)))) (EQUAL (BN N (S-UP X)) (S-UP (BN N X)))). This simplifies, expanding the definitions of ZEROP and BN, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (BN (SUB1 N) (S-UP X)) (S-UP (BN (SUB1 N) X)))) (EQUAL (B (BN (SUB1 N) (S-UP X))) (S-UP (B (BN (SUB1 N) X))))). Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new conjecture: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (BN Z (S-UP X)) (S-UP (BN Z X)))) (EQUAL (B (BN Z (S-UP X))) (S-UP (B (BN Z X))))), which further simplifies, obviously, to the new goal: (IMPLIES (AND (NUMBERP Z) (EQUAL (BN Z (S-UP X)) (S-UP (BN Z X)))) (EQUAL (B (BN Z (S-UP X))) (S-UP (B (BN Z X))))). We now use the above equality hypothesis by substituting (S-UP (BN Z X)) for (BN Z (S-UP X)) and throwing away the equality. We must thus prove: (IMPLIES (NUMBERP Z) (EQUAL (B (S-UP (BN Z X))) (S-UP (B (BN Z X))))). This further simplifies, applying A2-BC-S-UP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BNC-S-UP (DCL UI (U)) [ 0.0 0.0 0.0 ] UI (DEFN S-UI (X) (IF (EMPTY X) (E) (A (S-UI (P X)) (UI (L X))))) Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, S-UI is accepted under the definitional principle. Note that (STRINGP (S-UI X)) is a theorem. [ 0.0 0.0 0.0 ] S-UI (PROVE-LEMMA A2-EMPTY-S-UI (REWRITE) (EQUAL (EMPTY (S-UI X)) (EMPTY X)) ((DISABLE UI))) Give the conjecture the name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (EMPTY (S-UI X)) (EMPTY X))). This simplifies, expanding the functions S-UI, EMPTY, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (S-UI (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (S-UI X)) (EMPTY X))). This simplifies, rewriting with the lemma STR-NOT-EMPTY-A, and opening up S-UI and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-S-UI (PROVE-LEMMA A2-E-S-UI (REWRITE) (EQUAL (EQUAL (S-UI X) (E)) (EMPTY X)) ((DISABLE S-UI A2-EMPTY-S-UI) (ENABLE EMPTY) (USE (A2-EMPTY-S-UI)))) This simplifies, unfolding the definitions of EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-S-UI (PROVE-LEMMA A2-LP-S-UI (REWRITE) (EQUAL (LEN (S-UI X)) (LEN X)) ((DISABLE UI) (ENABLE LEN))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (LEN (S-UI X)) (LEN X))). This simplifies, expanding the functions S-UI, LEN, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (S-UI (P X))) (LEN (P X)))) (EQUAL (LEN (S-UI X)) (LEN X))). This simplifies, rewriting with the lemmas P-A and STR-NOT-EMPTY-A, and opening up S-UI and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-S-UI (PROVE-LEMMA A2-LPE-S-UI (REWRITE) (EQLEN (S-UI X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN S-UI))) This formula can be simplified, using the abbreviations A2-LP-S-UI and EQLEN-IS-EQUAL-LEN, to the new formula: (EQUAL (LEN X) (LEN X)), which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-S-UI (PROVE-LEMMA A2-IC-S-UI (REWRITE) (EQUAL (S-UI (I C_X X)) (I (UI C_X) (S-UI X))) ((ENABLE I) (DISABLE STR-A-I UI))) Call the conjecture *1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p C_X X)) (IMPLIES (AND (NOT (EMPTY X)) (p C_X (P X))) (p C_X X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT can be used to prove 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 two new goals: Case 2. (IMPLIES (EMPTY X) (EQUAL (S-UI (I C_X X)) (I (UI C_X) (S-UI X)))), which simplifies, applying the lemmas L-A, P-A, STR-NOT-EMPTY-A, and STR-I-E, and opening up the definitions of I, S-UI, and STRINGP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (S-UI (I C_X (P X))) (I (UI C_X) (S-UI (P X))))) (EQUAL (S-UI (I C_X X)) (I (UI C_X) (S-UI X)))), which simplifies, rewriting with L-A, P-A, and STR-NOT-EMPTY-A, and opening up the functions I and S-UI, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-IC-S-UI (PROVE-LEMMA A2-LC-S-UI (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (L (S-UI X)) (UI (L X)))) ((DISABLE UI) (EXPAND (S-UI X)))) This simplifies, appealing to the lemma L-A, and opening up the definition of S-UI, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LC-S-UI (PROVE-LEMMA A2-PC-S-UI (REWRITE) (EQUAL (P (S-UI X)) (S-UI (P X))) ((DISABLE UI))) This conjecture simplifies, opening up the function S-UI, to the following two new goals: Case 2. (IMPLIES (NOT (EMPTY X)) (EQUAL (P (A (S-UI (P X)) (UI (L X)))) (S-UI (P X)))). But this again simplifies, applying P-A, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (P (E)) (S-UI (P X)))). However this again simplifies, rewriting with STR-EMPTY-P, and unfolding P, S-UI, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-PC-S-UI (PROVE-LEMMA A2-HC-S-UI (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (H (S-UI X)) (UI (H X)))) ((DISABLE UI S-UI) (ENABLE H))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (AND (EMPTY (P X)) (NOT (EMPTY X))) (EQUAL (H (S-UI X)) (UI (H X)))), which simplifies, appealing to the lemmas A2-LC-S-UI, A2-PC-S-UI, and A2-EMPTY-S-UI, and unfolding H, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EQUAL (H (S-UI (P X))) (UI (H (P X)))) (NOT (EMPTY X))) (EQUAL (H (S-UI X)) (UI (H X)))), which simplifies, rewriting with the lemmas A2-PC-S-UI and A2-EMPTY-S-UI, and expanding the function H, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-HC-S-UI (PROVE-LEMMA A2-BC-S-UI (REWRITE) (EQUAL (B (S-UI X)) (S-UI (B X))) ((DISABLE UI) (ENABLE B))) Name the conjecture *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT 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 the following three new goals: Case 3. (IMPLIES (EMPTY X) (EQUAL (B (S-UI X)) (S-UI (B X)))). This simplifies, expanding S-UI, B, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (B (S-UI X)) (S-UI (B X)))). This simplifies, rewriting with A2-EMPTY-S-UI, P-A, and STR-NOT-EMPTY-A, and unfolding the definitions of S-UI, B, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (EQUAL (B (S-UI (P X))) (S-UI (B (P X))))) (EQUAL (B (S-UI X)) (S-UI (B X)))), which simplifies, rewriting with L-A, A2-EMPTY-S-UI, P-A, and STR-NOT-EMPTY-A, and expanding the definitions of S-UI and B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BC-S-UI (PROVE-LEMMA A2-BNC-S-UI (REWRITE) (EQUAL (BN N (S-UI X)) (S-UI (BN N X))) ((DISABLE UI S-UI))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N X)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) X)) (p N X))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us 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 the following two new formulas: Case 2. (IMPLIES (ZEROP N) (EQUAL (BN N (S-UI X)) (S-UI (BN N X)))). This simplifies, expanding the definitions of ZEROP, EQUAL, and BN, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (BN (SUB1 N) (S-UI X)) (S-UI (BN (SUB1 N) X)))) (EQUAL (BN N (S-UI X)) (S-UI (BN N X)))). This simplifies, expanding the definitions of ZEROP and BN, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (BN (SUB1 N) (S-UI X)) (S-UI (BN (SUB1 N) X)))) (EQUAL (B (BN (SUB1 N) (S-UI X))) (S-UI (B (BN (SUB1 N) X))))). Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new conjecture: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (BN Z (S-UI X)) (S-UI (BN Z X)))) (EQUAL (B (BN Z (S-UI X))) (S-UI (B (BN Z X))))), which further simplifies, obviously, to the new goal: (IMPLIES (AND (NUMBERP Z) (EQUAL (BN Z (S-UI X)) (S-UI (BN Z X)))) (EQUAL (B (BN Z (S-UI X))) (S-UI (B (BN Z X))))). We now use the above equality hypothesis by substituting (S-UI (BN Z X)) for (BN Z (S-UI X)) and throwing away the equality. We must thus prove: (IMPLIES (NUMBERP Z) (EQUAL (B (S-UI (BN Z X))) (S-UI (B (BN Z X))))). This further simplifies, applying A2-BC-S-UI, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BNC-S-UI (DCL UE (U)) [ 0.0 0.0 0.0 ] UE (DEFN S-UE (X) (IF (EMPTY X) (E) (A (S-UE (P X)) (UE (L X))))) Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT establish that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, S-UE is accepted under the definitional principle. Note that (STRINGP (S-UE X)) is a theorem. [ 0.0 0.0 0.0 ] S-UE (PROVE-LEMMA A2-EMPTY-S-UE (REWRITE) (EQUAL (EMPTY (S-UE X)) (EMPTY X)) ((DISABLE UE))) Give the conjecture the name *1. We will appeal to induction. There is only one plausible induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (EMPTY (S-UE X)) (EMPTY X))). This simplifies, expanding the functions S-UE, EMPTY, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (S-UE (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (S-UE X)) (EMPTY X))). This simplifies, rewriting with the lemma STR-NOT-EMPTY-A, and opening up S-UE and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-S-UE (PROVE-LEMMA A2-E-S-UE (REWRITE) (EQUAL (EQUAL (S-UE X) (E)) (EMPTY X)) ((DISABLE S-UE A2-EMPTY-S-UE) (ENABLE EMPTY) (USE (A2-EMPTY-S-UE)))) This simplifies, unfolding the definitions of EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-S-UE (PROVE-LEMMA A2-LP-S-UE (REWRITE) (EQUAL (LEN (S-UE X)) (LEN X)) ((DISABLE UE) (ENABLE LEN))) Give the conjecture the name *1. We will appeal to induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces the following two new conjectures: Case 2. (IMPLIES (EMPTY X) (EQUAL (LEN (S-UE X)) (LEN X))). This simplifies, expanding the functions S-UE, LEN, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (S-UE (P X))) (LEN (P X)))) (EQUAL (LEN (S-UE X)) (LEN X))). This simplifies, rewriting with the lemmas P-A and STR-NOT-EMPTY-A, and opening up S-UE and LEN, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-S-UE (PROVE-LEMMA A2-LPE-S-UE (REWRITE) (EQLEN (S-UE X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN S-UE))) This formula can be simplified, using the abbreviations A2-LP-S-UE and EQLEN-IS-EQUAL-LEN, to the new formula: (EQUAL (LEN X) (LEN X)), which simplifies, clearly, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-S-UE (PROVE-LEMMA A2-IC-S-UE (REWRITE) (EQUAL (S-UE (I C_X X)) (I (UE C_X) (S-UE X))) ((ENABLE I) (DISABLE STR-A-I UE))) Call the conjecture *1. Perhaps we can prove it by induction. Two inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p C_X X)) (IMPLIES (AND (NOT (EMPTY X)) (p C_X (P X))) (p C_X X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT can be used to prove 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 two new goals: Case 2. (IMPLIES (EMPTY X) (EQUAL (S-UE (I C_X X)) (I (UE C_X) (S-UE X)))), which simplifies, applying the lemmas L-A, P-A, STR-NOT-EMPTY-A, and STR-I-E, and opening up the definitions of I, S-UE, and STRINGP, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (S-UE (I C_X (P X))) (I (UE C_X) (S-UE (P X))))) (EQUAL (S-UE (I C_X X)) (I (UE C_X) (S-UE X)))), which simplifies, rewriting with L-A, P-A, and STR-NOT-EMPTY-A, and opening up the functions I and S-UE, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-IC-S-UE (PROVE-LEMMA A2-LC-S-UE (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (L (S-UE X)) (UE (L X)))) ((DISABLE UE) (EXPAND (S-UE X)))) This simplifies, appealing to the lemma L-A, and opening up the definition of S-UE, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LC-S-UE (PROVE-LEMMA A2-PC-S-UE (REWRITE) (EQUAL (P (S-UE X)) (S-UE (P X))) ((DISABLE UE))) This conjecture simplifies, opening up the function S-UE, to the following two new goals: Case 2. (IMPLIES (NOT (EMPTY X)) (EQUAL (P (A (S-UE (P X)) (UE (L X)))) (S-UE (P X)))). But this again simplifies, applying P-A, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (P (E)) (S-UE (P X)))). However this again simplifies, rewriting with STR-EMPTY-P, and unfolding P, S-UE, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-PC-S-UE (PROVE-LEMMA A2-HC-S-UE (REWRITE) (IMPLIES (NOT (EMPTY X)) (EQUAL (H (S-UE X)) (UE (H X)))) ((DISABLE UE S-UE) (ENABLE H))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates two new goals: Case 2. (IMPLIES (AND (EMPTY (P X)) (NOT (EMPTY X))) (EQUAL (H (S-UE X)) (UE (H X)))), which simplifies, appealing to the lemmas A2-LC-S-UE, A2-PC-S-UE, and A2-EMPTY-S-UE, and unfolding H, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EQUAL (H (S-UE (P X))) (UE (H (P X)))) (NOT (EMPTY X))) (EQUAL (H (S-UE X)) (UE (H X)))), which simplifies, rewriting with the lemmas A2-PC-S-UE and A2-EMPTY-S-UE, and expanding the function H, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-HC-S-UE (PROVE-LEMMA A2-BC-S-UE (REWRITE) (EQUAL (B (S-UE X)) (S-UE (B X))) ((DISABLE UE) (ENABLE B))) Name the conjecture *1. Perhaps we can prove it by induction. There are two plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (EMPTY X) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (p X)) (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (p (P X))) (p X))). Linear arithmetic and the lemmas P-LESSEQP and STR-EMPTY-COUNT 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 the following three new goals: Case 3. (IMPLIES (EMPTY X) (EQUAL (B (S-UE X)) (S-UE (B X)))). This simplifies, expanding S-UE, B, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (B (S-UE X)) (S-UE (B X)))). This simplifies, rewriting with A2-EMPTY-S-UE, P-A, and STR-NOT-EMPTY-A, and unfolding the definitions of S-UE, B, and EQUAL, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (EQUAL (B (S-UE (P X))) (S-UE (B (P X))))) (EQUAL (B (S-UE X)) (S-UE (B X)))), which simplifies, rewriting with L-A, A2-EMPTY-S-UE, P-A, and STR-NOT-EMPTY-A, and expanding the definitions of S-UE and B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BC-S-UE (PROVE-LEMMA A2-BNC-S-UE (REWRITE) (EQUAL (BN N (S-UE X)) (S-UE (BN N X))) ((DISABLE UE S-UE))) Name the conjecture *1. We will appeal to induction. The recursive terms in the conjecture suggest two inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (ZEROP N) (p N X)) (IMPLIES (AND (NOT (ZEROP N)) (p (SUB1 N) X)) (p N X))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform us 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 the following two new formulas: Case 2. (IMPLIES (ZEROP N) (EQUAL (BN N (S-UE X)) (S-UE (BN N X)))). This simplifies, expanding the definitions of ZEROP, EQUAL, and BN, to: T. Case 1. (IMPLIES (AND (NOT (ZEROP N)) (EQUAL (BN (SUB1 N) (S-UE X)) (S-UE (BN (SUB1 N) X)))) (EQUAL (BN N (S-UE X)) (S-UE (BN N X)))). This simplifies, expanding the definitions of ZEROP and BN, to: (IMPLIES (AND (NOT (EQUAL N 0)) (NUMBERP N) (EQUAL (BN (SUB1 N) (S-UE X)) (S-UE (BN (SUB1 N) X)))) (EQUAL (B (BN (SUB1 N) (S-UE X))) (S-UE (B (BN (SUB1 N) X))))). Applying the lemma SUB1-ELIM, replace N by (ADD1 Z) to eliminate (SUB1 N). We use the type restriction lemma noted when SUB1 was introduced to restrict the new variable. We thus obtain the new conjecture: (IMPLIES (AND (NUMBERP Z) (NOT (EQUAL (ADD1 Z) 0)) (EQUAL (BN Z (S-UE X)) (S-UE (BN Z X)))) (EQUAL (B (BN Z (S-UE X))) (S-UE (B (BN Z X))))), which further simplifies, obviously, to the new goal: (IMPLIES (AND (NUMBERP Z) (EQUAL (BN Z (S-UE X)) (S-UE (BN Z X)))) (EQUAL (B (BN Z (S-UE X))) (S-UE (B (BN Z X))))). We now use the above equality hypothesis by substituting (S-UE (BN Z X)) for (BN Z (S-UE X)) and throwing away the equality. We must thus prove: (IMPLIES (NUMBERP Z) (EQUAL (B (S-UE (BN Z X))) (S-UE (B (BN Z X))))). This further simplifies, applying A2-BC-S-UE, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-BNC-S-UE (DEFN TOPOR-SY-A (LN) (IF (EQUAL LN 'YPC) 0 (IF (EQUAL LN 'YPCN) 1 (IF (EQUAL LN 'YPR) 1 (IF (EQUAL LN 'YI) 2 (IF (EQUAL LN 'YE) 3 (IF (EQUAL LN 'YOUT) 0 (IF (EQUAL LN 'YEC1) 0 (IF (EQUAL LN 'YEC) 0 0))))))))) From the definition we can conclude that (NUMBERP (TOPOR-SY-A LN)) is a theorem. [ 0.0 0.0 0.0 ] TOPOR-SY-A (DEFN SY-A (LN X) (IF (EQUAL LN 'YPC) (IF (EMPTY X) (E) (I 0 (SY-A 'YPCN (P X)))) (IF (EQUAL LN 'YPCN) (S-INC (SY-A 'YPC X)) (IF (EQUAL LN 'YPR) (S-UP (SY-A 'YPC X)) (IF (EQUAL LN 'YI) (S-UI (SY-A 'YPR X)) (IF (EQUAL LN 'YE) (S-UE (SY-A 'YI X)) (IF (EQUAL LN 'YOUT) (IF (EMPTY X) (E) (I 0 (SY-A 'YE (P X)))) (IF (EQUAL LN 'YEC1) (IF (EMPTY X) (E) (I (UE (UI 0)) (SY-A 'YE (P X)))) (IF (EQUAL LN 'YEC) (IF (EMPTY X) (E) (I (UE 0) (SY-A 'YEC1 (P X)))) (SFIX X))))))))) ((LEX2 (LIST (COUNT X) (TOPOR-SY-A LN))))) Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-A, CAR, LESSP, and EQUAL inform us that the measure (LIST (COUNT X) (TOPOR-SY-A LN)) decreases according to the well-founded relation LEX2 in each recursive call. Hence, SY-A is accepted under the principle of definition. Note that (STRINGP (SY-A LN X)) is a theorem. [ 0.0 0.0 0.0 ] SY-A (PROVE-LEMMA A2-EMPTY-SY-A (REWRITE) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X)) ((DISABLE S-INC S-UP S-UI S-UE))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (p 'YPR X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (p 'YI X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (p 'YEC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-A, CAR, LESSP, and EQUAL can be used to establish that the measure (LIST (COUNT X) (TOPOR-SY-A LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme generates the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, clearly, to the new goal: (IMPLIES (EMPTY X) (EMPTY (SY-A 'YPC X))), which further simplifies, unfolding the functions EQUAL, SY-A, and EMPTY, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YPCN (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, obviously, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YPCN (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-A 'YPC X)))), which further simplifies, applying A2-EMPTY-S-INC and STR-NOT-EMPTY-I, and expanding the functions EQUAL and SY-A, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (EMPTY (SY-A 'YPC X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-S-INC, and opening up EQUAL and SY-A, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (EMPTY (SY-A 'YPC X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, expanding the definition of EQUAL, to: (IMPLIES (EQUAL (EMPTY (SY-A 'YPC X)) (EMPTY X)) (EQUAL (EMPTY (SY-A 'YPR X)) (EMPTY X))). This further simplifies, rewriting with A2-EMPTY-S-UP, and expanding the functions EQUAL and SY-A, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (EQUAL (EMPTY (SY-A 'YPR X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, unfolding the function EQUAL, to: (IMPLIES (EQUAL (EMPTY (SY-A 'YPR X)) (EMPTY X)) (EQUAL (EMPTY (SY-A 'YI X)) (EMPTY X))), which further simplifies, applying A2-EMPTY-S-UP and A2-EMPTY-S-UI, and opening up EQUAL and SY-A, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (EQUAL (EMPTY (SY-A 'YI X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-S-UE, and expanding EQUAL and SY-A, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, expanding the definitions of EQUAL, SY-A, and EMPTY, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YE (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, applying STR-NOT-EMPTY-I, and opening up the functions EQUAL and SY-A, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, expanding the functions EQUAL, SY-A, and EMPTY, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YE (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, applying STR-NOT-EMPTY-I, and opening up the functions EQUAL and SY-A, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, opening up the functions EQUAL, SY-A, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YEC1 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, rewriting with STR-NOT-EMPTY-I, and opening up EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-SFIX, and unfolding the function SY-A, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-SY-A (PROVE-LEMMA A2-E-SY-A (REWRITE) (EQUAL (EQUAL (SY-A LN X) (E)) (EMPTY X)) ((DISABLE SY-A A2-EMPTY-SY-A) (ENABLE EMPTY) (USE (A2-EMPTY-SY-A)))) This formula simplifies, opening up the functions EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-SY-A (PROVE-LEMMA A2-LP-SY-A (REWRITE) (EQUAL (LEN (SY-A LN X)) (LEN X)) ((DISABLE LEN S-INC S-UP S-UI S-UE) (ENABLE STR-ADD1-LEN-P))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (p 'YPR X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (p 'YI X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (p 'YEC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-A, CAR, LESSP, and EQUAL can be used to establish that the measure (LIST (COUNT X) (TOPOR-SY-A LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme generates the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, clearly, to the new goal: (IMPLIES (EMPTY X) (EQUAL (LEN (SY-A 'YPC X)) (LEN X))), which further simplifies, rewriting with STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-A, and LEN, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YPCN (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, clearly, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YPCN (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A 'YPC X)) (LEN X))), which further simplifies, appealing to the lemmas A2-LP-S-INC, STR-ADD1-LEN-P, and STR-LEN-I, and opening up the definitions of EQUAL and SY-A, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (LEN (SY-A 'YPC X)) (LEN X))) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, applying the lemma A2-LP-S-INC, and expanding the definitions of EQUAL and SY-A, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (LEN (SY-A 'YPC X)) (LEN X))) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, expanding the function EQUAL, to: (IMPLIES (EQUAL (LEN (SY-A 'YPC X)) (LEN X)) (EQUAL (LEN (SY-A 'YPR X)) (LEN X))). But this further simplifies, rewriting with the lemma A2-LP-S-UP, and opening up EQUAL and SY-A, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (EQUAL (LEN (SY-A 'YPR X)) (LEN X))) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, expanding the function EQUAL, to: (IMPLIES (EQUAL (LEN (SY-A 'YPR X)) (LEN X)) (EQUAL (LEN (SY-A 'YI X)) (LEN X))). This further simplifies, applying A2-LP-S-UP and A2-LP-S-UI, and unfolding the definitions of EQUAL and SY-A, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (EQUAL (LEN (SY-A 'YI X)) (LEN X))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, applying A2-LP-S-UE, and expanding EQUAL and SY-A, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, appealing to the lemma STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-A, and LEN, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YE (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, applying STR-ADD1-LEN-P and STR-LEN-I, and expanding the functions EQUAL and SY-A, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, appealing to the lemma STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-A, and LEN, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YE (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, rewriting with the lemmas STR-ADD1-LEN-P and STR-LEN-I, and unfolding EQUAL and SY-A, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, rewriting with the lemma STR-LEN0-EMPTY, and unfolding the definitions of EQUAL, SY-A, and LEN, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YEC1 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, rewriting with STR-ADD1-LEN-P and STR-LEN-I, and unfolding EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, applying A2-LP-SFIX, and unfolding SY-A, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-SY-A (PROVE-LEMMA A2-LPE-SY-A (REWRITE) (EQLEN (SY-A LN X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN SY-A))) This conjecture can be simplified, using the abbreviations A2-LP-SY-A and EQLEN-IS-EQUAL-LEN, to: (EQUAL (LEN X) (LEN X)). This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-SY-A (PROVE-LEMMA A2-PC-SY-A (REWRITE) (EQUAL (P (SY-A LN X)) (SY-A LN (P X))) ((DISABLE S-INC S-UP S-UI S-UE A2-IC-S-INC A2-IC-S-UP A2-IC-S-UI A2-IC-S-UE))) . Applying the lemma P-L-ELIM, replace X by (A Z V) to eliminate (P X) and (L X). We employ the type restriction lemma noted when P was introduced to restrict the new variables. We thus obtain the following three new formulas: Case 3. (IMPLIES (EQUAL X (E)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, expanding SFIX, S-UE, S-UI, S-UP, S-INC, SY-A, EMPTY, P, and EQUAL, to: T. Case 2. (IMPLIES (NOT (STRINGP X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, applying P-NSTRINGP, and expanding the functions SFIX, S-UE, S-UI, S-UP, S-INC, SY-A, and EMPTY, to the new formula: (IMPLIES (NOT (STRINGP X)) (EQUAL (P (SY-A LN X)) (E))), 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: (EQUAL (P (SY-A LN X)) (SY-A LN (P X))). We named this *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (p 'YPR X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (p 'YI X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (p 'YEC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-A, CAR, LESSP, and EQUAL can be used to prove that the measure (LIST (COUNT X) (TOPOR-SY-A LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme leads to the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, applying the lemma STR-EMPTY-P, and unfolding the definitions of EQUAL and SY-A, to the new goal: (IMPLIES (EMPTY X) (EQUAL (P (SY-A 'YPC X)) (E))), which further simplifies, expanding EQUAL, SY-A, and P, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YPCN (P X))) (SY-A 'YPCN (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, expanding the functions EQUAL and SY-A, to two new goals: Case 12.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YPCN (P X))) (S-INC (SY-A 'YPC (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-A 'YPC X)) (I 0 (S-INC (SY-A 'YPC (P (P X))))))), which further simplifies, rewriting with the lemmas A2-PC-S-INC, A2-EMPTY-S-INC, STR-NOT-EMPTY-I, and STR-P-I, and opening up the functions EQUAL and SY-A, to: T. Case 12.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YPCN (P X))) (S-INC (SY-A 'YPC (P (P X))))) (EMPTY (P X))) (EQUAL (P (SY-A 'YPC X)) (E))), which again simplifies, rewriting with the lemma STR-EMPTY-P, and opening up the functions EQUAL, SY-A, and S-INC, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YPCN (P X))) (E)) (EMPTY (P X))) (EQUAL (P (SY-A 'YPC X)) (E))). But this further simplifies, opening up the definitions of EQUAL, SY-A, S-INC, P, and I, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (P (SY-A 'YPC X)) (SY-A 'YPC (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, applying the lemma A2-PC-S-INC, and expanding the functions EQUAL and SY-A, to: (IMPLIES (EQUAL (P (SY-A 'YPC X)) (SY-A 'YPC (P X))) (EQUAL (S-INC (P (SY-A 'YPC X))) (SY-A 'YPCN (P X)))). However this further simplifies, applying STR-EMPTY-P and A2-E-S-INC, and unfolding EQUAL, SY-A, P, S-INC, and EMPTY, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (P (SY-A 'YPC X)) (SY-A 'YPC (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, expanding the functions EQUAL and SY-A, to: (IMPLIES (EQUAL (P (SY-A 'YPC X)) (SY-A 'YPC (P X))) (EQUAL (P (SY-A 'YPR X)) (S-UP (P (SY-A 'YPC X))))), which further simplifies, applying the lemma A2-PC-S-UP, and expanding the functions EQUAL, SY-A, S-UP, and P, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YI) (EQUAL (P (SY-A 'YPR X)) (SY-A 'YPR (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, unfolding EQUAL and SY-A, to: (IMPLIES (EQUAL (P (SY-A 'YPR X)) (S-UP (SY-A 'YPC (P X)))) (EQUAL (P (SY-A 'YI X)) (S-UI (S-UP (SY-A 'YPC (P X)))))). This further simplifies, applying A2-PC-S-UP, A2-PC-S-UI, and STR-EMPTY-P, and unfolding EQUAL, SY-A, S-UP, S-UI, and P, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YE) (EQUAL (P (SY-A 'YI X)) (SY-A 'YI (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, appealing to the lemma A2-PC-S-UE, and unfolding the definitions of EQUAL and SY-A, to the new goal: (IMPLIES (EQUAL (P (SY-A 'YI X)) (S-UI (S-UP (SY-A 'YPC (P X))))) (EQUAL (S-UE (P (SY-A 'YI X))) (SY-A 'YE (P X)))), which further simplifies, applying the lemmas A2-PC-S-UP, A2-PC-S-UI, and STR-EMPTY-P, and unfolding the definitions of EQUAL, SY-A, S-UP, S-UI, P, and S-UE, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, rewriting with the lemma STR-EMPTY-P, and unfolding the definitions of EQUAL, SY-A, and P, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YE (P X))) (SY-A 'YE (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, expanding EQUAL and SY-A, to two new formulas: Case 6.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YE (P X))) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X))))))) (NOT (EMPTY (P X)))) (EQUAL (P (I 0 (SY-A 'YE (P X)))) (I 0 (P (SY-A 'YE (P X)))))), which again simplifies, rewriting with A2-EMPTY-SY-A and STR-P-I, to: T. Case 6.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YE (P X))) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X))))))) (EMPTY (P X))) (EQUAL (P (I 0 (SY-A 'YE (P X)))) (E))). However this again simplifies, applying STR-EMPTY-P, A2-EMPTY-SY-A, and STR-P-I-E, and unfolding the functions EQUAL, SY-A, S-UP, S-UI, and S-UE, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, rewriting with STR-EMPTY-P and A2-E-SY-A, and expanding EQUAL, SY-A, and P, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (EQUAL LN 'YEC1) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YE (P X))) (SY-A 'YE (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, expanding EQUAL and SY-A, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YE (P X))) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))) (EQUAL (P (I (UE (UI 0)) (SY-A 'YE (P X)))) (SY-A 'YEC1 (P X)))). However this further simplifies, appealing to the lemmas A2-PC-S-UP, A2-PC-S-UI, A2-PC-S-UE, A2-EMPTY-S-UE, A2-EMPTY-S-UI, A2-EMPTY-S-UP, STR-NOT-EMPTY-I, STR-P-I, STR-I-E, and P-A, and expanding the functions EQUAL, SY-A, S-UP, S-UI, S-UE, and STRINGP, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, rewriting with STR-EMPTY-P, and opening up the functions EQUAL, SY-A, and P, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (EQUAL LN 'YEC) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YEC1 (P X))) (SY-A 'YEC1 (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, unfolding the functions EQUAL and SY-A, to the following two new conjectures: Case 2.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YEC1 (P X))) (SY-A 'YEC1 (P (P X)))) (NOT (EMPTY (P X)))) (EQUAL (P (I (UE 0) (SY-A 'YEC1 (P X)))) (I (UE 0) (P (SY-A 'YEC1 (P X)))))). But this again simplifies, rewriting with A2-EMPTY-SY-A and STR-P-I, to: T. Case 2.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YEC1 (P X))) (SY-A 'YEC1 (P (P X)))) (EMPTY (P X))) (EQUAL (P (I (UE 0) (SY-A 'YEC1 (P X)))) (E))). However this again simplifies, applying STR-EMPTY-P, A2-EMPTY-SY-A, and STR-P-I-E, and expanding the functions EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT)) (NOT (EQUAL LN 'YEC1)) (NOT (EQUAL LN 'YEC))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, rewriting with A2-PC-SFIX, and unfolding SY-A, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.2 ] A2-PC-SY-A (DEFN TOPOR-SY-B (LN) (IF (EQUAL LN 'YPC) 0 (IF (EQUAL LN 'YPCN) 1 (IF (EQUAL LN 'YPR) 1 (IF (EQUAL LN 'YPR2) 0 (IF (EQUAL LN 'YI) 1 (IF (EQUAL LN 'YI2) 0 (IF (EQUAL LN 'YE) 1 (IF (EQUAL LN 'YOUT) 0 0))))))))) From the definition we can conclude that (NUMBERP (TOPOR-SY-B LN)) is a theorem. [ 0.0 0.0 0.0 ] TOPOR-SY-B (DEFN SY-B (LN X) (IF (EQUAL LN 'YPC) (IF (EMPTY X) (E) (I 0 (SY-B 'YPCN (P X)))) (IF (EQUAL LN 'YPCN) (S-INC (SY-B 'YPC X)) (IF (EQUAL LN 'YPR) (S-UP (SY-B 'YPC X)) (IF (EQUAL LN 'YPR2) (IF (EMPTY X) (E) (I 0 (SY-B 'YPR (P X)))) (IF (EQUAL LN 'YI) (S-UI (SY-B 'YPR2 X)) (IF (EQUAL LN 'YI2) (IF (EMPTY X) (E) (I 0 (SY-B 'YI (P X)))) (IF (EQUAL LN 'YE) (S-UE (SY-B 'YI2 X)) (IF (EQUAL LN 'YOUT) (IF (EMPTY X) (E) (I 0 (SY-B 'YE (P X)))) (SFIX X))))))))) ((LEX2 (LIST (COUNT X) (TOPOR-SY-B LN))))) Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-B, CAR, LESSP, and EQUAL inform us that the measure (LIST (COUNT X) (TOPOR-SY-B LN)) decreases according to the well-founded relation LEX2 in each recursive call. Hence, SY-B is accepted under the principle of definition. Observe that (STRINGP (SY-B LN X)) is a theorem. [ 0.0 0.0 0.0 ] SY-B (PROVE-LEMMA A2-EMPTY-SY-B (REWRITE) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X)) ((DISABLE S-INC S-UP S-UI S-UE))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (p 'YPR (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (p 'YPR2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (p 'YI (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (p 'YI2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-B, CAR, LESSP, and EQUAL can be used to establish that the measure (LIST (COUNT X) (TOPOR-SY-B LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme generates the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, clearly, to the new goal: (IMPLIES (EMPTY X) (EMPTY (SY-B 'YPC X))), which further simplifies, unfolding the functions EQUAL, SY-B, and EMPTY, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YPCN (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, obviously, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YPCN (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-B 'YPC X)))), which further simplifies, applying A2-EMPTY-S-INC and STR-NOT-EMPTY-I, and expanding the functions EQUAL and SY-B, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (EMPTY (SY-B 'YPC X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-S-INC, and opening up EQUAL and SY-B, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (EMPTY (SY-B 'YPC X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, applying A2-EMPTY-S-UP, and expanding EQUAL and SY-B, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, opening up EQUAL, to: (IMPLIES (EMPTY X) (EMPTY (SY-B 'YPR2 X))), which further simplifies, opening up EQUAL, SY-B, and EMPTY, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YPR (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, unfolding the function EQUAL, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YPR (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-B 'YPR2 X)))). However this further simplifies, applying A2-EMPTY-S-UP and STR-NOT-EMPTY-I, and expanding the definitions of EQUAL and SY-B, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (EQUAL (EMPTY (SY-B 'YPR2 X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-S-UI, and expanding the definitions of EQUAL and SY-B, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, expanding the function EQUAL, to the goal: (IMPLIES (EMPTY X) (EMPTY (SY-B 'YI2 X))). But this further simplifies, expanding the definitions of EQUAL, SY-B, and EMPTY, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YI (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, unfolding the function EQUAL, to the conjecture: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YI (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-B 'YI2 X)))). However this further simplifies, rewriting with A2-EMPTY-S-UI and STR-NOT-EMPTY-I, and unfolding EQUAL and SY-B, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (EQUAL (EMPTY (SY-B 'YI2 X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, rewriting with the lemma A2-EMPTY-S-UE, and unfolding the definitions of EQUAL and SY-B, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, unfolding EQUAL, SY-B, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'YE (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, rewriting with STR-NOT-EMPTY-I, and expanding EQUAL and SY-B, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, appealing to the lemma A2-EMPTY-SFIX, and unfolding SY-B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-EMPTY-SY-B (PROVE-LEMMA A2-E-SY-B (REWRITE) (EQUAL (EQUAL (SY-B LN X) (E)) (EMPTY X)) ((DISABLE SY-B A2-EMPTY-SY-B) (ENABLE EMPTY) (USE (A2-EMPTY-SY-B)))) This formula simplifies, opening up the functions EMPTY and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-E-SY-B (PROVE-LEMMA A2-LP-SY-B (REWRITE) (EQUAL (LEN (SY-B LN X)) (LEN X)) ((DISABLE LEN S-INC S-UP S-UI S-UE) (ENABLE STR-ADD1-LEN-P))) Call the conjecture *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (p 'YPR (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (p 'YPR2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (p 'YI (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (p 'YI2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-B, CAR, LESSP, and EQUAL can be used to establish that the measure (LIST (COUNT X) (TOPOR-SY-B LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme generates the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, clearly, to the new goal: (IMPLIES (EMPTY X) (EQUAL (LEN (SY-B 'YPC X)) (LEN X))), which further simplifies, rewriting with STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-B, and LEN, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YPCN (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, clearly, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YPCN (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B 'YPC X)) (LEN X))), which further simplifies, appealing to the lemmas A2-LP-S-INC, STR-ADD1-LEN-P, and STR-LEN-I, and opening up the definitions of EQUAL and SY-B, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (LEN (SY-B 'YPC X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying the lemma A2-LP-S-INC, and expanding the definitions of EQUAL and SY-B, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (LEN (SY-B 'YPC X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying A2-LP-S-UP, and opening up EQUAL and SY-B, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, opening up the function EQUAL, to: (IMPLIES (EMPTY X) (EQUAL (LEN (SY-B 'YPR2 X)) (LEN X))), which further simplifies, rewriting with STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-B, and LEN, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YPR (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, opening up the definition of EQUAL, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YPR (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B 'YPR2 X)) (LEN X))), which further simplifies, applying A2-LP-S-UP, STR-ADD1-LEN-P, and STR-LEN-I, and expanding the definitions of EQUAL and SY-B, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (EQUAL (LEN (SY-B 'YPR2 X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, rewriting with A2-LP-S-UI, and expanding the functions EQUAL and SY-B, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, opening up the definition of EQUAL, to the conjecture: (IMPLIES (EMPTY X) (EQUAL (LEN (SY-B 'YI2 X)) (LEN X))). But this further simplifies, rewriting with STR-LEN0-EMPTY, and opening up the functions EQUAL, SY-B, and LEN, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YI (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, expanding EQUAL, to the new formula: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YI (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B 'YI2 X)) (LEN X))), which further simplifies, rewriting with A2-LP-S-UI, STR-ADD1-LEN-P, and STR-LEN-I, and opening up EQUAL and SY-B, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (EQUAL (LEN (SY-B 'YI2 X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, applying A2-LP-S-UE, and opening up EQUAL and SY-B, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying STR-LEN0-EMPTY, and unfolding the definitions of EQUAL, SY-B, and LEN, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'YE (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, rewriting with STR-ADD1-LEN-P and STR-LEN-I, and opening up the functions EQUAL and SY-B, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying A2-LP-SFIX, and unfolding the function SY-B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-LP-SY-B (PROVE-LEMMA A2-LPE-SY-B (REWRITE) (EQLEN (SY-B LN X) X) ((ENABLE EQLEN-IS-EQUAL-LEN) (DISABLE LEN SY-B))) This conjecture can be simplified, using the abbreviations A2-LP-SY-B and EQLEN-IS-EQUAL-LEN, to: (EQUAL (LEN X) (LEN X)). This simplifies, obviously, to: T. Q.E.D. [ 0.0 0.0 0.0 ] A2-LPE-SY-B (PROVE-LEMMA A2-PC-SY-B (REWRITE) (EQUAL (P (SY-B LN X)) (SY-B LN (P X))) ((DISABLE S-INC S-UP S-UI S-UE A2-IC-S-INC A2-IC-S-UP A2-IC-S-UI A2-IC-S-UE))) . Applying the lemma P-L-ELIM, replace X by (A Z V) to eliminate (P X) and (L X). We employ the type restriction lemma noted when P was introduced to restrict the new variables. We thus obtain the following three new formulas: Case 3. (IMPLIES (EQUAL X (E)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, expanding SFIX, S-UE, S-UI, S-UP, S-INC, SY-B, EMPTY, P, and EQUAL, to: T. Case 2. (IMPLIES (NOT (STRINGP X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying P-NSTRINGP, and expanding the functions SFIX, S-UE, S-UI, S-UP, S-INC, SY-B, and EMPTY, to the new formula: (IMPLIES (NOT (STRINGP X)) (EQUAL (P (SY-B LN X)) (E))), 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: (EQUAL (P (SY-B LN X)) (SY-B LN (P X))). We named this *1. We will try to prove it by induction. There is only one suggested induction. We will induct according to the following scheme: (AND (IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (p LN X)) (IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (p 'YPCN (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (p 'YPC X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (p 'YPR (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (p 'YPR2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (p 'YI (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (p 'YI2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YE (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, STR-EMPTY-COUNT, P-LESSEQP, and CDR-CONS, and the definitions of LEX2, CONS, TOPOR-SY-B, CAR, LESSP, and EQUAL can be used to prove that the measure (LIST (COUNT X) (TOPOR-SY-B LN)) decreases according to the well-founded relation LEX2 in each induction step of the scheme. The above induction scheme leads to the following 13 new formulas: Case 13.(IMPLIES (AND (EQUAL LN 'YPC) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, applying the lemma STR-EMPTY-P, and unfolding the definitions of EQUAL and SY-B, to the new goal: (IMPLIES (EMPTY X) (EQUAL (P (SY-B 'YPC X)) (E))), which further simplifies, expanding EQUAL, SY-B, and P, to: T. Case 12.(IMPLIES (AND (EQUAL LN 'YPC) (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPCN (P X))) (SY-B 'YPCN (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, expanding the functions EQUAL and SY-B, to two new goals: Case 12.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPCN (P X))) (S-INC (SY-B 'YPC (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-B 'YPC X)) (I 0 (S-INC (SY-B 'YPC (P (P X))))))), which further simplifies, rewriting with the lemmas A2-PC-S-INC, A2-EMPTY-S-INC, STR-NOT-EMPTY-I, and STR-P-I, and opening up the functions EQUAL and SY-B, to: T. Case 12.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPCN (P X))) (S-INC (SY-B 'YPC (P (P X))))) (EMPTY (P X))) (EQUAL (P (SY-B 'YPC X)) (E))), which again simplifies, rewriting with the lemma STR-EMPTY-P, and opening up the functions EQUAL, SY-B, and S-INC, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPCN (P X))) (E)) (EMPTY (P X))) (EQUAL (P (SY-B 'YPC X)) (E))). But this further simplifies, opening up the definitions of EQUAL, SY-B, S-INC, P, and I, to: T. Case 11.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (EQUAL LN 'YPCN) (EQUAL (P (SY-B 'YPC X)) (SY-B 'YPC (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying the lemma A2-PC-S-INC, and expanding the functions EQUAL and SY-B, to: (IMPLIES (EQUAL (P (SY-B 'YPC X)) (SY-B 'YPC (P X))) (EQUAL (S-INC (P (SY-B 'YPC X))) (SY-B 'YPCN (P X)))). However this further simplifies, applying STR-EMPTY-P and A2-E-S-INC, and unfolding EQUAL, SY-B, P, S-INC, and EMPTY, to: T. Case 10.(IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (EQUAL LN 'YPR) (EQUAL (P (SY-B 'YPC X)) (SY-B 'YPC (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, applying A2-PC-S-UP, and opening up the definitions of EQUAL and SY-B, to: (IMPLIES (EQUAL (P (SY-B 'YPC X)) (SY-B 'YPC (P X))) (EQUAL (S-UP (P (SY-B 'YPC X))) (SY-B 'YPR (P X)))). But this further simplifies, applying STR-EMPTY-P and A2-E-S-UP, and opening up the functions EQUAL, SY-B, P, S-UP, and EMPTY, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, rewriting with STR-EMPTY-P, and expanding the definitions of EQUAL and SY-B, to: (IMPLIES (EMPTY X) (EQUAL (P (SY-B 'YPR2 X)) (E))). This further simplifies, unfolding EQUAL, SY-B, and P, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (EQUAL LN 'YPR2) (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPR (P X))) (SY-B 'YPR (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, opening up EQUAL and SY-B, to two new goals: Case 8.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPR (P X))) (S-UP (SY-B 'YPC (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-B 'YPR2 X)) (I 0 (S-UP (SY-B 'YPC (P (P X))))))), which further simplifies, applying A2-PC-S-UP, A2-EMPTY-S-UP, STR-NOT-EMPTY-I, and STR-P-I, and expanding the functions EQUAL and SY-B, to: T. Case 8.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPR (P X))) (S-UP (SY-B 'YPC (P (P X))))) (EMPTY (P X))) (EQUAL (P (SY-B 'YPR2 X)) (E))). However this again simplifies, rewriting with STR-EMPTY-P, and unfolding the functions EQUAL, SY-B, and S-UP, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YPR (P X))) (E)) (EMPTY (P X))) (EQUAL (P (SY-B 'YPR2 X)) (E))), which further simplifies, opening up the functions EQUAL, SY-B, S-UP, P, and I, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (EQUAL LN 'YI) (EQUAL (P (SY-B 'YPR2 X)) (SY-B 'YPR2 (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, rewriting with A2-PC-S-UI, and unfolding the functions EQUAL and SY-B, to the new goal: (IMPLIES (EQUAL (P (SY-B 'YPR2 X)) (SY-B 'YPR2 (P X))) (EQUAL (S-UI (P (SY-B 'YPR2 X))) (SY-B 'YI (P X)))), which further simplifies, applying STR-EMPTY-P and A2-E-S-UI, and unfolding the functions EQUAL, SY-B, P, S-UI, and EMPTY, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, rewriting with STR-EMPTY-P, and expanding EQUAL and SY-B, to the conjecture: (IMPLIES (EMPTY X) (EQUAL (P (SY-B 'YI2 X)) (E))). However this further simplifies, unfolding EQUAL, SY-B, and P, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (EQUAL LN 'YI2) (NOT (EMPTY X)) (EQUAL (P (SY-B 'YI (P X))) (SY-B 'YI (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, expanding the functions EQUAL and SY-B, to two new goals: Case 5.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YI (P X))) (S-UI (SY-B 'YPR2 (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-B 'YI2 X)) (I 0 (P (SY-B 'YI (P X)))))), which further simplifies, applying the lemmas A2-PC-S-UI, A2-EMPTY-S-UI, STR-NOT-EMPTY-I, and STR-P-I, and unfolding EQUAL and SY-B, to: T. Case 5.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YI (P X))) (S-UI (SY-B 'YPR2 (P (P X))))) (EMPTY (P X))) (EQUAL (P (SY-B 'YI2 X)) (E))), which again simplifies, applying STR-EMPTY-P, and expanding the functions EQUAL, SY-B, and S-UI, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YI (P X))) (E)) (EMPTY (P X))) (EQUAL (P (SY-B 'YI2 X)) (E))), which further simplifies, unfolding the functions EQUAL, SY-B, S-UI, P, and I, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (EQUAL LN 'YE) (EQUAL (P (SY-B 'YI2 X)) (SY-B 'YI2 (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, rewriting with the lemma A2-PC-S-UE, and expanding EQUAL and SY-B, to: (IMPLIES (EQUAL (P (SY-B 'YI2 X)) (SY-B 'YI2 (P X))) (EQUAL (S-UE (P (SY-B 'YI2 X))) (SY-B 'YE (P X)))). But this further simplifies, applying the lemmas STR-EMPTY-P and A2-E-S-UE, and unfolding the definitions of EQUAL, SY-B, P, S-UE, and EMPTY, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying STR-EMPTY-P, and opening up the definitions of EQUAL, SY-B, and P, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (P (SY-B 'YE (P X))) (SY-B 'YE (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, expanding the definitions of EQUAL and SY-B, to the following two new goals: Case 2.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YE (P X))) (S-UE (SY-B 'YI2 (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (I 0 (SY-B 'YE (P X)))) (I 0 (P (SY-B 'YE (P X)))))). This again simplifies, rewriting with A2-EMPTY-SY-B and STR-P-I, to: T. Case 2.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'YE (P X))) (S-UE (SY-B 'YI2 (P (P X))))) (EMPTY (P X))) (EQUAL (P (I 0 (SY-B 'YE (P X)))) (E))). This again simplifies, applying STR-EMPTY-P, A2-EMPTY-SY-B, and STR-P-I-E, and unfolding EQUAL, SY-B, and S-UE, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'YPC)) (NOT (EQUAL LN 'YPCN)) (NOT (EQUAL LN 'YPR)) (NOT (EQUAL LN 'YPR2)) (NOT (EQUAL LN 'YI)) (NOT (EQUAL LN 'YI2)) (NOT (EQUAL LN 'YE)) (NOT (EQUAL LN 'YOUT))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, rewriting with the lemma A2-PC-SFIX, and expanding the definition of SY-B, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] A2-PC-SY-B (PROVE-LEMMA EQ-PC (REWRITE) (EQUAL (SY-B 'YPC X) (SY-A 'YPC X)) ((INDUCT (INDUCT-P X)))) This formula can be simplified, using the abbreviations NOT, OR, and AND, to the following two new formulas: Case 2. (IMPLIES (EMPTY X) (EQUAL (SY-B 'YPC X) (SY-A 'YPC X))). This simplifies, expanding the functions EQUAL, SY-B, and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (SY-B 'YPC (P X)) (SY-A 'YPC (P X)))) (EQUAL (SY-B 'YPC X) (SY-A 'YPC X))). Appealing to the lemma P-L-ELIM, we now replace X by (A Z V) to eliminate (P X) and (L X). We use the type restriction lemma noted when P was introduced to constrain the new variables. The result is three new conjectures: Case 1.3. (IMPLIES (AND (EQUAL X (E)) (NOT (EMPTY X)) (EQUAL (SY-B 'YPC (P X)) (SY-A 'YPC (P X)))) (EQUAL (SY-B 'YPC X) (SY-A 'YPC X))), which simplifies, expanding the definition of EMPTY, to: T. Case 1.2. (IMPLIES (AND (NOT (STRINGP X)) (NOT (EMPTY X)) (EQUAL (SY-B 'YPC (P X)) (SY-A 'YPC (P X)))) (EQUAL (SY-B 'YPC X) (SY-A 'YPC X))), which simplifies, applying P-NSTRINGP, and expanding the functions SY-B, SY-A, EQUAL, and I, to: T. Case 1.1. (IMPLIES (AND (STRINGP Z) (NOT (EQUAL (A Z V) (E))) (NOT (EMPTY (A Z V))) (EQUAL (SY-B 'YPC Z) (SY-A 'YPC Z))) (EQUAL (SY-B 'YPC (A Z V)) (SY-A 'YPC (A Z V)))). This simplifies, applying the lemmas STR-NOT-EMPTY-A and P-A, and unfolding the functions EQUAL, SY-B, and SY-A, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-PC (PROVE-LEMMA EQ-A-B NIL (EQUAL (SY-B 'YE X) (SY-A 'YEC X)) ((EXPAND (SY-B 'YE X) (SY-A 'YEC X) (SY-B 'YI2 X) (SY-A 'YEC1 (P X)) (SY-B 'YI (P X)) (SY-A 'YE (P (P X))) (SY-B 'YPR2 (P X)) (SY-A 'YI (P (P X))) (SY-B 'YPR (P (P X))) (SY-A 'YPR (P (P X)))))) This conjecture simplifies, applying EQ-PC, and unfolding the functions SY-B, EQUAL, and SY-A, to three new goals: Case 3. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (S-UE (I 0 (S-UI (E)))) (I (UE 0) (E)))), which again simplifies, applying STR-I-E, and expanding the definitions of S-UI, I, L, S-UE, P, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X)))) (EQUAL (S-UE (I 0 (S-UI (I 0 (S-UP (SY-A 'YPC (P (P X)))))))) (I (UE 0) (I (UE (UI 0)) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))))). This again simplifies, applying A2-IC-S-UI and A2-IC-S-UE, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (S-UE (E)) (E))). But this again simplifies, opening up S-UE and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-A-B (PROVE-LEMMA EQ-A-B2 NIL (EQUAL (SY-B 'YE X) (IF (EMPTY X) (E) (I (UE 0) (IF (EMPTY (P X)) (E) (I (UE (UI 0)) (SY-A 'YE (P (P X)))))))) ((EXPAND (SY-B 'YE X) (SY-B 'YI2 X) (SY-B 'YI (P X)) (SY-A 'YE (P (P X))) (SY-B 'YPR2 (P X)) (SY-A 'YI (P (P X))) (SY-B 'YPR (P (P X))) (SY-A 'YPR (P (P X)))))) This conjecture simplifies, rewriting with EQ-PC, and expanding the functions SY-B, EQUAL, and SY-A, to three new goals: Case 3. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (S-UE (I 0 (S-UI (E)))) (I (UE 0) (E)))), which again simplifies, rewriting with STR-I-E, and expanding S-UI, I, L, S-UE, P, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X)))) (EQUAL (S-UE (I 0 (S-UI (I 0 (S-UP (SY-A 'YPC (P (P X)))))))) (I (UE 0) (I (UE (UI 0)) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))))). But this again simplifies, applying A2-IC-S-UI and A2-IC-S-UE, to: T. Case 1. (IMPLIES (EMPTY X) (EQUAL (S-UE (E)) (E))). This again simplifies, expanding the definitions of S-UE and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-A-B2 (PROVE-LEMMA EQ-A-B3 NIL (IMPLIES (NOT (EMPTY (P X))) (EQUAL (SY-B 'YE X) (I (UE 0) (I (UE (UI 0)) (SY-A 'YE (P (P X))))))) ((EXPAND (SY-B 'YE X) (SY-B 'YI2 X) (SY-B 'YI (P X)) (SY-A 'YE (P (P X))) (SY-B 'YPR2 (P X)) (SY-A 'YI (P (P X))) (SY-B 'YPR (P (P X))) (SY-A 'YPR (P (P X)))))) This formula simplifies, rewriting with EQ-PC and A2-IC-S-UI, and expanding the definitions of SY-B, EQUAL, and SY-A, to the following two new conjectures: Case 2. (IMPLIES (AND (NOT (EMPTY (P X))) (NOT (EMPTY X))) (EQUAL (S-UE (I 0 (I (UI 0) (S-UI (S-UP (SY-A 'YPC (P (P X)))))))) (I (UE 0) (I (UE (UI 0)) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))))). This again simplifies, rewriting with A2-IC-S-UE, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EMPTY X)) (EQUAL (S-UE (E)) (I (UE 0) (I (UE (UI 0)) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))))). This again simplifies, rewriting with STR-EMPTY-P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-A-B3 (PROVE-LEMMA EQ-A-B4 NIL (IMPLIES (NOT (EMPTY (P X))) (EQUAL (B (B (SY-B 'YE X))) (SY-A 'YE (P (P X))))) ((EXPAND (SY-B 'YE X) (SY-B 'YI2 X) (SY-B 'YI (P X)) (SY-A 'YE (P (P X))) (SY-B 'YPR2 (P X)) (SY-A 'YI (P (P X))) (SY-B 'YPR (P (P X))) (SY-A 'YPR (P (P X)))))) This conjecture simplifies, rewriting with the lemmas EQ-PC, A2-IC-S-UI, and A2-BC-S-UE, and unfolding the functions SY-B, EQUAL, and SY-A, to two new formulas: Case 2. (IMPLIES (AND (NOT (EMPTY (P X))) (NOT (EMPTY X))) (EQUAL (S-UE (B (B (I 0 (I (UI 0) (S-UI (S-UP (SY-A 'YPC (P (P X)))))))))) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))), which again simplifies, rewriting with STR-B-I, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY (P X))) (EMPTY X)) (EQUAL (S-UE (B (B (E)))) (S-UE (S-UI (S-UP (SY-A 'YPC (P (P X)))))))). But this again simplifies, rewriting with STR-EMPTY-P, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-A-B4