(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 (DEFN TOPOR-SY-A (LN) (IF (EQUAL LN 'Y1) 1 (IF (EQUAL LN 'Y2) 2 (IF (EQUAL LN 'Y3) 3 (IF (EQUAL LN 'YC2) 0 (IF (EQUAL LN 'YC1) 0 (IF (EQUAL LN 'YOUT) 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 'Y1) (S-INC X) (IF (EQUAL LN 'Y2) (S-INC (SY-A 'Y1 X)) (IF (EQUAL LN 'Y3) (S-INC (SY-A 'Y2 X)) (IF (EQUAL LN 'YC2) (IF (EMPTY X) (E) (I 2 (SY-A 'Y3 (P X)))) (IF (EQUAL LN 'YC1) (IF (EMPTY X) (E) (I 1 (SY-A 'YC2 (P X)))) (IF (EQUAL LN 'YOUT) (IF (EMPTY X) (E) (I 0 (SY-A 'YC1 (P X)))) (SFIX X))))))) ((LEX2 (LIST (COUNT X) (TOPOR-SY-A LN))))) Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, STR-EMPTY-COUNT, and P-LESSEQP, and the definitions of LEX2, CAR, LESSP, CONS, TOPOR-SY-A, 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 recursive call. Hence, SY-A is accepted under the definitional principle. From the definition we can conclude 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))) 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 (EQUAL LN 'Y1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (p 'Y1 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (p 'Y2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (p 'Y3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (p 'YC2 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, STR-EMPTY-COUNT, and P-LESSEQP, and the definitions of LEX2, CAR, LESSP, CONS, TOPOR-SY-A, 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Y1) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, clearly, to the new goal: (EQUAL (EMPTY (SY-A 'Y1 X)) (EMPTY X)), which further simplifies, rewriting with A2-EMPTY-S-INC, and opening up the definitions of EQUAL and SY-A, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (EQUAL (EMPTY (SY-A 'Y1 X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, expanding the definition of EQUAL, to: (IMPLIES (EQUAL (EMPTY (SY-A 'Y1 X)) (EMPTY X)) (EQUAL (EMPTY (SY-A 'Y2 X)) (EMPTY X))), which further simplifies, appealing to the lemma A2-EMPTY-S-INC, and opening up the definitions of EQUAL and SY-A, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (EQUAL (EMPTY (SY-A 'Y2 X)) (EMPTY X))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, applying the lemma A2-EMPTY-S-INC, and expanding the definitions of EQUAL and SY-A, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, expanding the functions EQUAL, SY-A, and EMPTY, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'Y3 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, appealing to the lemma STR-NOT-EMPTY-I, and opening up EQUAL and SY-A, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, unfolding the functions EQUAL, SY-A, and EMPTY, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YC2 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, rewriting with STR-NOT-EMPTY-I, and opening up the definitions of EQUAL and SY-A, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, unfolding the definitions of EQUAL, SY-A, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-A 'YC1 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))). This simplifies, applying STR-NOT-EMPTY-I, and expanding EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (EQUAL (EMPTY (SY-A LN X)) (EMPTY X))), which simplifies, appealing to the lemma A2-EMPTY-SFIX, and opening up the definition of 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) (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 (EQUAL LN 'Y1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (p 'Y1 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (p 'Y2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (p 'Y3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (p 'YC2 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, STR-EMPTY-COUNT, and P-LESSEQP, and the definitions of LEX2, CAR, LESSP, CONS, TOPOR-SY-A, 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Y1) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, clearly, to the new goal: (EQUAL (LEN (SY-A 'Y1 X)) (LEN X)), which further simplifies, rewriting with A2-LP-S-INC, and opening up the definitions of EQUAL and SY-A, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (EQUAL (LEN (SY-A 'Y1 X)) (LEN X))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, expanding the definition of EQUAL, to: (IMPLIES (EQUAL (LEN (SY-A 'Y1 X)) (LEN X)) (EQUAL (LEN (SY-A 'Y2 X)) (LEN X))), which further simplifies, appealing to the lemma A2-LP-S-INC, and opening up the definitions of EQUAL and SY-A, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (EQUAL (LEN (SY-A 'Y2 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 7. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, applying STR-LEN0-EMPTY, and opening up EQUAL, SY-A, and LEN, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'Y3 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, appealing to the lemmas STR-ADD1-LEN-P and STR-LEN-I, and unfolding the functions EQUAL and SY-A, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, applying the lemma STR-LEN0-EMPTY, and opening up EQUAL, SY-A, and LEN, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YC2 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, applying STR-ADD1-LEN-P and STR-LEN-I, and expanding EQUAL and SY-A, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (LEN (SY-A LN X)) (LEN X))), which simplifies, applying STR-LEN0-EMPTY, and expanding the definitions of EQUAL, SY-A, and LEN, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (LEN (SY-A 'YC1 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, appealing to the lemmas STR-ADD1-LEN-P and STR-LEN-I, and opening up the functions EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (EQUAL (LEN (SY-A LN X)) (LEN X))). This simplifies, applying A2-LP-SFIX, and expanding the definition of 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 A2-IC-S-INC))) . 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, EMPTY, SY-A, S-INC, 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, EMPTY, SY-A, and S-INC, 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 (EQUAL LN 'Y1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (p 'Y1 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (p 'Y2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (p 'Y3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (p 'YC2 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (p 'YC1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (p LN X))). Linear arithmetic, the lemmas CAR-CONS, CDR-CONS, STR-EMPTY-COUNT, and P-LESSEQP, and the definitions of LEX2, CAR, LESSP, CONS, TOPOR-SY-A, 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Y1) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, opening up the definitions of EQUAL and SY-A, to: (EQUAL (P (SY-A 'Y1 X)) (S-INC (P X))), which further simplifies, applying A2-PC-S-INC, and opening up EQUAL and SY-A, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (EQUAL LN 'Y2) (EQUAL (P (SY-A 'Y1 X)) (SY-A 'Y1 (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, unfolding the functions EQUAL and SY-A, to the new goal: (IMPLIES (EQUAL (P (SY-A 'Y1 X)) (S-INC (P X))) (EQUAL (P (SY-A 'Y2 X)) (S-INC (S-INC (P X))))), which further simplifies, appealing to the lemma A2-PC-S-INC, and opening up EQUAL and SY-A, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (EQUAL LN 'Y3) (EQUAL (P (SY-A 'Y2 X)) (SY-A 'Y2 (P X)))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, appealing to the lemma A2-PC-S-INC, and opening up EQUAL and SY-A, to the conjecture: (IMPLIES (EQUAL (P (SY-A 'Y2 X)) (S-INC (S-INC (P X)))) (EQUAL (S-INC (S-INC (S-INC (P X)))) (SY-A 'Y3 (P X)))). But this further simplifies, applying the lemma A2-PC-S-INC, and unfolding the definitions of EQUAL and SY-A, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, applying STR-EMPTY-P and A2-E-SY-A, and opening up the definitions of EQUAL, SY-A, and P, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (EQUAL LN 'YC2) (NOT (EMPTY X)) (EQUAL (P (SY-A 'Y3 (P X))) (SY-A 'Y3 (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, unfolding the definitions of EQUAL and SY-A, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'Y3 (P X))) (S-INC (S-INC (S-INC (P (P X))))))) (EQUAL (P (I 2 (SY-A 'Y3 (P X)))) (SY-A 'YC2 (P X)))), which further simplifies, applying the lemma A2-PC-S-INC, and opening up the definitions of EQUAL and SY-A, to two new goals: Case 6.2. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X)))) (EQUAL (P (I 2 (S-INC (S-INC (S-INC (P X)))))) (I 2 (S-INC (S-INC (S-INC (P (P X)))))))), which again simplifies, applying A2-EMPTY-S-INC, A2-PC-S-INC, and STR-P-I, to: T. Case 6.1. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (P (I 2 (S-INC (S-INC (S-INC (P X)))))) (E))). But this again simplifies, rewriting with A2-EMPTY-S-INC and STR-P-I-E, and unfolding the definition of EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, applying STR-EMPTY-P and A2-E-SY-A, and expanding EQUAL, SY-A, and P, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (EQUAL LN 'YC1) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YC2 (P X))) (SY-A 'YC2 (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, unfolding the functions EQUAL and SY-A, to the conjecture: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YC2 (P X))) (SY-A 'YC2 (P (P X))))) (EQUAL (P (I 1 (SY-A 'YC2 (P X)))) (SY-A 'YC1 (P X)))). This further simplifies, applying STR-NOT-EMPTY-I and STR-P-I, and expanding the functions EQUAL, SY-A, I, and P, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (EMPTY X)) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, applying STR-EMPTY-P, and unfolding EQUAL, SY-A, and P, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (EQUAL LN 'YOUT) (NOT (EMPTY X)) (EQUAL (P (SY-A 'YC1 (P X))) (SY-A 'YC1 (P (P X))))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))), which simplifies, unfolding the definitions of EQUAL and SY-A, to two new goals: Case 2.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-A 'YC1 (P X))) (SY-A 'YC1 (P (P X)))) (NOT (EMPTY (P X)))) (EQUAL (P (I 0 (SY-A 'YC1 (P X)))) (I 0 (P (SY-A 'YC1 (P X)))))), which 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 'YC1 (P X))) (SY-A 'YC1 (P (P X)))) (EMPTY (P X))) (EQUAL (P (I 0 (SY-A 'YC1 (P X)))) (E))). But this again simplifies, rewriting with STR-EMPTY-P, A2-EMPTY-SY-A, and STR-P-I-E, and opening up EQUAL and SY-A, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Y1)) (NOT (EQUAL LN 'Y2)) (NOT (EQUAL LN 'Y3)) (NOT (EQUAL LN 'YC2)) (NOT (EQUAL LN 'YC1)) (NOT (EQUAL LN 'YOUT))) (EQUAL (P (SY-A LN X)) (SY-A LN (P X)))). This simplifies, rewriting with A2-PC-SFIX, and opening up SY-A, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] A2-PC-SY-A (DEFN TOPOR-SY-B (LN) (IF (EQUAL LN 'Z1) 1 (IF (EQUAL LN 'Z2) 0 (IF (EQUAL LN 'Z3) 1 (IF (EQUAL LN 'Z4) 0 (IF (EQUAL LN 'Z5) 1 (IF (EQUAL LN 'ZOUT) 0 0))))))) From the definition we can conclude that (NUMBERP (TOPOR-SY-B LN)) is a theorem. [ 0.0 0.0 0.2 ] TOPOR-SY-B (DEFN SY-B (LN X) (IF (EQUAL LN 'Z1) (S-INC X) (IF (EQUAL LN 'Z2) (IF (EMPTY X) (E) (I 0 (SY-B 'Z1 (P X)))) (IF (EQUAL LN 'Z3) (S-INC (SY-B 'Z2 X)) (IF (EQUAL LN 'Z4) (IF (EMPTY X) (E) (I 0 (SY-B 'Z3 (P X)))) (IF (EQUAL LN 'Z5) (S-INC (SY-B 'Z4 X)) (IF (EQUAL LN 'ZOUT) (IF (EMPTY X) (E) (I 0 (SY-B 'Z5 (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, EQUAL, CAR, and LESSP 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 recursive call. Hence, SY-B is accepted under the definitional principle. From the definition we can conclude 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))) 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 (EQUAL LN 'Z1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (p 'Z1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (p 'Z2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (p 'Z3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (p 'Z4 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (p 'Z5 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (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, EQUAL, CAR, and LESSP 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Z1) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, applying A2-EMPTY-S-INC, and expanding the functions EQUAL and SY-B, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, opening up the function EQUAL, to: (IMPLIES (EMPTY X) (EMPTY (SY-B 'Z2 X))). This further simplifies, unfolding the definitions of EQUAL, SY-B, and EMPTY, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'Z1 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, expanding the definition of EQUAL, to the goal: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'Z1 (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-B 'Z2 X)))). But this further simplifies, applying the lemmas A2-EMPTY-S-INC and STR-NOT-EMPTY-I, and expanding the definitions of EQUAL and SY-B, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (EQUAL (EMPTY (SY-B 'Z2 X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, applying A2-EMPTY-S-INC, and opening up EQUAL and SY-B, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, opening up the function EQUAL, to: (IMPLIES (EMPTY X) (EMPTY (SY-B 'Z4 X))), which further simplifies, unfolding the functions EQUAL, SY-B, and EMPTY, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'Z3 (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 'Z3 (P X))) (EMPTY (P X)))) (NOT (EMPTY (SY-B 'Z4 X)))). This further simplifies, applying A2-EMPTY-S-INC and STR-NOT-EMPTY-I, and expanding the definitions of EQUAL and SY-B, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (EQUAL (EMPTY (SY-B 'Z4 X)) (EMPTY X))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, rewriting with A2-EMPTY-S-INC, and expanding the functions EQUAL and SY-B, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, opening up the definitions of EQUAL, SY-B, and EMPTY, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (EQUAL (EMPTY (SY-B 'Z5 (P X))) (EMPTY (P X)))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))), which simplifies, applying STR-NOT-EMPTY-I, and expanding the functions EQUAL and SY-B, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (EQUAL (EMPTY (SY-B LN X)) (EMPTY X))). This simplifies, appealing to the lemma A2-EMPTY-SFIX, and opening up the definition of 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) (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 (EQUAL LN 'Z1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (p 'Z1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (p 'Z2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (p 'Z3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (p 'Z4 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (p 'Z5 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (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, EQUAL, CAR, and LESSP 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Z1) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, applying A2-LP-S-INC, and expanding the functions EQUAL and SY-B, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, opening up the function EQUAL, to: (IMPLIES (EMPTY X) (EQUAL (LEN (SY-B 'Z2 X)) (LEN X))). This further simplifies, rewriting with STR-LEN0-EMPTY, and expanding the definitions of EQUAL, SY-B, and LEN, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'Z1 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, expanding the function EQUAL, to the new conjecture: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'Z1 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B 'Z2 X)) (LEN X))), which further simplifies, applying the lemmas A2-LP-S-INC, 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 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (EQUAL (LEN (SY-B 'Z2 X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying A2-LP-S-INC, and opening up EQUAL and SY-B, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (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 'Z4 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 5. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'Z3 (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 'Z3 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B 'Z4 X)) (LEN X))), which further simplifies, applying A2-LP-S-INC, STR-ADD1-LEN-P, and STR-LEN-I, and expanding the definitions of EQUAL and SY-B, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (EQUAL (LEN (SY-B 'Z4 X)) (LEN X))) (EQUAL (LEN (SY-B LN X)) (LEN X))). This simplifies, rewriting with A2-LP-S-INC, and expanding the functions EQUAL and SY-B, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying the lemma STR-LEN0-EMPTY, and opening up the definitions of EQUAL, SY-B, and LEN, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (EQUAL (LEN (SY-B 'Z5 (P X))) (LEN (P X)))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, appealing to the lemmas STR-ADD1-LEN-P and STR-LEN-I, and unfolding the functions EQUAL and SY-B, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (EQUAL (LEN (SY-B LN X)) (LEN X))), which simplifies, applying A2-LP-SFIX, and expanding 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 A2-IC-S-INC))) . 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, SY-B, EMPTY, S-INC, 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, SY-B, EMPTY, and S-INC, 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 (EQUAL LN 'Z1) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (p 'Z1 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (p 'Z2 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (p 'Z3 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (p 'Z4 X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (p 'Z5 (P X))) (p LN X)) (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (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, EQUAL, CAR, and LESSP 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 ten new formulas: Case 10.(IMPLIES (EQUAL LN 'Z1) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, applying the lemma A2-PC-S-INC, and unfolding the definitions of EQUAL and SY-B, to the new goal: (EQUAL (S-INC (P X)) (SY-B 'Z1 (P X))), which further simplifies, expanding EQUAL and SY-B, to: T. Case 9. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying STR-EMPTY-P, and opening up EQUAL and SY-B, to the new goal: (IMPLIES (EMPTY X) (EQUAL (P (SY-B 'Z2 X)) (E))), which further simplifies, opening up the functions EQUAL, SY-B, and P, to: T. Case 8. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (EQUAL LN 'Z2) (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z1 (P X))) (SY-B 'Z1 (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 'Z1 (P X))) (S-INC (P (P X)))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-B 'Z2 X)) (I 0 (S-INC (P (P X)))))), which further simplifies, rewriting with the lemmas A2-PC-S-INC, A2-EMPTY-S-INC, and STR-P-I, and opening up the definitions of EQUAL and SY-B, to: T. Case 8.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z1 (P X))) (S-INC (P (P X)))) (EMPTY (P X))) (EQUAL (P (SY-B 'Z2 X)) (E))), which further simplifies, applying the lemmas A2-PC-S-INC, A2-EMPTY-S-INC, and STR-P-I-E, and expanding the functions EQUAL and SY-B, to: T. Case 7. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (EQUAL LN 'Z3) (EQUAL (P (SY-B 'Z2 X)) (SY-B 'Z2 (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, rewriting with A2-PC-S-INC, and unfolding the definitions of EQUAL and SY-B, to: (IMPLIES (EQUAL (P (SY-B 'Z2 X)) (SY-B 'Z2 (P X))) (EQUAL (S-INC (P (SY-B 'Z2 X))) (SY-B 'Z3 (P X)))), which further simplifies, applying the lemmas STR-EMPTY-P and A2-E-S-INC, and opening up the definitions of EQUAL, SY-B, P, S-INC, and EMPTY, to: T. Case 6. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying the lemma STR-EMPTY-P, and expanding the functions EQUAL and SY-B, to the formula: (IMPLIES (EMPTY X) (EQUAL (P (SY-B 'Z4 X)) (E))). This further simplifies, expanding the definitions of EQUAL, SY-B, and P, to: T. Case 5. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (EQUAL LN 'Z4) (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z3 (P X))) (SY-B 'Z3 (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, unfolding EQUAL and SY-B, to two new goals: Case 5.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z3 (P X))) (S-INC (SY-B 'Z2 (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (SY-B 'Z4 X)) (I 0 (P (SY-B 'Z3 (P X)))))), which further simplifies, applying A2-PC-S-INC, A2-EMPTY-S-INC, STR-NOT-EMPTY-I, and STR-P-I, and opening up the definitions of EQUAL and SY-B, to: T. Case 5.1. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z3 (P X))) (S-INC (SY-B 'Z2 (P (P X))))) (EMPTY (P X))) (EQUAL (P (SY-B 'Z4 X)) (E))). This again simplifies, applying the lemma STR-EMPTY-P, and unfolding the definitions of EQUAL, SY-B, and S-INC, to: (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z3 (P X))) (E)) (EMPTY (P X))) (EQUAL (P (SY-B 'Z4 X)) (E))). But this further simplifies, unfolding the definitions of EQUAL, SY-B, S-INC, P, and I, to: T. Case 4. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (EQUAL LN 'Z5) (EQUAL (P (SY-B 'Z4 X)) (SY-B 'Z4 (P X)))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, applying A2-PC-S-INC, and unfolding EQUAL and SY-B, to: (IMPLIES (EQUAL (P (SY-B 'Z4 X)) (SY-B 'Z4 (P X))) (EQUAL (S-INC (P (SY-B 'Z4 X))) (SY-B 'Z5 (P X)))), which further simplifies, rewriting with STR-EMPTY-P and A2-E-S-INC, and opening up EQUAL, SY-B, P, S-INC, and EMPTY, to: T. Case 3. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (EMPTY X)) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))). This simplifies, rewriting with STR-EMPTY-P, and opening up EQUAL, SY-B, and P, to: T. Case 2. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (EQUAL LN 'ZOUT) (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z5 (P X))) (SY-B 'Z5 (P (P X))))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, expanding EQUAL and SY-B, to two new formulas: Case 2.2. (IMPLIES (AND (NOT (EMPTY X)) (EQUAL (P (SY-B 'Z5 (P X))) (S-INC (SY-B 'Z4 (P (P X))))) (NOT (EMPTY (P X)))) (EQUAL (P (I 0 (SY-B 'Z5 (P X)))) (I 0 (P (SY-B 'Z5 (P X)))))), which 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 'Z5 (P X))) (S-INC (SY-B 'Z4 (P (P X))))) (EMPTY (P X))) (EQUAL (P (I 0 (SY-B 'Z5 (P X)))) (E))). However this again simplifies, appealing to the lemmas STR-EMPTY-P, A2-EMPTY-SY-B, and STR-P-I-E, and expanding the functions EQUAL, SY-B, and S-INC, to: T. Case 1. (IMPLIES (AND (NOT (EQUAL LN 'Z1)) (NOT (EQUAL LN 'Z2)) (NOT (EQUAL LN 'Z3)) (NOT (EQUAL LN 'Z4)) (NOT (EQUAL LN 'Z5)) (NOT (EQUAL LN 'ZOUT))) (EQUAL (P (SY-B LN X)) (SY-B LN (P X)))), which simplifies, rewriting with A2-PC-SFIX, and opening up the function 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-A-B NIL (EQUAL (SY-B 'ZOUT X) (SY-A 'YOUT X)) ((DISABLE LEN) (ENABLE STR-ADD1-LEN-P2) (EXPAND (SY-B 'ZOUT X) (SY-B 'Z5 (P X)) (SY-B 'Z4 (P X)) (SY-B 'Z3 (P (P X))) (SY-B 'Z2 (P (P X))) (SY-A 'YOUT X) (SY-A 'YC1 (P X)) (SY-A 'YC2 (P (P X))) (SY-A 'Y3 (P (P (P X)))) (SY-A 'Y2 (P (P (P X))))))) This conjecture simplifies, expanding SY-B, EQUAL, and SY-A, to the following three new goals: Case 3. (IMPLIES (AND (NOT (EMPTY X)) (EMPTY (P X))) (EQUAL (I 0 (S-INC (E))) (I 0 (E)))). However this again simplifies, expanding the definitions of S-INC, I, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (NOT (EMPTY (P (P X))))) (EQUAL (I 0 (S-INC (I 0 (S-INC (I 0 (S-INC (P (P (P X))))))))) (I 0 (I 1 (I 2 (S-INC (S-INC (S-INC (P (P (P X))))))))))), which again simplifies, applying A2-IC-S-INC, and expanding the definition of INC, to: T. Case 1. (IMPLIES (AND (NOT (EMPTY X)) (NOT (EMPTY (P X))) (EMPTY (P (P X)))) (EQUAL (I 0 (S-INC (I 0 (S-INC (E))))) (I 0 (I 1 (E))))). But this again simplifies, opening up S-INC, I, and EQUAL, to: T. Q.E.D. [ 0.0 0.0 0.0 ] EQ-A-B