(BOOT-STRAP NQTHM) [ 0.1 0.1 0.0 ] GROUND-ZERO (DEFN BOARDP (X) (IF (NLISTP X) (EQUAL X NIL) (AND (OR (EQUAL (CAR X) 'X) (EQUAL (CAR X) 'O) (EQUAL (CAR X) F)) (BOARDP (CDR X))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, BOARDP is accepted under the principle of definition. From the definition we can conclude that (OR (FALSEP (BOARDP X)) (TRUEP (BOARDP X))) is a theorem. [ 0.0 0.0 0.0 ] BOARDP (DEFN ENDP (BOARD) (IF (NLISTP BOARD) T (IF (CAR BOARD) (ENDP (CDR BOARD)) F))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each recursive call. Hence, ENDP is accepted under the definitional principle. From the definition we can conclude that (OR (FALSEP (ENDP BOARD)) (TRUEP (ENDP BOARD))) is a theorem. [ 0.0 0.0 0.0 ] ENDP (DEFN LEGAL-MOVEP (BOARD1 PLAYER BOARD2) (COND ((NLISTP BOARD1) F) ((EQUAL (CAR BOARD1) (CAR BOARD2)) (LEGAL-MOVEP (CDR BOARD1) PLAYER (CDR BOARD2))) ((AND (EQUAL (CAR BOARD1) F) (EQUAL (CAR BOARD2) PLAYER)) (EQUAL (CDR BOARD1) (CDR BOARD2))) (T F))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT BOARD1) decreases according to the well-founded relation LESSP in each recursive call. Hence, LEGAL-MOVEP is accepted under the principle of definition. Observe that: (OR (FALSEP (LEGAL-MOVEP BOARD1 PLAYER BOARD2)) (TRUEP (LEGAL-MOVEP BOARD1 PLAYER BOARD2))) is a theorem. [ 0.0 0.0 0.0 ] LEGAL-MOVEP (DEFN NTH (I BOARD) (IF (ZEROP I) (CAR BOARD) (NTH (SUB1 I) (CDR BOARD)))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the measure (COUNT I) decreases according to the well-founded relation LESSP in each recursive call. Hence, NTH is accepted under the principle of definition. [ 0.0 0.0 0.0 ] NTH (DEFN WINP1 (X LINE BOARD) (IF (NLISTP LINE) T (IF (EQUAL X (NTH (CAR LINE) BOARD)) (WINP1 X (CDR LINE) BOARD) F))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT LINE) decreases according to the well-founded relation LESSP in each recursive call. Hence, WINP1 is accepted under the principle of definition. From the definition we can conclude that: (OR (FALSEP (WINP1 X LINE BOARD)) (TRUEP (WINP1 X LINE BOARD))) is a theorem. [ 0.0 0.0 0.0 ] WINP1 (DEFN WINP (X BOARD) (OR (WINP1 X '(0 1 2) BOARD) (WINP1 X '(3 4 5) BOARD) (WINP1 X '(6 7 8) BOARD) (WINP1 X '(0 3 6) BOARD) (WINP1 X '(1 4 7) BOARD) (WINP1 X '(2 5 8) BOARD) (WINP1 X '(0 4 8) BOARD) (WINP1 X '(2 4 6) BOARD))) Observe that (OR (FALSEP (WINP X BOARD)) (TRUEP (WINP X BOARD))) is a theorem. [ 0.1 0.0 0.0 ] WINP (DISABLE WINP) [ 0.0 0.0 0.0 ] WINP-OFF (DEFN OTHER-PLAYER (PLAYER) (IF (EQUAL PLAYER 'X) 'O 'X)) Observe that (LITATOM (OTHER-PLAYER PLAYER)) is a theorem. [ 0.0 0.0 0.0 ] OTHER-PLAYER (DEFN END (OUTCOME PLAYER LST) (LET ((OUTCOME (IF (EQUAL OUTCOME 'WIN) (IF (EQUAL PLAYER 'O) 'O-WIN 'X-WIN) 'DRAW))) (IF (EQUAL LST (LIST OUTCOME)) OUTCOME F))) Note that: (OR (FALSEP (END OUTCOME PLAYER LST)) (LITATOM (END OUTCOME PLAYER LST))) is a theorem. [ 0.0 0.0 0.0 ] END (DEFN TIC-TAC-TOEP1 (BOARD PLAYER LST) (COND ((NLISTP LST) (END 'WIN (OTHER-PLAYER PLAYER) LST)) ((NOT (BOARDP (CAR LST))) F) ((NOT (LEGAL-MOVEP BOARD PLAYER (CAR LST))) (END 'WIN (OTHER-PLAYER PLAYER) (CDR LST))) ((WINP PLAYER (CAR LST)) (END 'WIN PLAYER (CDR LST))) ((ENDP (CAR LST)) (END 'DRAW PLAYER (CDR LST))) (T (TIC-TAC-TOEP1 (CAR LST) (OTHER-PLAYER PLAYER) (CDR LST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to establish that the measure (COUNT LST) decreases according to the well-founded relation LESSP in each recursive call. Hence, TIC-TAC-TOEP1 is accepted under the principle of definition. Observe that: (OR (FALSEP (TIC-TAC-TOEP1 BOARD PLAYER LST)) (LITATOM (TIC-TAC-TOEP1 BOARD PLAYER LST))) is a theorem. [ 0.0 0.0 0.0 ] TIC-TAC-TOEP1 (DEFN TIC-TAC-TOEP (LST) (IF (AND (LISTP LST) (EQUAL (CAR LST) (LIST F F F F F F F F F))) (TIC-TAC-TOEP1 (CAR LST) 'X (CDR LST)) F)) From the definition we can conclude that: (OR (FALSEP (TIC-TAC-TOEP LST)) (LITATOM (TIC-TAC-TOEP LST))) is a theorem. [ 0.0 0.0 0.0 ] TIC-TAC-TOEP (DEFN MOVE (X I BOARD) (IF (NLISTP BOARD) BOARD (IF (ZEROP I) (CONS X (CDR BOARD)) (CONS (CAR BOARD) (MOVE X (SUB1 I) (CDR BOARD)))))) Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of ZEROP and NLISTP establish that the measure (COUNT I) decreases according to the well-founded relation LESSP in each recursive call. Hence, MOVE is accepted under the principle of definition. The definition of MOVE can be justified in another way. Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definitions of ZEROP and NLISTP inform us that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each recursive call. Observe that (OR (LISTP (MOVE X I BOARD)) (EQUAL (MOVE X I BOARD) BOARD)) is a theorem. [ 0.0 0.0 0.0 ] MOVE (DEFN LEGALP (I BOARD) (AND (LESSP I '9) (EQUAL (NTH I BOARD) F))) Note that (OR (FALSEP (LEGALP I BOARD)) (TRUEP (LEGALP I BOARD))) is a theorem. [ 0.0 0.0 0.0 ] LEGALP (DEFN OPEN-SQUARES (BOARD) (IF (NLISTP BOARD) 0 (IF (CAR BOARD) (OPEN-SQUARES (CDR BOARD)) (ADD1 (OPEN-SQUARES (CDR BOARD)))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each recursive call. Hence, OPEN-SQUARES is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (OPEN-SQUARES BOARD)) is a theorem. [ 0.0 0.0 0.0 ] OPEN-SQUARES (PROVE-LEMMA LEGAL-MOVES-REDUCE-OPEN-SQUARES (REWRITE) (IMPLIES (AND X (LEGALP I BOARD)) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD)))) WARNING: Note that the proposed lemma LEGAL-MOVES-REDUCE-OPEN-SQUARES is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. This conjecture can be simplified, using the abbreviations LEGALP, AND, and IMPLIES, to: (IMPLIES (AND X (LESSP I 9) (EQUAL (NTH I BOARD) F)) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))). This simplifies, clearly, to: (IMPLIES (AND X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))), which we will name *1. We will appeal to induction. There are five plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (OR (EQUAL 9 0) (NOT (NUMBERP 9))) (p X I BOARD)) (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (OR (EQUAL I 0) (NOT (NUMBERP I)))) (p X I BOARD)) (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (p X (SUB1 I) (CDR BOARD))) (p X I BOARD))). Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions of OR and NOT inform us that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for BOARD. The above induction scheme produces the following five new goals: Case 5. (IMPLIES (AND (OR (EQUAL 9 0) (NOT (NUMBERP 9))) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))). This simplifies, expanding the definitions of EQUAL, NUMBERP, NOT, and OR, to: T. Case 4. (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (OR (EQUAL I 0) (NOT (NUMBERP I))) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))). This simplifies, opening up the definitions of EQUAL, NUMBERP, NOT, OR, LESSP, NTH, MOVE, and OPEN-SQUARES, to the following four new formulas: Case 4.4. (IMPLIES (AND (EQUAL I 0) X (NOT (CAR BOARD)) (NOT (LISTP BOARD))) (LESSP (OPEN-SQUARES BOARD) 0)). But this again simplifies, rewriting with the lemma CAR-NLISTP, to: T. Case 4.3. (IMPLIES (AND (EQUAL I 0) X (NOT (CAR BOARD)) (LISTP BOARD)) (LESSP (OPEN-SQUARES (CONS X (CDR BOARD))) (ADD1 (OPEN-SQUARES (CDR BOARD))))), which again simplifies, rewriting with CDR-CONS, CAR-CONS, and SUB1-ADD1, and opening up the definitions of OPEN-SQUARES and LESSP, to the new goal: (IMPLIES (AND X (NOT (CAR BOARD)) (LISTP BOARD) (NOT (EQUAL (OPEN-SQUARES (CDR BOARD)) 0))) (LESSP (SUB1 (OPEN-SQUARES (CDR BOARD))) (OPEN-SQUARES (CDR BOARD)))), which again simplifies, using linear arithmetic, to: T. Case 4.2. (IMPLIES (AND (NOT (NUMBERP I)) X (NOT (CAR BOARD)) (NOT (LISTP BOARD))) (LESSP (OPEN-SQUARES BOARD) 0)), which again simplifies, applying CAR-NLISTP, to: T. Case 4.1. (IMPLIES (AND (NOT (NUMBERP I)) X (NOT (CAR BOARD)) (LISTP BOARD)) (LESSP (OPEN-SQUARES (CONS X (CDR BOARD))) (ADD1 (OPEN-SQUARES (CDR BOARD))))). This again simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and unfolding the definitions of OPEN-SQUARES and LESSP, to the new goal: (IMPLIES (AND (NOT (NUMBERP I)) X (NOT (CAR BOARD)) (LISTP BOARD) (NOT (EQUAL (OPEN-SQUARES (CDR BOARD)) 0))) (LESSP (SUB1 (OPEN-SQUARES (CDR BOARD))) (OPEN-SQUARES (CDR BOARD)))), which again simplifies, using linear arithmetic, to: T. Case 3. (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (NOT (LESSP (SUB1 I) 9)) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))), which simplifies, using linear arithmetic, to: (IMPLIES (AND (LESSP I 1) (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (NOT (LESSP (SUB1 I) 9)) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))). But this again simplifies, unfolding the functions SUB1, NUMBERP, EQUAL, LESSP, NOT, and OR, to: T. Case 2. (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (NTH (SUB1 I) (CDR BOARD)) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))), which simplifies, expanding the definitions of EQUAL, NUMBERP, NOT, OR, LESSP, SUB1, and NTH, to: T. Case 1. (IMPLIES (AND (NOT (OR (EQUAL 9 0) (NOT (NUMBERP 9)))) (NOT (OR (EQUAL I 0) (NOT (NUMBERP I)))) (LESSP (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))) (OPEN-SQUARES (CDR BOARD))) X (LESSP I 9) (NOT (NTH I BOARD))) (LESSP (OPEN-SQUARES (MOVE X I BOARD)) (OPEN-SQUARES BOARD))), which simplifies, unfolding EQUAL, NUMBERP, NOT, OR, LESSP, SUB1, NTH, MOVE, and OPEN-SQUARES, to three new conjectures: Case 1.3. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))) (OPEN-SQUARES (CDR BOARD))) X (LESSP (SUB1 I) 8) (NOT (NTH (SUB1 I) (CDR BOARD))) (NOT (LISTP BOARD))) (LESSP (OPEN-SQUARES BOARD) 0)), which again simplifies, unfolding OPEN-SQUARES and LESSP, to: (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))) (OPEN-SQUARES (CDR BOARD))) X (LESSP (SUB1 I) 8) (NOT (NTH (SUB1 I) (CDR BOARD)))) (LISTP BOARD)). But this further simplifies, rewriting with CDR-NLISTP, and unfolding the definitions of LISTP, MOVE, OPEN-SQUARES, and LESSP, to: T. Case 1.2. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))) (OPEN-SQUARES (CDR BOARD))) X (LESSP (SUB1 I) 8) (NOT (NTH (SUB1 I) (CDR BOARD))) (LISTP BOARD) (CAR BOARD)) (LESSP (OPEN-SQUARES (CONS (CAR BOARD) (MOVE X (SUB1 I) (CDR BOARD)))) (OPEN-SQUARES (CDR BOARD)))). This again simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding the function OPEN-SQUARES, to: T. Case 1.1. (IMPLIES (AND (NOT (EQUAL I 0)) (NUMBERP I) (LESSP (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))) (OPEN-SQUARES (CDR BOARD))) X (LESSP (SUB1 I) 8) (NOT (NTH (SUB1 I) (CDR BOARD))) (LISTP BOARD) (NOT (CAR BOARD))) (LESSP (OPEN-SQUARES (CONS (CAR BOARD) (MOVE X (SUB1 I) (CDR BOARD)))) (ADD1 (OPEN-SQUARES (CDR BOARD))))). However this again simplifies, applying CDR-CONS, CAR-CONS, and SUB1-ADD1, and unfolding the functions OPEN-SQUARES and LESSP, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LEGAL-MOVES-REDUCE-OPEN-SQUARES (PROVE-LEMMA MOVE-NEVER-INCREASES-OPEN-SQUARES (REWRITE) (IMPLIES X (NOT (LESSP (OPEN-SQUARES BOARD) (OPEN-SQUARES (MOVE X I BOARD)))))) WARNING: Note that the proposed lemma MOVE-NEVER-INCREASES-OPEN-SQUARES is to be stored as zero type prescription rules, zero compound recognizer rules, one linear rule, and zero replacement rules. Name the conjecture *1. Let us appeal to the induction principle. The recursive terms in the conjecture suggest three inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP BOARD) (p BOARD X I)) (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (p (CDR BOARD) X (SUB1 I))) (p BOARD X I)) (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (CAR BOARD)) (p (CDR BOARD) X (SUB1 I))) (p BOARD X I))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instances chosen for I. The above induction scheme leads to the following three new goals: Case 3. (IMPLIES (AND (NLISTP BOARD) X) (NOT (LESSP (OPEN-SQUARES BOARD) (OPEN-SQUARES (MOVE X I BOARD))))). This simplifies, expanding the definitions of NLISTP, OPEN-SQUARES, MOVE, and LESSP, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X) (NOT (LESSP (OPEN-SQUARES BOARD) (OPEN-SQUARES (MOVE X I BOARD))))). This simplifies, unfolding NLISTP, OPEN-SQUARES, and MOVE, to the following three new goals: Case 2.3. (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (EQUAL I 0)) (NUMBERP I)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CONS (CAR BOARD) (MOVE X (SUB1 I) (CDR BOARD))))))). This again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and expanding the function OPEN-SQUARES, to: T. Case 2.2. (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (EQUAL I 0)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CONS X (CDR BOARD)))))), which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding the functions SUB1, EQUAL, MOVE, and OPEN-SQUARES, to: (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (LISTP (CDR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CONS X (CDDR BOARD))))) X) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CDR BOARD))))), which again simplifies, using linear arithmetic, to: T. Case 2.1. (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (NUMBERP I))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CONS X (CDR BOARD)))))), which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding OPEN-SQUARES, to: (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (NUMBERP I))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CDR BOARD))))), which again simplifies, using linear arithmetic, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (CAR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X) (NOT (LESSP (OPEN-SQUARES BOARD) (OPEN-SQUARES (MOVE X I BOARD))))), which simplifies, applying SUB1-ADD1, and expanding the functions NLISTP, OPEN-SQUARES, MOVE, and LESSP, to the following three new goals: Case 1.3. (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (NUMBERP I)) (NOT (EQUAL (OPEN-SQUARES (CONS X (CDR BOARD))) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CONS X (CDR BOARD))))))). However this again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up OPEN-SQUARES, to the new conjecture: (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (NUMBERP I)) (NOT (EQUAL (OPEN-SQUARES (CDR BOARD)) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CDR BOARD)))))), which again simplifies, using linear arithmetic, to: T. Case 1.2. (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (EQUAL I 0) (NOT (EQUAL (OPEN-SQUARES (CONS X (CDR BOARD))) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CONS X (CDR BOARD))))))), which again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and unfolding the definitions of SUB1, EQUAL, MOVE, and OPEN-SQUARES, to two new formulas: Case 1.2.2. (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (NOT (LISTP (CDR BOARD))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CDR BOARD)))) X (NOT (EQUAL (OPEN-SQUARES (CDR BOARD)) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CDR BOARD)))))), which again simplifies, using linear arithmetic, to: T. Case 1.2.1. (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (LISTP (CDR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (CONS X (CDDR BOARD))))) X (NOT (EQUAL (OPEN-SQUARES (CDR BOARD)) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CDR BOARD)))))), which again simplifies, using linear arithmetic, to: T. Case 1.1. (IMPLIES (AND (LISTP BOARD) (NOT (CAR BOARD)) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (OPEN-SQUARES (MOVE X (SUB1 I) (CDR BOARD))))) X (NOT (EQUAL I 0)) (NUMBERP I) (NOT (EQUAL (OPEN-SQUARES (CONS F (MOVE X (SUB1 I) (CDR BOARD)))) 0))) (NOT (LESSP (OPEN-SQUARES (CDR BOARD)) (SUB1 (OPEN-SQUARES (CONS F (MOVE X (SUB1 I) (CDR BOARD)))))))), which again simplifies, rewriting with CDR-CONS, CAR-CONS, and SUB1-ADD1, and opening up the definition of OPEN-SQUARES, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.1 0.0 ] MOVE-NEVER-INCREASES-OPEN-SQUARES (DEFN PICK-MOVE1 (BOARD I) (COND ((NLISTP BOARD) 0) ((EQUAL (CAR BOARD) F) I) (T (PICK-MOVE1 (CDR BOARD) (ADD1 I))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each recursive call. Hence, PICK-MOVE1 is accepted under the definitional principle. From the definition we can conclude that: (OR (NUMBERP (PICK-MOVE1 BOARD I)) (EQUAL (PICK-MOVE1 BOARD I) I)) is a theorem. [ 0.0 0.0 0.0 ] PICK-MOVE1 (DEFN PICK-MOVE (BOARD) (LET ((BOOK-MOVE (ASSOC BOARD '(((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE X X *1*FALSE O O O X X) . 3) ((X *1*FALSE X *1*FALSE O O O X X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE O X X) . 5) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X X O X) . 1) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE X O X) . 1) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE X O X) . 1) ((O X X *1*FALSE O *1*FALSE X O X) . 5) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((*1*FALSE *1*FALSE O *1*FALSE O X *1*FALSE X X) . 6) ((*1*FALSE *1*FALSE O X O X X O X) . 1) ((*1*FALSE *1*FALSE O *1*FALSE O X X *1*FALSE X) . 7) ((*1*FALSE *1*FALSE O X O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((X *1*FALSE O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O X O *1*FALSE X) . 2) ((*1*FALSE *1*FALSE X X O *1*FALSE O *1*FALSE X) . 5) ((*1*FALSE X *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((*1*FALSE *1*FALSE X *1*FALSE O O *1*FALSE X X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O O X *1*FALSE X) . 3) ((O *1*FALSE X X O O *1*FALSE X X) . 6) ((O *1*FALSE X X O O X *1*FALSE X) . 7) ((*1*FALSE X X *1*FALSE O O *1*FALSE *1*FALSE X) . 3) ((X *1*FALSE X *1*FALSE O O *1*FALSE *1*FALSE X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((*1*FALSE X O *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((*1*FALSE X O *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O X O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 2) ((X O X *1*FALSE O *1*FALSE O X X) . 5) ((X O *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((X O *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((X O *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE X) . 7) ((X O *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((X O X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE X) . 4) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE X X *1*FALSE O O O X X) . 3) ((X *1*FALSE X *1*FALSE O O O X X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE O X X) . 5) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((X *1*FALSE X O O *1*FALSE X X O) . 5) ((X X *1*FALSE O O *1*FALSE X X O) . 5) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X X O) . 3) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((X O *1*FALSE *1*FALSE O X X X O) . 3) ((X O *1*FALSE X O X *1*FALSE X O) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE X *1*FALSE) . 8) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O X O X *1*FALSE) . 2) ((O *1*FALSE X X O *1*FALSE O X X) . 5) ((O *1*FALSE X X O X O X *1*FALSE) . 8) ((O X X X O *1*FALSE O X *1*FALSE) . 8) ((*1*FALSE X *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X O X X O *1*FALSE *1*FALSE X O) . 6) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((*1*FALSE X O *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((*1*FALSE X O X O *1*FALSE X X O) . 5) ((X X O *1*FALSE O *1*FALSE X X O) . 5) ((*1*FALSE X O *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((*1*FALSE X O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((*1*FALSE X O X O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((X *1*FALSE *1*FALSE *1*FALSE O X O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X O X *1*FALSE O *1*FALSE O X X) . 5) ((X O X *1*FALSE O X O X *1*FALSE) . 8) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE X *1*FALSE) . 4) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X X O X) . 1) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE X O X) . 1) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE X O X) . 1) ((O X X *1*FALSE O *1*FALSE X O X) . 5) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((X *1*FALSE X O O *1*FALSE X X O) . 5) ((X X *1*FALSE O O *1*FALSE X X O) . 5) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X X O) . 3) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((X *1*FALSE *1*FALSE *1*FALSE O X X *1*FALSE O) . 3) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O *1*FALSE X *1*FALSE X) . 7) ((O *1*FALSE *1*FALSE X O *1*FALSE X X *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((*1*FALSE O X *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((*1*FALSE O X *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((*1*FALSE O X *1*FALSE O X X *1*FALSE *1*FALSE) . 7) ((*1*FALSE O X X O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((X O X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 1) ((O X X *1*FALSE O *1*FALSE X O X) . 5) ((O X *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((O X *1*FALSE *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((O X *1*FALSE *1*FALSE O X X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((X *1*FALSE *1*FALSE O O *1*FALSE X *1*FALSE X) . 5) ((X *1*FALSE *1*FALSE O O *1*FALSE X X *1*FALSE) . 5) ((X O *1*FALSE O O X X *1*FALSE X) . 7) ((X O *1*FALSE O O X X X *1*FALSE) . 8) ((X *1*FALSE X O O *1*FALSE X *1*FALSE *1*FALSE) . 5) ((X X *1*FALSE O O *1*FALSE X *1*FALSE *1*FALSE) . 5) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 3) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE X *1*FALSE *1*FALSE) . 4) ((*1*FALSE *1*FALSE O *1*FALSE O X *1*FALSE X X) . 6) ((*1*FALSE *1*FALSE O X O X X O X) . 1) ((*1*FALSE *1*FALSE O *1*FALSE O X X *1*FALSE X) . 7) ((*1*FALSE *1*FALSE O X O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((X *1*FALSE O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE X) . 2) ((X O *1*FALSE *1*FALSE O X X X O) . 3) ((X O *1*FALSE X O X *1*FALSE X O) . 6) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE X *1*FALSE) . 8) ((X *1*FALSE *1*FALSE *1*FALSE O X X *1*FALSE O) . 3) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X *1*FALSE *1*FALSE X) . 2) ((O *1*FALSE *1*FALSE X O X *1*FALSE X *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((X O X *1*FALSE O X X *1*FALSE O) . 7) ((X O X X O X *1*FALSE *1*FALSE O) . 7) ((*1*FALSE *1*FALSE X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((O X O *1*FALSE O X X *1*FALSE X) . 7) ((O X O *1*FALSE O X X X *1*FALSE) . 8) ((O X O X O X X *1*FALSE *1*FALSE) . 8) ((*1*FALSE X O X O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 2) ((X *1*FALSE O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((X *1*FALSE O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((X *1*FALSE O O O X X *1*FALSE X) . 7) ((X *1*FALSE O O O X X X *1*FALSE) . 8) ((X *1*FALSE O *1*FALSE O X X *1*FALSE *1*FALSE) . 3) ((X *1*FALSE O X O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 2) ((*1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE X *1*FALSE *1*FALSE *1*FALSE) . 4) ((O X O *1*FALSE X *1*FALSE *1*FALSE *1*FALSE X) . 7) ((O *1*FALSE *1*FALSE *1*FALSE X *1*FALSE *1*FALSE *1*FALSE X) . 2) ((O O X *1*FALSE X *1*FALSE *1*FALSE X *1*FALSE) . 6) ((O X O *1*FALSE X *1*FALSE X *1*FALSE *1*FALSE) . 7) ((O *1*FALSE *1*FALSE *1*FALSE X *1*FALSE X *1*FALSE *1*FALSE) . 2) ((O *1*FALSE *1*FALSE O X X *1*FALSE *1*FALSE X) . 6) ((O *1*FALSE *1*FALSE O X X *1*FALSE X *1*FALSE) . 6) ((O *1*FALSE *1*FALSE O X X X *1*FALSE *1*FALSE) . 2) ((O *1*FALSE X O X X *1*FALSE *1*FALSE *1*FALSE) . 6) ((O X *1*FALSE O X X *1*FALSE *1*FALSE *1*FALSE) . 6) ((O *1*FALSE *1*FALSE *1*FALSE X X *1*FALSE *1*FALSE *1*FALSE) . 3) ((O X O X X O X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X X O X *1*FALSE *1*FALSE) . 2) ((O *1*FALSE X X X O *1*FALSE *1*FALSE *1*FALSE) . 6) ((O X *1*FALSE X X O *1*FALSE *1*FALSE *1*FALSE) . 7) ((O *1*FALSE *1*FALSE X X *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 5) ((O *1*FALSE X *1*FALSE X *1*FALSE O *1*FALSE X) . 3) ((O *1*FALSE X *1*FALSE X *1*FALSE O X *1*FALSE) . 3) ((O *1*FALSE X *1*FALSE X X O *1*FALSE *1*FALSE) . 3) ((O *1*FALSE X X X *1*FALSE O *1*FALSE *1*FALSE) . 5) ((O *1*FALSE X *1*FALSE X *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 6) ((O X *1*FALSE O X X *1*FALSE O X) . 6) ((O X *1*FALSE *1*FALSE X X *1*FALSE O *1*FALSE) . 3) ((O X *1*FALSE X X *1*FALSE *1*FALSE O *1*FALSE) . 5) ((O X X *1*FALSE X X O O *1*FALSE) . 8) ((O X X X X *1*FALSE O O *1*FALSE) . 8) ((O X X *1*FALSE X *1*FALSE *1*FALSE O *1*FALSE) . 6) ((O X *1*FALSE *1*FALSE X *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 7) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O X O *1*FALSE X) . 2) ((*1*FALSE *1*FALSE X X O *1*FALSE O *1*FALSE X) . 5) ((*1*FALSE X *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE O X X) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O X O X *1*FALSE) . 2) ((O *1*FALSE X X O *1*FALSE O X X) . 5) ((O *1*FALSE X X O X O X *1*FALSE) . 8) ((O X X X O *1*FALSE O X *1*FALSE) . 8) ((*1*FALSE X *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((*1*FALSE *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((O *1*FALSE *1*FALSE X O *1*FALSE X *1*FALSE X) . 7) ((O *1*FALSE *1*FALSE X O *1*FALSE X X *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X *1*FALSE *1*FALSE X) . 2) ((O *1*FALSE *1*FALSE X O X *1*FALSE X *1*FALSE) . 8) ((O *1*FALSE *1*FALSE X O X X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O O *1*FALSE X X) . 6) ((O *1*FALSE X X O O X *1*FALSE X) . 7) ((O *1*FALSE X X O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((O *1*FALSE X X O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O *1*FALSE X X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X O X O *1*FALSE *1*FALSE X X) . 6) ((O X O X O *1*FALSE X *1*FALSE X) . 7) ((O X *1*FALSE X O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((X *1*FALSE *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O X O *1*FALSE *1*FALSE) . 2) ((X O X X O *1*FALSE O *1*FALSE X) . 7) ((X *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 6) ((*1*FALSE *1*FALSE *1*FALSE X *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 4) ((*1*FALSE *1*FALSE X *1*FALSE O O *1*FALSE X X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O O X *1*FALSE X) . 3) ((O *1*FALSE X X O O *1*FALSE X X) . 6) ((O *1*FALSE X X O O X *1*FALSE X) . 7) ((*1*FALSE X X *1*FALSE O O *1*FALSE *1*FALSE X) . 3) ((X *1*FALSE X *1*FALSE O O *1*FALSE *1*FALSE X) . 3) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((X O X X O *1*FALSE *1*FALSE X O) . 6) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((*1*FALSE O X *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((*1*FALSE O X *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((*1*FALSE O X *1*FALSE O X X *1*FALSE *1*FALSE) . 7) ((*1*FALSE O X X O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((X O X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((*1*FALSE *1*FALSE X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 1) ((X O X *1*FALSE O X X *1*FALSE O) . 7) ((X O X X O X *1*FALSE *1*FALSE O) . 7) ((*1*FALSE *1*FALSE X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O O *1*FALSE X X) . 6) ((O *1*FALSE X X O O X *1*FALSE X) . 7) ((O *1*FALSE X X O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((O *1*FALSE X X O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O *1*FALSE X X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O *1*FALSE X X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((O X X *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((X O X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((X O X O O X *1*FALSE X *1*FALSE) . 8) ((X O X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((X O X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 7) ((X O X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 7) ((*1*FALSE *1*FALSE X *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 4) ((*1*FALSE X O *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((*1*FALSE X O *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O X O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 2) ((*1*FALSE X O *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((*1*FALSE X O X O *1*FALSE X X O) . 5) ((X X O *1*FALSE O *1*FALSE X X O) . 5) ((*1*FALSE X O *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((*1*FALSE X O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((*1*FALSE X O X O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 2) ((O X X *1*FALSE O *1*FALSE X O X) . 5) ((O X *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((O X *1*FALSE *1*FALSE O *1*FALSE X X *1*FALSE) . 8) ((O X *1*FALSE *1*FALSE O X X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((*1*FALSE X O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((*1*FALSE X O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((O X O *1*FALSE O X X *1*FALSE X) . 7) ((O X O *1*FALSE O X X X *1*FALSE) . 8) ((O X O X O X X *1*FALSE *1*FALSE) . 8) ((*1*FALSE X O X O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((*1*FALSE X *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 2) ((O X O X O *1*FALSE *1*FALSE X X) . 6) ((O X O X O *1*FALSE X *1*FALSE X) . 7) ((O X *1*FALSE X O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O X *1*FALSE X O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X *1*FALSE X O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 5) ((O X X *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 8) ((O X X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 8) ((O X X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 8) ((O X X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 8) ((X X O *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 6) ((*1*FALSE X *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 4) ((X O X *1*FALSE O *1*FALSE O X X) . 5) ((X O *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X X) . 6) ((X O *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE X) . 7) ((X O *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE X) . 7) ((X O *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((X O X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE O X X) . 2) ((X *1*FALSE *1*FALSE *1*FALSE O X O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X O X *1*FALSE O *1*FALSE O X X) . 5) ((X O X *1*FALSE O X O X *1*FALSE) . 8) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X *1*FALSE *1*FALSE O O *1*FALSE X *1*FALSE X) . 5) ((X *1*FALSE *1*FALSE O O *1*FALSE X X *1*FALSE) . 5) ((X O *1*FALSE O O X X *1*FALSE X) . 7) ((X O *1*FALSE O O X X X *1*FALSE) . 8) ((X *1*FALSE X O O *1*FALSE X *1*FALSE *1*FALSE) . 5) ((X X *1*FALSE O O *1*FALSE X *1*FALSE *1*FALSE) . 5) ((X *1*FALSE *1*FALSE *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 3) ((X *1*FALSE O *1*FALSE O X *1*FALSE *1*FALSE X) . 6) ((X *1*FALSE O *1*FALSE O X *1*FALSE X *1*FALSE) . 6) ((X *1*FALSE O O O X X *1*FALSE X) . 7) ((X *1*FALSE O O O X X X *1*FALSE) . 8) ((X *1*FALSE O *1*FALSE O X X *1*FALSE *1*FALSE) . 3) ((X *1*FALSE O X O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X *1*FALSE *1*FALSE *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O *1*FALSE X) . 2) ((X *1*FALSE *1*FALSE X O *1*FALSE O X *1*FALSE) . 2) ((X *1*FALSE *1*FALSE X O X O *1*FALSE *1*FALSE) . 2) ((X O X X O *1*FALSE O *1*FALSE X) . 7) ((X *1*FALSE *1*FALSE X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 6) ((X O X *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 7) ((X O X O O X *1*FALSE X *1*FALSE) . 8) ((X O X *1*FALSE O *1*FALSE X *1*FALSE *1*FALSE) . 7) ((X O X *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 7) ((X O X X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 7) ((X X O *1*FALSE O *1*FALSE *1*FALSE *1*FALSE X) . 6) ((X X O *1*FALSE O *1*FALSE *1*FALSE X *1*FALSE) . 6) ((X X O *1*FALSE O X *1*FALSE *1*FALSE *1*FALSE) . 6) ((X X O X O *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 6) ((X *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE *1*FALSE) . 4))))) (IF BOOK-MOVE (CDR BOOK-MOVE) (PICK-MOVE1 BOARD 0)))) [ 0.1 0.0 0.0 ] PICK-MOVE (DISABLE PICK-MOVE) [ 0.0 0.0 0.0 ] PICK-MOVE-OFF (DEFN TIC-TAC-TOE1 (XMOVES BOARD) (LET ((BOARD1 (MOVE 'X (CAR XMOVES) BOARD))) (IF (LEGALP (CAR XMOVES) BOARD) (IF (ENDP BOARD1) (LIST BOARD1 'DRAW) (LET ((BOARD2 (MOVE 'O (PICK-MOVE BOARD1) BOARD1))) (IF (WINP 'O BOARD2) (LIST BOARD1 BOARD2 'O-WIN) (CONS BOARD1 (CONS BOARD2 (TIC-TAC-TOE1 (CDR XMOVES) BOARD2)))))) (LIST BOARD1 'O-WIN))) ((LESSP (OPEN-SQUARES BOARD)))) Linear arithmetic and the lemmas MOVE-NEVER-INCREASES-OPEN-SQUARES and LEGAL-MOVES-REDUCE-OPEN-SQUARES inform us that the measure (OPEN-SQUARES BOARD) decreases according to the well-founded relation LESSP in each recursive call. Hence, TIC-TAC-TOE1 is accepted under the principle of definition. From the definition we can conclude that: (LISTP (TIC-TAC-TOE1 XMOVES BOARD)) is a theorem. [ 0.1 0.0 0.0 ] TIC-TAC-TOE1 (DEFN TIC-TAC-TOE (XMOVES) (LET ((BOARD0 (LIST F F F F F F F F F))) (CONS BOARD0 (TIC-TAC-TOE1 XMOVES BOARD0)))) Note that (LISTP (TIC-TAC-TOE XMOVES)) is a theorem. [ 0.0 0.0 0.0 ] TIC-TAC-TOE (DEFN LENGTH (X) (IF (NLISTP X) 0 (ADD1 (LENGTH (CDR X))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT X) decreases according to the well-founded relation LESSP in each recursive call. Hence, LENGTH is accepted under the principle of definition. From the definition we can conclude that (NUMBERP (LENGTH X)) is a theorem. [ 0.0 0.0 0.0 ] LENGTH (PROVE-LEMMA LENGTH-MOVE (REWRITE) (EQUAL (LENGTH (MOVE X I BOARD)) (LENGTH BOARD))) Name the conjecture *1. Perhaps we can prove it by induction. There are three plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP BOARD) (p X I BOARD)) (IMPLIES (AND (NOT (NLISTP BOARD)) (ZEROP I)) (p X I BOARD)) (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (ZEROP I)) (p X (SUB1 I) (CDR BOARD))) (p X I BOARD))). Linear arithmetic, the lemma COUNT-NUMBERP, and the definitions of ZEROP and NLISTP establish that the measure (COUNT I) decreases according to the well-founded relation LESSP in each induction step of the scheme. Note, however, the inductive instance chosen for BOARD. The above induction scheme produces the following three new goals: Case 3. (IMPLIES (NLISTP BOARD) (EQUAL (LENGTH (MOVE X I BOARD)) (LENGTH BOARD))). This simplifies, expanding NLISTP, MOVE, LENGTH, and EQUAL, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP BOARD)) (ZEROP I)) (EQUAL (LENGTH (MOVE X I BOARD)) (LENGTH BOARD))). This simplifies, rewriting with CDR-CONS, and unfolding the definitions of NLISTP, ZEROP, EQUAL, MOVE, and LENGTH, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (ZEROP I)) (EQUAL (LENGTH (MOVE X (SUB1 I) (CDR BOARD))) (LENGTH (CDR BOARD)))) (EQUAL (LENGTH (MOVE X I BOARD)) (LENGTH BOARD))), which simplifies, rewriting with CDR-CONS, and expanding the definitions of NLISTP, ZEROP, MOVE, and LENGTH, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LENGTH-MOVE (DEFN LEGAL-BOOKP (ALIST) (IF (NLISTP ALIST) T (AND (LEGALP (CDAR ALIST) (CAAR ALIST)) (LEGAL-BOOKP (CDR ALIST))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT ALIST) decreases according to the well-founded relation LESSP in each recursive call. Hence, LEGAL-BOOKP is accepted under the definitional principle. Observe that: (OR (FALSEP (LEGAL-BOOKP ALIST)) (TRUEP (LEGAL-BOOKP ALIST))) is a theorem. [ 0.0 0.0 0.0 ] LEGAL-BOOKP (PROVE-LEMMA LEGAL-BOOKP-IMPLIES-LEGALP-CDR-ASSOC (REWRITE) (IMPLIES (AND (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD))) WARNING: Note that the rewrite rule LEGAL-BOOKP-IMPLIES-LEGALP-CDR-ASSOC will be stored so as to apply only to terms with the nonrecursive function symbol LEGALP. This conjecture simplifies, expanding the definition of LEGALP, to the following two new formulas: Case 2. (IMPLIES (AND (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LESSP (CDR (ASSOC BOARD ALIST)) 9)). Name the above subgoal *1. Case 1. (IMPLIES (AND (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (NOT (NTH (CDR (ASSOC BOARD ALIST)) BOARD))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (IMPLIES (AND (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which we named *1 above. We will appeal to induction. Three inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP ALIST) (p BOARD ALIST)) (IMPLIES (AND (NOT (NLISTP ALIST)) (EQUAL BOARD (CAAR ALIST))) (p BOARD ALIST)) (IMPLIES (AND (NOT (NLISTP ALIST)) (NOT (EQUAL BOARD (CAAR ALIST))) (p BOARD (CDR ALIST))) (p BOARD ALIST))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to show that the measure (COUNT ALIST) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces five new conjectures: Case 5. (IMPLIES (AND (NLISTP ALIST) (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which simplifies, unfolding the definitions of NLISTP, LEGAL-BOOKP, and ASSOC, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP ALIST)) (EQUAL BOARD (CAAR ALIST)) (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which simplifies, expanding NLISTP, LEGAL-BOOKP, LEGALP, ASSOC, and EQUAL, to: T. Case 3. (IMPLIES (AND (NOT (NLISTP ALIST)) (NOT (EQUAL BOARD (CAAR ALIST))) (NOT (LEGAL-BOOKP (CDR ALIST))) (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which simplifies, expanding the functions NLISTP, LEGAL-BOOKP, and LEGALP, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP ALIST)) (NOT (EQUAL BOARD (CAAR ALIST))) (NOT (ASSOC BOARD (CDR ALIST))) (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which simplifies, opening up NLISTP, LEGAL-BOOKP, LEGALP, and ASSOC, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP ALIST)) (NOT (EQUAL BOARD (CAAR ALIST))) (LEGALP (CDR (ASSOC BOARD (CDR ALIST))) BOARD) (LEGAL-BOOKP ALIST) (ASSOC BOARD ALIST)) (LEGALP (CDR (ASSOC BOARD ALIST)) BOARD)), which simplifies, unfolding the definitions of NLISTP, LEGALP, LEGAL-BOOKP, ASSOC, and EQUAL, to: T. That finishes the proof of *1. Q.E.D. [ 0.0 0.0 0.0 ] LEGAL-BOOKP-IMPLIES-LEGALP-CDR-ASSOC (DEFN PICK-MOVE2 (BOARD) (COND ((NLISTP BOARD) 0) ((EQUAL (CAR BOARD) F) 0) (T (ADD1 (PICK-MOVE2 (CDR BOARD)))))) Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each recursive call. Hence, PICK-MOVE2 is accepted under the definitional principle. From the definition we can conclude that (NUMBERP (PICK-MOVE2 BOARD)) is a theorem. [ 0.0 0.0 0.0 ] PICK-MOVE2 (PROVE-LEMMA NOT-ENDP-IMPLIES-LEGALP-PICK-MOVE2 (REWRITE) (IMPLIES (AND (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD))) WARNING: Note that the rewrite rule NOT-ENDP-IMPLIES-LEGALP-PICK-MOVE2 will be stored so as to apply only to terms with the nonrecursive function symbol LEGALP. This conjecture simplifies, unfolding the definition of LEGALP, to two new conjectures: Case 2. (IMPLIES (AND (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LESSP (PICK-MOVE2 BOARD) 9)), which we will name *1. Case 1. (IMPLIES (AND (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (NOT (NTH (PICK-MOVE2 BOARD) BOARD))), which we would usually push and work on later by induction. But if we must use induction to prove the input conjecture, we prefer to induct on the original formulation of the problem. Thus we will disregard all that we have previously done, give the name *1 to the original input, and work on it. So now let us consider: (IMPLIES (AND (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)), which we named *1 above. We will appeal to induction. The recursive terms in the conjecture suggest three inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP BOARD) (p BOARD)) (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (p (CDR BOARD))) (p BOARD)) (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (CAR BOARD))) (p BOARD))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT BOARD) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following five new conjectures: Case 5. (IMPLIES (AND (NLISTP BOARD) (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)). This simplifies, expanding the definitions of NLISTP and ENDP, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (ENDP (CDR BOARD)) (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)). This simplifies, unfolding NLISTP and ENDP, to: T. Case 3. (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (NOT (LESSP (LENGTH (CDR BOARD)) 10)) (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)). This simplifies, applying SUB1-ADD1, and unfolding the definitions of NLISTP, ENDP, LENGTH, SUB1, NUMBERP, EQUAL, LESSP, PICK-MOVE2, NTH, and LEGALP, to two new formulas: Case 3.2. (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (LENGTH (CDR BOARD)) 10)) (NOT (ENDP (CDR BOARD))) (LESSP (LENGTH (CDR BOARD)) 9)) (LESSP (PICK-MOVE2 (CDR BOARD)) 8)), which again simplifies, using linear arithmetic, to: T. Case 3.1. (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (NOT (LESSP (LENGTH (CDR BOARD)) 10)) (NOT (ENDP (CDR BOARD))) (LESSP (LENGTH (CDR BOARD)) 9)) (NOT (NTH (PICK-MOVE2 (CDR BOARD)) (CDR BOARD)))), which again simplifies, using linear arithmetic, to: T. Case 2. (IMPLIES (AND (NOT (NLISTP BOARD)) (CAR BOARD) (LEGALP (PICK-MOVE2 (CDR BOARD)) (CDR BOARD)) (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)), which simplifies, applying the lemma SUB1-ADD1, and unfolding the definitions of NLISTP, LEGALP, ENDP, LENGTH, SUB1, NUMBERP, EQUAL, LESSP, PICK-MOVE2, and NTH, to the formula: (IMPLIES (AND (LISTP BOARD) (CAR BOARD) (LESSP (PICK-MOVE2 (CDR BOARD)) 9) (NOT (NTH (PICK-MOVE2 (CDR BOARD)) (CDR BOARD))) (NOT (ENDP (CDR BOARD))) (LESSP (LENGTH (CDR BOARD)) 9)) (LESSP (PICK-MOVE2 (CDR BOARD)) 8)). However this again simplifies, using linear arithmetic, to: (IMPLIES (AND (EQUAL (PICK-MOVE2 (CDR BOARD)) 8) (LISTP BOARD) (CAR BOARD) (LESSP 8 9) (NOT (NTH 8 (CDR BOARD))) (NOT (ENDP (CDR BOARD))) (LESSP (LENGTH (CDR BOARD)) 9)) (LESSP 8 8)). However this again simplifies, unfolding the function LESSP, to: (IMPLIES (AND (EQUAL (PICK-MOVE2 (CDR BOARD)) 8) (LISTP BOARD) (CAR BOARD) (NOT (NTH 8 (CDR BOARD))) (NOT (ENDP (CDR BOARD)))) (NOT (LESSP (LENGTH (CDR BOARD)) 9))). Appealing to the lemma CAR-CDR-ELIM, we now replace BOARD by (CONS Z X) to eliminate (CDR BOARD) and (CAR BOARD). The result is: (IMPLIES (AND (EQUAL (PICK-MOVE2 X) 8) Z (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). Eliminate the irrelevant term. We would thus like to prove: (IMPLIES (AND (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))), which we will finally name *1.1. Case 1. (IMPLIES (AND (NOT (NLISTP BOARD)) (NOT (CAR BOARD)) (NOT (ENDP BOARD)) (LESSP (LENGTH BOARD) 10)) (LEGALP (PICK-MOVE2 BOARD) BOARD)). This simplifies, appealing to the lemma SUB1-ADD1, and expanding the definitions of NLISTP, ENDP, LENGTH, SUB1, NUMBERP, EQUAL, LESSP, PICK-MOVE2, NTH, and LEGALP, to: T. So let us turn our attention to: (IMPLIES (AND (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))), which is formula *1.1 above. We will appeal to induction. The recursive terms in the conjecture suggest three inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP X) (p X)) (IMPLIES (AND (NOT (NLISTP X)) (EQUAL (CAR X) F)) (p X)) (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (CAR X) F)) (p (CDR X))) (p X))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP 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 leads to the following six new goals: Case 6. (IMPLIES (AND (NLISTP X) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). This simplifies, expanding the functions NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (NLISTP X)) (EQUAL (CAR X) F) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). This simplifies, unfolding the definitions of NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (CAR X) F)) (NOT (EQUAL (PICK-MOVE2 (CDR X)) 8)) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). This simplifies, rewriting with the lemmas ADD1-EQUAL and SUB1-ADD1, and opening up NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP X) (CAR X) (NOT (EQUAL (PICK-MOVE2 (CDR X)) 8)) (EQUAL (PICK-MOVE2 (CDR X)) 7) (NOT (NTH 8 X)) (NOT (ENDP (CDR X)))) (NOT (LESSP (LENGTH (CDR X)) 8))), which again simplifies, opening up the definition of EQUAL, to the formula: (IMPLIES (AND (LISTP X) (CAR X) (EQUAL (PICK-MOVE2 (CDR X)) 7) (NOT (NTH 8 X)) (NOT (ENDP (CDR X)))) (NOT (LESSP (LENGTH (CDR X)) 8))). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to eliminate (CAR X) and (CDR X). This generates: (IMPLIES (AND Z (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 8 (CONS Z V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). But this further simplifies, rewriting with CDR-CONS, and unfolding the definitions of SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND Z (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which has an irrelevant term in it. By eliminating the term we get: (IMPLIES (AND (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which we will finally name *1.1.1. Case 3. (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (CAR X) F)) (NTH 8 (CDR X)) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). This simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and unfolding the functions NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP X) (CAR X) (NTH 8 (CDR X)) (EQUAL (PICK-MOVE2 (CDR X)) 7) (NOT (NTH 8 X)) (NOT (ENDP (CDR X)))) (NOT (LESSP (LENGTH (CDR X)) 8))). Appealing to the lemma CAR-CDR-ELIM, we now replace X by (CONS Z V) to eliminate (CAR X) and (CDR X). We must thus prove the formula: (IMPLIES (AND Z (NTH 8 V) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 8 (CONS Z V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). However this further simplifies, appealing to the lemma CDR-CONS, and expanding the definitions of SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND Z (NTH 8 V) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). Eliminate the irrelevant term. We would thus like to prove: (IMPLIES (AND (NTH 8 V) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which we will name *1.1.2. Case 2. (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (CAR X) F)) (ENDP (CDR X)) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))). This simplifies, rewriting with ADD1-EQUAL, and expanding the definitions of NLISTP, PICK-MOVE2, NUMBERP, and ENDP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP X)) (NOT (EQUAL (CAR X) F)) (NOT (LESSP (LENGTH (CDR X)) 9)) (EQUAL (PICK-MOVE2 X) 8) (NOT (NTH 8 X)) (NOT (ENDP X))) (NOT (LESSP (LENGTH X) 9))), which simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and opening up the functions NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP X) (CAR X) (NOT (LESSP (LENGTH (CDR X)) 9)) (EQUAL (PICK-MOVE2 (CDR X)) 7) (NOT (NTH 8 X)) (NOT (ENDP (CDR X)))) (NOT (LESSP (LENGTH (CDR X)) 8))), which again simplifies, using linear arithmetic, to: T. So we now return to: (IMPLIES (AND (NTH 8 V) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which we named *1.1.2 above. Ah ha! This conjecture is subsumed by the subgoal we named *1.1.1 above. So let us turn our attention to: (IMPLIES (AND (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which we named *1.1.1 above. Let us appeal to the induction principle. Three inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP V) (p V)) (IMPLIES (AND (NOT (NLISTP V)) (EQUAL (CAR V) F)) (p V)) (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (p (CDR V))) (p V))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP establish that the measure (COUNT V) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme produces six new goals: Case 6. (IMPLIES (AND (NLISTP V) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which simplifies, expanding the functions NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (NLISTP V)) (EQUAL (CAR V) F) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which simplifies, opening up the functions NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NOT (EQUAL (PICK-MOVE2 (CDR V)) 7)) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))), which simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and opening up the functions NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP V) (CAR V) (NOT (EQUAL (PICK-MOVE2 (CDR V)) 7)) (EQUAL (PICK-MOVE2 (CDR V)) 6) (NOT (NTH 7 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 7))), which again simplifies, expanding EQUAL, to: (IMPLIES (AND (LISTP V) (CAR V) (EQUAL (PICK-MOVE2 (CDR V)) 6) (NOT (NTH 7 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 7))). Appealing to the lemma CAR-CDR-ELIM, we now replace V by (CONS X Z) to eliminate (CAR V) and (CDR V). We must thus prove: (IMPLIES (AND X (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 7 (CONS X Z))) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). But this further simplifies, rewriting with the lemma CDR-CONS, and unfolding the functions SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). Eliminate the irrelevant term. This produces: (IMPLIES (AND (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), which we will finally name *1.1.1.1. Case 3. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NTH 7 (CDR V)) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). This simplifies, applying the lemmas ADD1-EQUAL and SUB1-ADD1, and expanding the definitions of NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to the new formula: (IMPLIES (AND (LISTP V) (CAR V) (NTH 7 (CDR V)) (EQUAL (PICK-MOVE2 (CDR V)) 6) (NOT (NTH 7 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 7))). Applying the lemma CAR-CDR-ELIM, replace V by (CONS X Z) to eliminate (CAR V) and (CDR V). We would thus like to prove: (IMPLIES (AND X (NTH 7 Z) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 7 (CONS X Z))) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), which further simplifies, applying the lemma CDR-CONS, and opening up the definitions of SUB1, NUMBERP, EQUAL, and NTH, to the conjecture: (IMPLIES (AND X (NTH 7 Z) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). Eliminate the irrelevant term. We thus obtain the new goal: (IMPLIES (AND (NTH 7 Z) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), which we will name *1.1.1.2. Case 2. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (ENDP (CDR V)) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). This simplifies, applying the lemma ADD1-EQUAL, and expanding NLISTP, PICK-MOVE2, NUMBERP, and ENDP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NOT (LESSP (LENGTH (CDR V)) 8)) (EQUAL (PICK-MOVE2 V) 7) (NOT (NTH 7 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 8))). This simplifies, applying ADD1-EQUAL and SUB1-ADD1, and expanding NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to the goal: (IMPLIES (AND (LISTP V) (CAR V) (NOT (LESSP (LENGTH (CDR V)) 8)) (EQUAL (PICK-MOVE2 (CDR V)) 6) (NOT (NTH 7 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 7))). However this again simplifies, using linear arithmetic, to: T. So we now return to: (IMPLIES (AND (NTH 7 Z) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), which is formula *1.1.1.2 above. But this conjecture is subsumed by the subgoal we named *1.1.1.1 above. So let us turn our attention to: (IMPLIES (AND (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), named *1.1.1.1 above. Let us appeal to the induction principle. Three inductions are suggested by terms in the conjecture. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP Z) (p Z)) (IMPLIES (AND (NOT (NLISTP Z)) (EQUAL (CAR Z) F)) (p Z)) (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (p (CDR Z))) (p Z))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP can be used to prove that the measure (COUNT Z) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to the following six new goals: Case 6. (IMPLIES (AND (NLISTP Z) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). This simplifies, unfolding the functions NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (NLISTP Z)) (EQUAL (CAR Z) F) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). This simplifies, unfolding the definitions of NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NOT (EQUAL (PICK-MOVE2 (CDR Z)) 6)) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). This simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and expanding NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP Z) (CAR Z) (NOT (EQUAL (PICK-MOVE2 (CDR Z)) 6)) (EQUAL (PICK-MOVE2 (CDR Z)) 5) (NOT (NTH 6 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 6))). But this again simplifies, opening up EQUAL, to: (IMPLIES (AND (LISTP Z) (CAR Z) (EQUAL (PICK-MOVE2 (CDR Z)) 5) (NOT (NTH 6 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 6))). Appealing to the lemma CAR-CDR-ELIM, we now replace Z by (CONS X V) to eliminate (CAR Z) and (CDR Z). The result is: (IMPLIES (AND X (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 6 (CONS X V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). This further simplifies, applying the lemma CDR-CONS, and expanding SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). Eliminate the irrelevant term. We thus obtain: (IMPLIES (AND (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which we will finally name *1.1.1.1.1. Case 3. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NTH 6 (CDR Z)) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). This simplifies, applying ADD1-EQUAL and SUB1-ADD1, and expanding the definitions of NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP Z) (CAR Z) (NTH 6 (CDR Z)) (EQUAL (PICK-MOVE2 (CDR Z)) 5) (NOT (NTH 6 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 6))). Appealing to the lemma CAR-CDR-ELIM, we now replace Z by (CONS X V) to eliminate (CAR Z) and (CDR Z). The result is: (IMPLIES (AND X (NTH 6 V) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 6 (CONS X V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). But this further simplifies, applying CDR-CONS, and opening up the functions SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (NTH 6 V) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which has an irrelevant term in it. By eliminating the term we get: (IMPLIES (AND (NTH 6 V) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which we will name *1.1.1.1.2. Case 2. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (ENDP (CDR Z)) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))). This simplifies, rewriting with ADD1-EQUAL, and unfolding NLISTP, PICK-MOVE2, NUMBERP, and ENDP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NOT (LESSP (LENGTH (CDR Z)) 7)) (EQUAL (PICK-MOVE2 Z) 6) (NOT (NTH 6 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 7))), which simplifies, rewriting with the lemmas ADD1-EQUAL and SUB1-ADD1, and opening up NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP Z) (CAR Z) (NOT (LESSP (LENGTH (CDR Z)) 7)) (EQUAL (PICK-MOVE2 (CDR Z)) 5) (NOT (NTH 6 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 6))). But this again simplifies, using linear arithmetic, to: T. So next consider: (IMPLIES (AND (NTH 6 V) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which is formula *1.1.1.1.2 above. You probably did not notice, but this conjecture is subsumed by another subgoal awaiting our attention, namely *1.1.1.1.1 above. So next consider: (IMPLIES (AND (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), named *1.1.1.1.1 above. Let us appeal to the induction principle. There are three plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP V) (p V)) (IMPLIES (AND (NOT (NLISTP V)) (EQUAL (CAR V) F)) (p V)) (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (p (CDR V))) (p V))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT V) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme generates six new formulas: Case 6. (IMPLIES (AND (NLISTP V) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which simplifies, opening up NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (NLISTP V)) (EQUAL (CAR V) F) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which simplifies, unfolding the definitions of NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NOT (EQUAL (PICK-MOVE2 (CDR V)) 5)) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))), which simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and expanding the definitions of NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP V) (CAR V) (NOT (EQUAL (PICK-MOVE2 (CDR V)) 5)) (EQUAL (PICK-MOVE2 (CDR V)) 4) (NOT (NTH 5 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 5))), which again simplifies, opening up the function EQUAL, to the formula: (IMPLIES (AND (LISTP V) (CAR V) (EQUAL (PICK-MOVE2 (CDR V)) 4) (NOT (NTH 5 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 5))). Appealing to the lemma CAR-CDR-ELIM, we now replace V by (CONS X Z) to eliminate (CAR V) and (CDR V). This generates the goal: (IMPLIES (AND X (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 5 (CONS X Z))) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))). But this further simplifies, appealing to the lemma CDR-CONS, and expanding SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))). Eliminate the irrelevant term. This produces: (IMPLIES (AND (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which we will finally name *1.1.1.1.1.1. Case 3. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NTH 5 (CDR V)) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). This simplifies, applying the lemmas ADD1-EQUAL and SUB1-ADD1, and unfolding the functions NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP V) (CAR V) (NTH 5 (CDR V)) (EQUAL (PICK-MOVE2 (CDR V)) 4) (NOT (NTH 5 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 5))). Applying the lemma CAR-CDR-ELIM, replace V by (CONS X Z) to eliminate (CAR V) and (CDR V). This produces: (IMPLIES (AND X (NTH 5 Z) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 5 (CONS X Z))) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which further simplifies, rewriting with CDR-CONS, and unfolding the functions SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (NTH 5 Z) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which has an irrelevant term in it. By eliminating the term we get: (IMPLIES (AND (NTH 5 Z) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which we will name *1.1.1.1.1.2. Case 2. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (ENDP (CDR V)) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). This simplifies, rewriting with the lemma ADD1-EQUAL, and expanding the definitions of NLISTP, PICK-MOVE2, NUMBERP, and ENDP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP V)) (NOT (EQUAL (CAR V) F)) (NOT (LESSP (LENGTH (CDR V)) 6)) (EQUAL (PICK-MOVE2 V) 5) (NOT (NTH 5 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 6))). This simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and unfolding the definitions of NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP V) (CAR V) (NOT (LESSP (LENGTH (CDR V)) 6)) (EQUAL (PICK-MOVE2 (CDR V)) 4) (NOT (NTH 5 V)) (NOT (ENDP (CDR V)))) (NOT (LESSP (LENGTH (CDR V)) 5))). However this again simplifies, using linear arithmetic, to: T. So let us turn our attention to: (IMPLIES (AND (NTH 5 Z) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), named *1.1.1.1.1.2 above. Ah ha! This conjecture is subsumed by the subgoal we named *1.1.1.1.1.1 above. So we now return to: (IMPLIES (AND (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which is formula *1.1.1.1.1.1 above. We will try to prove it by induction. There are three plausible inductions. However, they merge into one likely candidate induction. We will induct according to the following scheme: (AND (IMPLIES (NLISTP Z) (p Z)) (IMPLIES (AND (NOT (NLISTP Z)) (EQUAL (CAR Z) F)) (p Z)) (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (p (CDR Z))) (p Z))). Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of NLISTP inform us that the measure (COUNT Z) decreases according to the well-founded relation LESSP in each induction step of the scheme. The above induction scheme leads to six new goals: Case 6. (IMPLIES (AND (NLISTP Z) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which simplifies, opening up the definitions of NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 5. (IMPLIES (AND (NOT (NLISTP Z)) (EQUAL (CAR Z) F) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which simplifies, expanding NLISTP, PICK-MOVE2, and EQUAL, to: T. Case 4. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NOT (EQUAL (PICK-MOVE2 (CDR Z)) 4)) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))), which simplifies, rewriting with ADD1-EQUAL and SUB1-ADD1, and unfolding the definitions of NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to: (IMPLIES (AND (LISTP Z) (CAR Z) (NOT (EQUAL (PICK-MOVE2 (CDR Z)) 4)) (EQUAL (PICK-MOVE2 (CDR Z)) 3) (NOT (NTH 4 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 4))), which again simplifies, expanding EQUAL, to: (IMPLIES (AND (LISTP Z) (CAR Z) (EQUAL (PICK-MOVE2 (CDR Z)) 3) (NOT (NTH 4 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 4))). Appealing to the lemma CAR-CDR-ELIM, we now replace Z by (CONS X V) to eliminate (CAR Z) and (CDR Z). The result is the conjecture: (IMPLIES (AND X (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 4 (CONS X V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))). But this further simplifies, applying the lemma CDR-CONS, and opening up the functions SUB1, NUMBERP, EQUAL, and NTH, to the formula: (IMPLIES (AND X (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 3 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))). Eliminate the irrelevant term. This produces: (IMPLIES (AND (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 3 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))), which we will finally name *1.1.1.1.1.1.1. Case 3. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NTH 4 (CDR Z)) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))). This simplifies, applying ADD1-EQUAL and SUB1-ADD1, and unfolding NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to the conjecture: (IMPLIES (AND (LISTP Z) (CAR Z) (NTH 4 (CDR Z)) (EQUAL (PICK-MOVE2 (CDR Z)) 3) (NOT (NTH 4 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 4))). Appealing to the lemma CAR-CDR-ELIM, we now replace Z by (CONS X V) to eliminate (CAR Z) and (CDR Z). The result is: (IMPLIES (AND X (NTH 4 V) (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 4 (CONS X V))) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))). However this further simplifies, rewriting with CDR-CONS, and opening up the definitions of SUB1, NUMBERP, EQUAL, and NTH, to: (IMPLIES (AND X (NTH 4 V) (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 3 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))), which has an irrelevant term in it. By eliminating the term we get the new formula: (IMPLIES (AND (NTH 4 V) (EQUAL (PICK-MOVE2 V) 3) (NOT (NTH 3 V)) (NOT (ENDP V))) (NOT (LESSP (LENGTH V) 4))), which we will name *1.1.1.1.1.1.2. Case 2. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (ENDP (CDR Z)) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))). This simplifies, rewriting with the lemma ADD1-EQUAL, and opening up the functions NLISTP, PICK-MOVE2, NUMBERP, and ENDP, to: T. Case 1. (IMPLIES (AND (NOT (NLISTP Z)) (NOT (EQUAL (CAR Z) F)) (NOT (LESSP (LENGTH (CDR Z)) 5)) (EQUAL (PICK-MOVE2 Z) 4) (NOT (NTH 4 Z)) (NOT (ENDP Z))) (NOT (LESSP (LENGTH Z) 5))). This simplifies, applying ADD1-EQUAL and SUB1-ADD1, and unfolding NLISTP, PICK-MOVE2, NUMBERP, ENDP, LENGTH, SUB1, EQUAL, and LESSP, to the conjecture: (IMPLIES (AND (LISTP Z) (CAR Z) (NOT (LESSP (LENGTH (CDR Z)) 5)) (EQUAL (PICK-MOVE2 (CDR Z)) 3) (NOT (NTH 4 Z)) (NOT (ENDP (CDR Z)))) (NOT (LESSP (LENGTH (CDR Z)) 4))). However this again simplifies, using linear arithmetic, to: T. So we now return to: (IMPLIES (AND (NTH 4 V)