(NOTE-LIB "unsolv" T)
Loading ./basic/unsolv.lib
Finished loading ./basic/unsolv.lib
Loading ./basic/unsolv.o
Finished loading ./basic/unsolv.o
(#./basic/unsolv.lib #./basic/unsolv)
(COMPILE-UNCOMPILED-DEFNS "tmp")
Loading ./basic/tmp.o
Finished loading ./basic/tmp.o
/v/hank/v28/boyer/nqthm-2nd/nqthm-1992/examples/basic/tmp.lisp
(DEFN SYMBOL (X) (MEMBER X '(0 1)))
Observe that (OR (FALSEP (SYMBOL X)) (TRUEP (SYMBOL X))) is a theorem.
[ 0.0 0.0 0.0 ]
SYMBOL
(DEFN HALF-TAPE
(X)
(IF (NLISTP X)
(EQUAL X 0)
(AND (SYMBOL (CAR X))
(HALF-TAPE (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, HALF-TAPE
is accepted under the principle of definition. Note that:
(OR (FALSEP (HALF-TAPE X))
(TRUEP (HALF-TAPE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
HALF-TAPE
(DEFN TAPE
(X)
(AND (LISTP X)
(HALF-TAPE (CAR X))
(HALF-TAPE (CDR X))))
Observe that (OR (FALSEP (TAPE X)) (TRUEP (TAPE X))) is a theorem.
[ 0.0 0.0 0.0 ]
TAPE
(DEFN OPERATION
(X)
(MEMBER X '(L R 0 1)))
From the definition we can conclude that:
(OR (FALSEP (OPERATION X))
(TRUEP (OPERATION X)))
is a theorem.
[ 0.0 0.0 0.0 ]
OPERATION
(DEFN STATE (X) (LITATOM X))
Observe that (OR (FALSEP (STATE X)) (TRUEP (STATE X))) is a theorem.
[ 0.0 0.0 0.0 ]
STATE
(DEFN TURING-4TUPLE
(X)
(AND (LISTP X)
(STATE (CAR X))
(SYMBOL (CADR X))
(OPERATION (CADDR X))
(STATE (CADDDR X))
(EQUAL (CDDDDR X) NIL)))
Note that (OR (FALSEP (TURING-4TUPLE X)) (TRUEP (TURING-4TUPLE X))) is a
theorem.
[ 0.0 0.0 0.0 ]
TURING-4TUPLE
(DEFN TURING-MACHINE
(X)
(IF (NLISTP X)
(EQUAL X NIL)
(AND (TURING-4TUPLE (CAR X))
(TURING-MACHINE (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,
TURING-MACHINE is accepted under the principle of definition. Note that:
(OR (FALSEP (TURING-MACHINE X))
(TRUEP (TURING-MACHINE X)))
is a theorem.
[ 0.0 0.0 0.0 ]
TURING-MACHINE
(DEFN INSTR
(ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TM) decreases according to the well-founded relation LESSP in each
recursive call. Hence, INSTR is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
INSTR
(DEFN NEW-TAPE
(OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
Observe that (LISTP (NEW-TAPE OP TAPE)) is a theorem.
[ 0.0 0.0 0.0 ]
NEW-TAPE
(DEFN TMI
(ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM
(SUB1 N))
TAPE)))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to prove that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, TMI is accepted
under the principle of definition. Observe that:
(OR (OR (LISTP (TMI ST TAPE TM N))
(BTMP (TMI ST TAPE TM N)))
(EQUAL (TMI ST TAPE TM N) TAPE))
is a theorem.
[ 0.0 0.1 0.0 ]
TMI
(DEFN INSTR-DEFN NIL
'((ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F)))
From the definition we can conclude that (LISTP (INSTR-DEFN)) is a
theorem.
[ 0.0 0.0 0.0 ]
INSTR-DEFN
(DEFN NEW-TAPE-DEFN NIL
'((OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE))))))))
Note that (LISTP (NEW-TAPE-DEFN)) is a theorem.
[ 0.0 0.0 0.0 ]
NEW-TAPE-DEFN
(DEFN TMI-DEFN NIL
'((ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE)))
Note that (LISTP (TMI-DEFN)) is a theorem.
[ 0.0 0.0 0.0 ]
TMI-DEFN
(DEFN KWOTE (X) (LIST 'QUOTE X))
Observe that (LISTP (KWOTE X)) is a theorem.
[ 0.0 0.0 0.0 ]
KWOTE
(DEFN TMI-FA
(TM)
(LIST (LIST 'TM NIL (KWOTE TM))
(CONS 'INSTR (INSTR-DEFN))
(CONS 'NEW-TAPE (NEW-TAPE-DEFN))
(CONS 'TMI (TMI-DEFN))))
Observe that (LISTP (TMI-FA TM)) is a theorem.
[ 0.0 0.0 0.0 ]
TMI-FA
(DEFN TMI-X
(ST TAPE)
(LIST 'TMI
(KWOTE ST)
(KWOTE TAPE)
'(TM)))
From the definition we can conclude that (LISTP (TMI-X ST TAPE)) is a
theorem.
[ 0.0 0.0 0.0 ]
TMI-X
(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
(DEFN TMI-K
(ST TAPE TM N)
(DIFFERENCE N (ADD1 (LENGTH TM))))
WARNING: ST and TAPE are in the arglist but not in the body of the definition
of TMI-K.
Observe that (NUMBERP (TMI-K ST TAPE TM N)) is a theorem.
[ 0.0 0.0 0.0 ]
TMI-K
(DEFN TMI-N
(ST TAPE TM K)
(PLUS K (ADD1 (LENGTH TM))))
WARNING: ST and TAPE are in the arglist but not in the body of the definition
of TMI-N.
Observe that (NUMBERP (TMI-N ST TAPE TM K)) is a theorem.
[ 0.0 0.0 0.0 ]
TMI-N
(PROVE-LEMMA LENGTH-0
(REWRITE)
(EQUAL (EQUAL (LENGTH X) 0)
(NLISTP X)))
This formula simplifies, opening up the definition of NLISTP, to two new
conjectures:
Case 2. (IMPLIES (NOT (EQUAL (LENGTH X) 0))
(LISTP X)),
which again simplifies, unfolding the definitions of LENGTH and EQUAL, to:
T.
Case 1. (IMPLIES (EQUAL (LENGTH X) 0)
(NOT (LISTP X))),
which we will name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP X) (p X))
(IMPLIES (AND (NOT (NLISTP X)) (p (CDR X)))
(p X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP 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 produces three new formulas:
Case 3. (IMPLIES (AND (NLISTP X) (EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, opening up NLISTP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NOT (EQUAL (LENGTH (CDR X)) 0))
(EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, opening up NLISTP and LENGTH, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(NOT (LISTP (CDR X)))
(EQUAL (LENGTH X) 0))
(NOT (LISTP X))),
which simplifies, expanding the definitions of NLISTP and LENGTH, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
LENGTH-0
(PROVE-LEMMA PLUS-EQUAL-0
(REWRITE)
(EQUAL (EQUAL (PLUS I J) 0)
(AND (ZEROP I) (ZEROP J))))
This simplifies, opening up the functions ZEROP and AND, to six new
conjectures:
Case 6. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
(NOT (NUMBERP I)))
(NOT (EQUAL J 0))),
which again simplifies, expanding NUMBERP, PLUS, and EQUAL, to:
T.
Case 5. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
(NOT (NUMBERP I)))
(NUMBERP J)),
which again simplifies, unfolding PLUS and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
(EQUAL I 0))
(NOT (EQUAL J 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (PLUS I J) 0))
(EQUAL I 0))
(NUMBERP J)),
which again simplifies, expanding the functions EQUAL and PLUS, to:
T.
Case 2. (IMPLIES (AND (EQUAL (PLUS I J) 0)
(NOT (EQUAL I 0)))
(NOT (NUMBERP I))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (EQUAL (PLUS I J) 0)
(NOT (EQUAL J 0)))
(NOT (NUMBERP J))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PLUS-EQUAL-0
(PROVE-LEMMA PLUS-DIFFERENCE
(REWRITE)
(EQUAL (PLUS (DIFFERENCE I J) J)
(IF (LEQ I J) (FIX J) I)))
This simplifies, expanding FIX, to three new goals:
Case 3. (IMPLIES (AND (NOT (LESSP J I)) (NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which we will name *1.
Case 2. (IMPLIES (AND (NOT (LESSP J I))
(NOT (NUMBERP J)))
(EQUAL (PLUS (DIFFERENCE I J) J) 0)).
But this again simplifies, opening up the functions LESSP, EQUAL, DIFFERENCE,
and PLUS, to:
T.
Case 1. (IMPLIES (LESSP J I)
(EQUAL (PLUS (DIFFERENCE I J) J) I)),
which again simplifies, using linear arithmetic, to two new conjectures:
Case 1.2.
(IMPLIES (AND (LESSP I J) (LESSP J I))
(EQUAL (PLUS (DIFFERENCE I J) J) I)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (NUMBERP I)) (LESSP J I))
(EQUAL (PLUS (DIFFERENCE I J) J) I)),
which again simplifies, unfolding LESSP, to:
T.
So we now return to:
(IMPLIES (AND (NOT (LESSP J I)) (NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
named *1 above. Let us appeal to the induction principle. The recursive
terms in the conjecture suggest four inductions. However, they merge into one
likely candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL I 0) (NOT (NUMBERP I)))
(p I J))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL J 0) (NOT (NUMBERP J))))
(p I J))
(IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(p (SUB1 I) (SUB1 J)))
(p I J))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT J) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for I. The above induction scheme
produces four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL I 0) (NOT (NUMBERP I)))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which simplifies, unfolding the definitions of NOT, OR, EQUAL, LESSP,
DIFFERENCE, and PLUS, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(OR (EQUAL J 0) (NOT (NUMBERP J)))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which simplifies, unfolding the definitions of NOT, OR, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(LESSP (SUB1 J) (SUB1 I))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP I 1)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(LESSP (SUB1 J) (SUB1 I))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)).
But this again simplifies, unfolding SUB1, NUMBERP, EQUAL, LESSP, NOT, and
OR, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which simplifies, using linear arithmetic, to four new formulas:
Case 1.4.
(IMPLIES (AND (LESSP I J)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, using linear arithmetic, to three new conjectures:
Case 1.4.3.
(IMPLIES (AND (EQUAL J 0)
(LESSP I J)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, using linear arithmetic, to:
T.
Case 1.4.2.
(IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
(LESSP I J)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, opening up LESSP, NOT, OR, and DIFFERENCE, to:
(IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
(NOT (EQUAL J 0))
(NOT (EQUAL I 0))
(NUMBERP I)
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) (SUB1 I)))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
J)
J)).
Appealing to the lemma SUB1-ELIM, we now replace I by (ADD1 X) to
eliminate (SUB1 I). We rely upon the type restriction lemma noted when
SUB1 was introduced to constrain the new variable. This generates the
formula:
(IMPLIES (AND (NUMBERP X)
(LESSP X (SUB1 J))
(NOT (EQUAL J 0))
(NOT (EQUAL (ADD1 X) 0))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) X))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
J)).
This further simplifies, clearly, to the new formula:
(IMPLIES (AND (NUMBERP X)
(LESSP X (SUB1 J))
(NOT (EQUAL J 0))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) X))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
J)).
Applying the lemma SUB1-ELIM, replace J by (ADD1 Z) to eliminate
(SUB1 J). We rely upon the type restriction lemma noted when SUB1 was
introduced to restrict the new variable. This produces:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(LESSP X Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 Z))),
which further simplifies, obviously, to the new formula:
(IMPLIES (AND (NUMBERP X)
(LESSP X Z)
(EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 Z))).
We use the above equality hypothesis by cross-fertilizing:
(PLUS (DIFFERENCE X Z) Z)
for Z and throwing away the equality. The result is:
(IMPLIES (AND (NUMBERP X)
(LESSP X Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 (PLUS (DIFFERENCE X Z) Z)))).
We will try to prove the above formula by generalizing it, replacing
(DIFFERENCE X Z) by Y. We restrict the new variable by recalling the
type restriction lemma noted when DIFFERENCE was introduced. We would
thus like to prove:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP X)
(LESSP X Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS Y (ADD1 Z))
(ADD1 (PLUS Y Z)))),
which finally simplifies, using linear arithmetic, to:
T.
Case 1.4.1.
(IMPLIES (AND (LESSP I 1)
(LESSP I J)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, opening up SUB1, NUMBERP, EQUAL, LESSP, NOT, and
OR, to:
T.
Case 1.3.
(IMPLIES (AND (EQUAL J 0)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP I 0)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL 0 0) (NOT (NUMBERP 0))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 0))
(SUB1 0))
(SUB1 0))
(NOT (LESSP 0 I))
(NUMBERP 0))
(EQUAL (PLUS (DIFFERENCE I 0) 0) 0)).
But this again simplifies, using linear arithmetic, to:
T.
Case 1.2.
(IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, unfolding the definitions of NOT, OR, LESSP, and
DIFFERENCE, to the conjecture:
(IMPLIES (AND (LESSP (SUB1 I) (SUB1 J))
(NOT (EQUAL I 0))
(NUMBERP I)
(NOT (EQUAL J 0))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) (SUB1 I)))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
J)
J)).
Appealing to the lemma SUB1-ELIM, we now replace I by (ADD1 X) to
eliminate (SUB1 I). We employ the type restriction lemma noted when SUB1
was introduced to constrain the new variable. This generates the goal:
(IMPLIES (AND (NUMBERP X)
(LESSP X (SUB1 J))
(NOT (EQUAL (ADD1 X) 0))
(NOT (EQUAL J 0))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) X))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
J)).
This further simplifies, trivially, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X (SUB1 J))
(NOT (EQUAL J 0))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP (SUB1 J) X))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE X (SUB1 J)) J)
J)).
Applying the lemma SUB1-ELIM, replace J by (ADD1 Z) to eliminate (SUB1 J).
We rely upon the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. We thus obtain the new conjecture:
(IMPLIES (AND (NUMBERP Z)
(NUMBERP X)
(LESSP X Z)
(NOT (EQUAL (ADD1 Z) 0))
(EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 Z))),
which further simplifies, trivially, to:
(IMPLIES (AND (NUMBERP X)
(LESSP X Z)
(EQUAL (PLUS (DIFFERENCE X Z) Z) Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 Z))).
We now use the above equality hypothesis by cross-fertilizing:
(PLUS (DIFFERENCE X Z) Z)
for Z and throwing away the equality. This generates:
(IMPLIES (AND (NUMBERP X)
(LESSP X Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS (DIFFERENCE X Z) (ADD1 Z))
(ADD1 (PLUS (DIFFERENCE X Z) Z)))).
We will try to prove the above formula by generalizing it, replacing
(DIFFERENCE X Z) by Y. We restrict the new variable by recalling the type
restriction lemma noted when DIFFERENCE was introduced. This produces:
(IMPLIES (AND (NUMBERP Y)
(NUMBERP X)
(LESSP X Z)
(NOT (LESSP Z X)))
(EQUAL (PLUS Y (ADD1 Z))
(ADD1 (PLUS Y Z)))),
which finally simplifies, using linear arithmetic, to:
T.
Case 1.1.
(IMPLIES (AND (LESSP I 1)
(NOT (OR (EQUAL I 0) (NOT (NUMBERP I))))
(NOT (OR (EQUAL J 0) (NOT (NUMBERP J))))
(EQUAL (PLUS (DIFFERENCE (SUB1 I) (SUB1 J))
(SUB1 J))
(SUB1 J))
(NOT (LESSP J I))
(NUMBERP J))
(EQUAL (PLUS (DIFFERENCE I J) J) J)),
which again simplifies, opening up the functions SUB1, NUMBERP, EQUAL,
LESSP, NOT, and OR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.1 ]
PLUS-DIFFERENCE
(TOGGLE DIFFERENCE-OFF DIFFERENCE T)
[ 0.0 0.0 0.0 ]
DIFFERENCE-OFF
(PROVE-LEMMA PR-EVAL-FN-0
(REWRITE)
(IMPLIES (AND (ZEROP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (UNSOLV-SUBRP FN))
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(BTM))))
WARNING: Note that PR-EVAL-FN-0 contains the free variable VARGS which will
be chosen by instantiating the hypothesis:
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)).
This conjecture can be simplified, using the abbreviations NOT, AND, IMPLIES,
and UNSOLV-SUBRP, to:
(IMPLIES (AND (ZEROP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (MEMBER FN
'(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS
CAR CDR LISTP PACK UNPACK LITATOM
EQUAL LIST)))
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(BTM))).
This simplifies, applying the lemmas CDR-CONS and CAR-CONS, and expanding the
definitions of ZEROP, CDR, CAR, LISTP, MEMBER, UNSOLV-SUBRP, EQUAL, and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-FN-0
(PROVE-LEMMA PR-EVAL-FN-1
(REWRITE)
(IMPLIES (AND (NOT (ZEROP N))
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (UNSOLV-SUBRP FN))
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(IF (BTMP VARGS)
(BTM)
(IF (BTMP (GET FN FA))
(BTM)
(EV 'AL
(CADR (GET FN FA))
(PAIRLIST (CAR (GET FN FA)) VARGS)
FA
(SUB1 N)))))))
WARNING: Note that PR-EVAL-FN-1 contains the free variable VARGS which will
be chosen by instantiating the hypothesis:
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)).
This conjecture can be simplified, using the abbreviations ZEROP, NOT, AND,
IMPLIES, and UNSOLV-SUBRP, to:
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (MEMBER FN
'(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS
CAR CDR LISTP PACK UNPACK LITATOM
EQUAL LIST)))
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(COND ((BTMP VARGS) (BTM))
((BTMP (GET FN FA)) (BTM))
(T (EV 'AL
(CADR (GET FN FA))
(PAIRLIST (CAR (GET FN FA)) VARGS)
FA
(SUB1 N)))))).
This simplifies, unfolding the functions CDR, CAR, LISTP, and MEMBER, to the
following three new formulas:
Case 3. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (EQUAL FN 'ZERO))
(NOT (EQUAL FN 'TRUE))
(NOT (EQUAL FN 'FALSE))
(NOT (EQUAL FN 'ADD1))
(NOT (EQUAL FN 'SUB1))
(NOT (EQUAL FN 'NUMBERP))
(NOT (EQUAL FN 'CONS))
(NOT (EQUAL FN 'CAR))
(NOT (EQUAL FN 'CDR))
(NOT (EQUAL FN 'LISTP))
(NOT (EQUAL FN 'PACK))
(NOT (EQUAL FN 'UNPACK))
(NOT (EQUAL FN 'LITATOM))
(NOT (EQUAL FN 'EQUAL))
(NOT (EQUAL FN 'LIST))
(BTMP (EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(BTM))).
But this again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
opening up the definitions of EQUAL and EV, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (EQUAL FN 'ZERO))
(NOT (EQUAL FN 'TRUE))
(NOT (EQUAL FN 'FALSE))
(NOT (EQUAL FN 'ADD1))
(NOT (EQUAL FN 'SUB1))
(NOT (EQUAL FN 'NUMBERP))
(NOT (EQUAL FN 'CONS))
(NOT (EQUAL FN 'CAR))
(NOT (EQUAL FN 'CDR))
(NOT (EQUAL FN 'LISTP))
(NOT (EQUAL FN 'PACK))
(NOT (EQUAL FN 'UNPACK))
(NOT (EQUAL FN 'LITATOM))
(NOT (EQUAL FN 'EQUAL))
(NOT (EQUAL FN 'LIST))
(BTMP (GET FN FA)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(BTM))),
which again simplifies, applying CDR-CONS and CAR-CONS, and unfolding
UNSOLV-SUBRP, CDR, CAR, LISTP, MEMBER, EQUAL, and EV, to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL FN 'QUOTE))
(NOT (EQUAL FN 'IF))
(NOT (EQUAL FN 'ZERO))
(NOT (EQUAL FN 'TRUE))
(NOT (EQUAL FN 'FALSE))
(NOT (EQUAL FN 'ADD1))
(NOT (EQUAL FN 'SUB1))
(NOT (EQUAL FN 'NUMBERP))
(NOT (EQUAL FN 'CONS))
(NOT (EQUAL FN 'CAR))
(NOT (EQUAL FN 'CDR))
(NOT (EQUAL FN 'LISTP))
(NOT (EQUAL FN 'PACK))
(NOT (EQUAL FN 'UNPACK))
(NOT (EQUAL FN 'LITATOM))
(NOT (EQUAL FN 'EQUAL))
(NOT (EQUAL FN 'LIST))
(NOT (BTMP (EV 'LIST ARGS VA FA N)))
(NOT (BTMP (GET FN FA))))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(EV 'AL
(CADR (GET FN FA))
(PAIRLIST (CAR (GET FN FA))
(EV 'LIST ARGS VA FA N))
FA
(SUB1 N)))).
However this again simplifies, rewriting with the lemmas CDR-CONS and
CAR-CONS, and opening up the functions UNSOLV-SUBRP, CDR, CAR, LISTP, MEMBER,
EQUAL, and EV, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
PR-EVAL-FN-1
(PROVE-LEMMA PR-EVAL-UNSOLV-SUBRP
(REWRITE)
(IMPLIES (AND (UNSOLV-SUBRP FN)
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(IF (BTMP VARGS)
(BTM)
(UNSOLV-APPLY-SUBR FN VARGS)))))
WARNING: Note that PR-EVAL-UNSOLV-SUBRP contains the free variable VARGS
which will be chosen by instantiating the hypothesis:
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)).
This conjecture can be simplified, using the abbreviations AND, IMPLIES, and
UNSOLV-SUBRP, to:
(IMPLIES (AND (MEMBER FN
'(ZERO TRUE FALSE ADD1 SUB1 NUMBERP CONS CAR CDR
LISTP PACK UNPACK LITATOM EQUAL LIST))
(EQUAL VARGS
(EV 'LIST ARGS VA FA N)))
(EQUAL (EV 'AL (CONS FN ARGS) VA FA N)
(IF (BTMP VARGS)
(BTM)
(UNSOLV-APPLY-SUBR FN VARGS)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
functions CDR, CAR, LISTP, MEMBER, UNSOLV-APPLY-SUBR, UNSOLV-SUBRP, EQUAL, and
EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-UNSOLV-SUBRP
(PROVE-LEMMA PR-EVAL-IF
(REWRITE)
(IMPLIES (EQUAL VX1 (EV 'AL X1 VA FA N))
(EQUAL (EV 'AL (LIST 'IF X1 X2 X3) VA FA N)
(IF (BTMP VX1)
(BTM)
(IF VX1
(EV 'AL X2 VA FA N)
(EV 'AL X3 VA FA N))))))
WARNING: Note that PR-EVAL-IF contains the free variable VX1 which will be
chosen by instantiating the hypothesis (EQUAL VX1 (EV (QUOTE AL) X1 VA FA N)).
This simplifies, applying CDR-CONS and CAR-CONS, and opening up the functions
EQUAL and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-IF
(PROVE-LEMMA PR-EVAL-QUOTE
(REWRITE)
(EQUAL (EV 'AL (LIST 'QUOTE X) VA FA N)
X))
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up EQUAL
and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-QUOTE
(PROVE-LEMMA PR-EVAL-NLISTP
(REWRITE)
(AND (EQUAL (EV 'AL 0 VA FA N) 0)
(EQUAL (EV 'AL (ADD1 N) VA FA N)
(ADD1 N))
(EQUAL (EV 'AL (PACK X) VA FA N)
(IF (EQUAL (PACK X) 'T)
T
(IF (EQUAL (PACK X) 'F)
F
(IF (EQUAL (PACK X) 'NIL)
NIL
(GET (PACK X) VA)))))))
WARNING: Note that the proposed lemma PR-EVAL-NLISTP is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and three replacement rules.
This formula can be simplified, using the abbreviations AND and PACK-EQUAL, to
the following three new formulas:
Case 3. (EQUAL (EV 'AL 0 VA FA N) 0).
This simplifies, unfolding NUMBERP, LISTP, EQUAL, and EV, to:
T.
Case 2. (EQUAL (EV 'AL (ADD1 N) VA FA N)
(ADD1 N)).
This simplifies, expanding EQUAL and EV, to:
T.
Case 1. (EQUAL (EV 'AL (PACK X) VA FA N)
(CASE X
((84 . 0) T)
((70 . 0) F)
((78 73 76 . 0) NIL)
(OTHERWISE (GET (PACK X) VA)))).
This simplifies, rewriting with the lemmas PACK-EQUAL and UNPACK-PACK, and
expanding UNPACK, EQUAL, and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-NLISTP
(PROVE-LEMMA EVLIST-NIL
(REWRITE)
(EQUAL (EV 'LIST NIL VA FA N) NIL))
This simplifies, unfolding the definitions of LISTP, EQUAL, and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EVLIST-NIL
(PROVE-LEMMA EVLIST-CONS
(REWRITE)
(IMPLIES (AND (EQUAL VX (EV 'AL X VA FA N))
(EQUAL VL (EV 'LIST L VA FA N)))
(EQUAL (EV 'LIST (CONS X L) VA FA N)
(IF (BTMP VX)
(BTM)
(IF (BTMP VL) (BTM) (CONS VX VL))))))
WARNING: Note that EVLIST-CONS contains the free variables VL and VX which
will be chosen by instantiating the hypotheses:
(EQUAL VX (EV 'AL X VA FA N))
and (EQUAL VL (EV (QUOTE LIST) L VA FA N)).
This simplifies, applying CDR-CONS and CAR-CONS, and expanding the functions
EQUAL and EV, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
EVLIST-CONS
(TOGGLE UNSOLV-SUBRP-OFF UNSOLV-SUBRP T)
[ 0.0 0.0 0.0 ]
UNSOLV-SUBRP-OFF
(TOGGLE EV-OFF EV T)
[ 0.0 0.0 0.0 ]
EV-OFF
(DEFN CNB
(X)
(IF (LISTP X)
(AND (CNB (CAR X)) (CNB (CDR X)))
(NOT (BTMP X))))
Linear arithmetic and the lemmas CDR-LESSP and CAR-LESSP establish that
the measure (COUNT X) decreases according to the well-founded relation LESSP
in each recursive call. Hence, CNB is accepted under the definitional
principle. Note that (OR (FALSEP (CNB X)) (TRUEP (CNB X))) is a theorem.
[ 0.0 0.0 0.0 ]
CNB
(PROVE-LEMMA CNB-NBTM
(REWRITE)
(IMPLIES (CNB X) (EQUAL (BTMP X) F)))
This formula simplifies, opening up the definition of CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-NBTM
(PROVE-LEMMA CNB-CONS
(REWRITE)
(AND (EQUAL (CNB (CONS A B))
(AND (CNB A) (CNB B)))
(IMPLIES (CNB X) (CNB (CAR X)))
(IMPLIES (CNB X) (CNB (CDR X)))))
WARNING: Note that the proposed lemma CNB-CONS is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and
three replacement rules.
This formula can be simplified, using the abbreviations IMPLIES and AND, to
the following three new conjectures:
Case 3. (EQUAL (CNB (CONS A B))
(AND (CNB A) (CNB B))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
functions CNB and AND, to:
T.
Case 2. (IMPLIES (CNB X) (CNB (CAR X))),
which simplifies, applying CAR-NLISTP, and unfolding the function CNB, to:
T.
Case 1. (IMPLIES (CNB X) (CNB (CDR X))).
This simplifies, appealing to the lemma CDR-NLISTP, and expanding the
function CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-CONS
(PROVE-LEMMA CNB-LITATOM
(REWRITE)
(IMPLIES (LITATOM X) (CNB X)))
This simplifies, expanding the function CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-LITATOM
(PROVE-LEMMA CNB-NUMBERP
(REWRITE)
(IMPLIES (NUMBERP X) (CNB X)))
This simplifies, expanding the function CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-NUMBERP
(TOGGLE CNB-OFF CNB T)
[ 0.0 0.0 0.0 ]
CNB-OFF
(PROVE-LEMMA GET-TMI-FA
(REWRITE)
(AND (EQUAL (GET 'TM (TMI-FA TM))
(LIST NIL (KWOTE TM)))
(EQUAL (GET 'INSTR (TMI-FA TM))
(INSTR-DEFN))
(EQUAL (GET 'NEW-TAPE (TMI-FA TM))
(NEW-TAPE-DEFN))
(EQUAL (GET 'TMI (TMI-FA TM))
(TMI-DEFN))))
WARNING: Note that the proposed lemma GET-TMI-FA is to be stored as zero type
prescription rules, zero compound recognizer rules, zero linear rules, and
four replacement rules.
This conjecture can be simplified, using the abbreviations AND, TMI-DEFN,
NEW-TAPE-DEFN, INSTR-DEFN, KWOTE, and TMI-FA, to four new goals:
Case 4. (EQUAL
(GET 'TM
(CONS (LIST 'TM NIL (LIST 'QUOTE TM))
'((INSTR (ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
(NEW-TAPE (OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
(TMI (ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE)))))
(LIST NIL (LIST 'QUOTE TM))),
which simplifies, applying CDR-CONS and CAR-CONS, and expanding the
definitions of EQUAL and GET, to:
T.
Case 3. (EQUAL
(GET 'INSTR
(CONS (LIST 'TM NIL (LIST 'QUOTE TM))
'((INSTR (ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
(NEW-TAPE (OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
(TMI (ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE)))))
'((ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding GET and
EQUAL, to:
T.
Case 2. (EQUAL
(GET 'NEW-TAPE
(CONS (LIST 'TM NIL (LIST 'QUOTE TM))
'((INSTR (ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
(NEW-TAPE (OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
(TMI (ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE)))))
'((OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))),
which simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
definitions of GET and EQUAL, to:
T.
Case 1. (EQUAL
(GET 'TMI
(CONS (LIST 'TM NIL (LIST 'QUOTE TM))
'((INSTR (ST SYM TM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTR ST SYM (CDR TM)))
(INSTR ST SYM (CDR TM)))
F))
(NEW-TAPE (OP TAPE)
(IF (EQUAL OP 'L)
(CONS (CDR (CAR TAPE))
(CONS (CAR (CAR TAPE)) (CDR TAPE)))
(IF (EQUAL OP 'R)
(CONS (CONS (CAR (CDR TAPE)) (CAR TAPE))
(CDR (CDR TAPE)))
(CONS (CAR TAPE)
(CONS OP (CDR (CDR TAPE)))))))
(TMI (ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE)))))
'((ST TAPE TM)
(IF (INSTR ST (CAR (CDR TAPE)) TM)
(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
TAPE))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
functions GET and EQUAL, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GET-TMI-FA
(TOGGLE TMI-FA-OFF TMI-FA T)
[ 0.0 0.0 0.0 ]
TMI-FA-OFF
(DEFN INSTRN
(ST SYM TM N)
(IF (ZEROP N)
(BTM)
(IF (LISTP TM)
(IF (EQUAL ST (CAR (CAR TM)))
(IF (EQUAL SYM (CAR (CDR (CAR TM))))
(CDR (CDR (CAR TM)))
(INSTRN ST SYM (CDR TM) (SUB1 N)))
(INSTRN ST SYM (CDR TM) (SUB1 N)))
F)))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT TM) decreases according to the well-founded relation LESSP in each
recursive call. Hence, INSTRN is accepted under the definitional principle.
The definition of INSTRN can be justified in another way. Linear arithmetic,
the lemma COUNT-NUMBERP, and the definition of ZEROP establish that the
measure (COUNT N) decreases according to the well-founded relation LESSP in
each recursive call.
[ 0.0 0.0 0.0 ]
INSTRN
(DEFN PR-EVAL-INSTR-INDUCTION-SCHEME
(ST SYM TM-- VA TM N)
(IF
(ZEROP N)
T
(PR-EVAL-INSTR-INDUCTION-SCHEME 'ST
'SYM
'(CDR TM)
(LIST (CONS 'ST
(PR-EVAL ST VA (TMI-FA TM) N))
(CONS 'SYM
(PR-EVAL SYM VA (TMI-FA TM) N))
(CONS 'TM
(PR-EVAL TM-- VA (TMI-FA TM) N)))
TM
(SUB1 N))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
establish that the measure (COUNT N) decreases according to the well-founded
relation LESSP in each recursive call. Hence, PR-EVAL-INSTR-INDUCTION-SCHEME
is accepted under the definitional principle. From the definition we can
conclude that (TRUEP (PR-EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N)) is
a theorem.
[ 0.0 0.0 0.0 ]
PR-EVAL-INSTR-INDUCTION-SCHEME
(PROVE-LEMMA PR-EVAL-INSTR
(REWRITE)
(IMPLIES (AND (CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'INSTR ST SYM TM--)
VA
(TMI-FA TM)
N)
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N)))
((INDUCT (PR-EVAL-INSTR-INDUCTION-SCHEME ST SYM TM-- VA TM N))))
This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, AND, and PR-EVAL, to two new goals:
Case 2. (IMPLIES (AND (ZEROP N)
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'INSTR ST SYM TM--)
VA
(TMI-FA TM)
N)
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which simplifies, rewriting with EVLIST-CONS, CNB-NBTM, EVLIST-NIL, and
PR-EVAL-FN-0, and opening up the definitions of ZEROP, BTMP, UNSOLV-SUBRP,
EQUAL, and INSTRN, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES
(AND (CNB (EV 'AL
'ST
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))
(CNB (EV 'AL
'SYM
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))
(CNB (EV 'AL
'(CDR TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))))
(EQUAL (EV 'AL
'(INSTR ST SYM (CDR TM))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(INSTRN (EV 'AL
'ST
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL
'SYM
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL
'(CDR TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(SUB1 N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'INSTR ST SYM TM--)
VA
(TMI-FA TM)
N)
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This simplifies, rewriting with CDR-CONS, CAR-CONS, PR-EVAL-NLISTP,
EVLIST-CONS, CNB-NBTM, EVLIST-NIL, PR-EVAL-UNSOLV-SUBRP, CNB-CONS,
GET-TMI-FA, PR-EVAL-IF, and PR-EVAL-FN-1, and expanding the functions PACK,
EQUAL, GET, BTMP, UNSOLV-SUBRP, UNSOLV-APPLY-SUBR, AND, IMPLIES, INSTR-DEFN,
CDR, CAR, LISTP, and PAIRLIST, to four new formulas:
Case 1.4.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EV 'AL
'(INSTR ST SYM (CDR TM))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (LISTP (EV 'AL TM-- VA (TMI-FA TM) N))))
(EQUAL F
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, rewriting with CDR-NLISTP, and unfolding the
definitions of LISTP, INSTRN, and EQUAL, to:
T.
Case 1.3.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EV 'AL
'(INSTR ST SYM (CDR TM))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (EQUAL (EV 'AL ST VA (TMI-FA TM) N)
(CAAR (EV 'AL TM-- VA (TMI-FA TM) N)))))
(EQUAL (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This again simplifies, expanding the definition of INSTRN, to:
T.
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EV 'AL
'(INSTR ST SYM (CDR TM))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (EQUAL (EV 'AL SYM VA (TMI-FA TM) N)
(CADAR (EV 'AL TM-- VA (TMI-FA TM) N)))))
(EQUAL (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, opening up the definition of INSTRN, to:
T.
Case 1.1.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EV 'AL
'(INSTR ST SYM (CDR TM))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'SYM
(EV 'AL SYM VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(CDR (EV 'AL TM-- VA (TMI-FA TM) N))
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL SYM VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(LISTP (EV 'AL TM-- VA (TMI-FA TM) N))
(EQUAL (EV 'AL ST VA (TMI-FA TM) N)
(CAAR (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL SYM VA (TMI-FA TM) N)
(CADAR (EV 'AL TM-- VA (TMI-FA TM) N))))
(EQUAL (CDDAR (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL SYM VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, expanding the function INSTRN, to:
T.
Q.E.D.
[ 0.0 0.1 0.1 ]
PR-EVAL-INSTR
(PROVE-LEMMA PR-EVAL-NEW-TAPE
(REWRITE)
(IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(IF (ZEROP N)
(BTM)
(NEW-TAPE (EV 'AL OP VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N))))))
This conjecture simplifies, opening up the definitions of ZEROP and NEW-TAPE,
to the following five new goals:
Case 5. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(NOT (NUMBERP N)))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(BTM))).
This again simplifies, applying the lemmas EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
and PR-EVAL-FN-0, and expanding the functions BTMP, UNSOLV-SUBRP, EQUAL, and
ZEROP, to:
T.
Case 4. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(EQUAL N 0))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(BTM))),
which again simplifies, rewriting with EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
and PR-EVAL-FN-0, and opening up the functions BTMP, UNSOLV-SUBRP, EQUAL,
and ZEROP, to:
T.
Case 3. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (EV 'AL OP VA (TMI-FA TM) N)
'L))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(CONS (CDAR (EV 'AL TAPE VA (TMI-FA TM) N))
(CONS (CAAR (EV 'AL TAPE VA (TMI-FA TM) N))
(CDR (EV 'AL TAPE VA (TMI-FA TM) N)))))).
However this again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and unfolding CNB,
BTMP, UNSOLV-SUBRP, EQUAL, NEW-TAPE-DEFN, CDR, CAR, CONS, LISTP, PAIRLIST,
UNSOLV-APPLY-SUBR, GET, and PACK, to:
T.
Case 2. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
'L))
(NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
'R)))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(CONS (CAR (EV 'AL TAPE VA (TMI-FA TM) N))
(CONS (EV 'AL OP VA (TMI-FA TM) N)
(CDDR (EV 'AL TAPE VA (TMI-FA TM) N)))))).
This again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and unfolding BTMP,
UNSOLV-SUBRP, EQUAL, NEW-TAPE-DEFN, CDR, CAR, LISTP, PAIRLIST,
UNSOLV-APPLY-SUBR, CONS, GET, and PACK, to:
T.
Case 1. (IMPLIES (AND (CNB (EV 'AL OP VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (EV 'AL OP VA (TMI-FA TM) N)
'L))
(EQUAL (EV 'AL OP VA (TMI-FA TM) N)
'R))
(EQUAL (EV 'AL
(LIST 'NEW-TAPE OP TAPE)
VA
(TMI-FA TM)
N)
(CONS (CONS (CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(CAR (EV 'AL TAPE VA (TMI-FA TM) N)))
(CDDR (EV 'AL TAPE VA (TMI-FA TM) N))))).
But this again simplifies, applying EVLIST-NIL, CNB-NBTM, EVLIST-CONS,
GET-TMI-FA, CDR-CONS, CAR-CONS, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-QUOTE,
PR-EVAL-NLISTP, CNB-CONS, PR-EVAL-IF, and PR-EVAL-FN-1, and opening up the
functions CNB, EQUAL, BTMP, UNSOLV-SUBRP, NEW-TAPE-DEFN, CDR, CAR, CONS,
LISTP, PAIRLIST, UNSOLV-APPLY-SUBR, GET, and PACK, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-NEW-TAPE
(PROVE-LEMMA CNB-INSTRN
(REWRITE)
(IMPLIES (AND (NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))))
Call the conjecture *1.
Let us appeal to the induction principle. There are four plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (ZEROP N) (p ST SYM TM N))
(IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(EQUAL SYM (CADAR TM)))
(p ST SYM TM N))
(IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(NOT (EQUAL SYM (CADAR TM)))
(p ST SYM (CDR TM) (SUB1 N)))
(p ST SYM TM N))
(IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(NOT (EQUAL ST (CAAR TM)))
(p ST SYM (CDR TM) (SUB1 N)))
(p ST SYM TM N))
(IMPLIES (AND (NOT (ZEROP N)) (NOT (LISTP TM)))
(p ST SYM TM N))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT TM) decreases according to the well-founded relation LESSP in each
induction step of the scheme. Note, however, the inductive instances chosen
for N. The above induction scheme produces nine new formulas:
Case 9. (IMPLIES (AND (ZEROP N)
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, opening up the definitions of ZEROP, EQUAL, INSTRN, and
BTMP, to:
T.
Case 8. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(EQUAL SYM (CADAR TM))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, applying CNB-CONS and CNB-NBTM, and expanding the
definitions of ZEROP and INSTRN, to:
T.
Case 7. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(NOT (EQUAL SYM (CADAR TM)))
(BTMP (INSTRN ST SYM (CDR TM) (SUB1 N)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))).
This simplifies, unfolding the functions ZEROP and INSTRN, to:
T.
Case 6. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(NOT (EQUAL SYM (CADAR TM)))
(NOT (CNB (CDR TM)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))).
This simplifies, applying CNB-CONS, and expanding ZEROP, to:
T.
Case 5. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(EQUAL ST (CAAR TM))
(NOT (EQUAL SYM (CADAR TM)))
(CNB (INSTRN ST SYM (CDR TM) (SUB1 N)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, rewriting with the lemma CNB-NBTM, and opening up ZEROP
and INSTRN, to:
T.
Case 4. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(NOT (EQUAL ST (CAAR TM)))
(BTMP (INSTRN ST SYM (CDR TM) (SUB1 N)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, expanding ZEROP and INSTRN, to:
T.
Case 3. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(NOT (EQUAL ST (CAAR TM)))
(NOT (CNB (CDR TM)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, applying CNB-CONS, and expanding the function ZEROP, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP N))
(LISTP TM)
(NOT (EQUAL ST (CAAR TM)))
(CNB (INSTRN ST SYM (CDR TM) (SUB1 N)))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))).
This simplifies, applying CNB-NBTM, and expanding the definitions of ZEROP
and INSTRN, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP N))
(NOT (LISTP TM))
(NOT (BTMP (INSTRN ST SYM TM N)))
(CNB TM))
(CNB (INSTRN ST SYM TM N))),
which simplifies, opening up the functions ZEROP, INSTRN, BTMP, and CNB, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-INSTRN
(PROVE-LEMMA CNB-NEW-TAPE
(REWRITE)
(IMPLIES (AND (CNB OP) (CNB TAPE))
(CNB (NEW-TAPE OP TAPE))))
This simplifies, unfolding the definition of NEW-TAPE, to the following three
new goals:
Case 3. (IMPLIES (AND (CNB OP)
(CNB TAPE)
(NOT (EQUAL OP 'L))
(EQUAL OP 'R))
(CNB (CONS (CONS (CADR TAPE) (CAR TAPE))
(CDDR TAPE)))).
This again simplifies, applying the lemma CNB-CONS, and opening up the
definitions of CNB and EQUAL, to:
T.
Case 2. (IMPLIES (AND (CNB OP)
(CNB TAPE)
(NOT (EQUAL OP 'L))
(NOT (EQUAL OP 'R)))
(CNB (CONS (CAR TAPE)
(CONS OP (CDDR TAPE))))),
which again simplifies, applying CNB-CONS, to:
T.
Case 1. (IMPLIES (AND (CNB OP)
(CNB TAPE)
(EQUAL OP 'L))
(CNB (CONS (CDAR TAPE)
(CONS (CAAR TAPE) (CDR TAPE))))).
However this again simplifies, applying the lemma CNB-CONS, and opening up
the function CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CNB-NEW-TAPE
(TOGGLE NEW-TAPE-OFF NEW-TAPE T)
[ 0.0 0.0 0.0 ]
NEW-TAPE-OFF
(DEFN TMIN
(ST TAPE TM N)
(IF (ZEROP N)
(BTM)
(IF (BTMP (INSTRN ST
(CAR (CDR TAPE))
TM
(SUB1 N)))
(BTM)
(IF (INSTRN ST
(CAR (CDR TAPE))
TM
(SUB1 N))
(TMIN (CAR (CDR (INSTRN ST
(CAR (CDR TAPE))
TM
(SUB1 N))))
(NEW-TAPE (CAR (INSTRN ST
(CAR (CDR TAPE))
TM
(SUB1 N)))
TAPE)
TM
(SUB1 N))
TAPE))))
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
can be used to establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each recursive call. Hence, TMIN is accepted
under the principle of definition. From the definition we can conclude that:
(OR (OR (LISTP (TMIN ST TAPE TM N))
(BTMP (TMIN ST TAPE TM N)))
(EQUAL (TMIN ST TAPE TM N) TAPE))
is a theorem.
[ 0.0 0.0 0.0 ]
TMIN
(DEFN PR-EVAL-TMI-INDUCTION-SCHEME
(ST TAPE TM-- VA TM N)
(IF
(ZEROP N)
T
(PR-EVAL-TMI-INDUCTION-SCHEME '(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
'TM
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
TM
(SUB1 N))))
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 recursive call. Hence, PR-EVAL-TMI-INDUCTION-SCHEME is
accepted under the definitional principle. Observe that:
(TRUEP (PR-EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N))
is a theorem.
[ 0.0 0.0 0.0 ]
PR-EVAL-TMI-INDUCTION-SCHEME
(PROVE-LEMMA PR-EVAL-TMI
(REWRITE)
(IMPLIES (AND (CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'TMI ST TAPE TM--)
VA
(TMI-FA TM)
N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N)))
((INDUCT (PR-EVAL-TMI-INDUCTION-SCHEME ST TAPE TM-- VA TM N))))
This conjecture can be simplified, using the abbreviations ZEROP, IMPLIES, NOT,
OR, and AND, to two new formulas:
Case 2. (IMPLIES (AND (ZEROP N)
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'TMI ST TAPE TM--)
VA
(TMI-FA TM)
N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which simplifies, rewriting with EVLIST-CONS, CNB-NBTM, EVLIST-NIL, and
PR-EVAL-FN-0, and opening up the definitions of ZEROP, BTMP, UNSOLV-SUBRP,
EQUAL, and TMIN, to:
T.
Case 1. (IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(IMPLIES
(AND (CNB (EV 'AL
'(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))
(CNB (EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))
(CNB (EV 'AL
'TM
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL
'(CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL
'TM
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(SUB1 N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N)))
(EQUAL (EV 'AL
(LIST 'TMI ST TAPE TM--)
VA
(TMI-FA TM)
N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This simplifies, applying PR-EVAL-UNSOLV-SUBRP, EVLIST-NIL, CNB-NBTM,
EVLIST-CONS, CNB-CONS, PR-EVAL-NLISTP, CAR-CONS, CDR-CONS, PR-EVAL-INSTR,
GET-TMI-FA, PR-EVAL-IF, and PR-EVAL-FN-1, and expanding UNSOLV-APPLY-SUBR,
BTMP, GET, EQUAL, PACK, UNSOLV-SUBRP, AND, IMPLIES, TMI-DEFN, CDR, CAR,
LISTP, PAIRLIST, and TMIN, to 13 new conjectures:
Case 1.13.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(NOT (CNB (BTM)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, rewriting with CAR-CONS, CNB-CONS, CNB-INSTRN, and
CNB-NBTM, to:
T.
Case 1.12.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(NOT (CNB (BTM)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
However this again simplifies, opening up CONS, CAR, CDR, and BTMP, to:
T.
Case 1.11.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(NOT (CNB (BTM)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (BTM)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, rewriting with CAR-CONS and CDR-NLISTP, and
opening up the function BTMP, to:
T.
Case 1.10.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(NOT
(CNB
(CAAR
(LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This again simplifies, unfolding the definitions of BTMP, CONS, CAR, CDR,
and CNB, to:
T.
Case 1.9.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(NOT
(CNB
(CAAR
(LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, applying CAR-CONS, CNB-CONS, CNB-INSTRN, and
CNB-NBTM, to:
T.
Case 1.8.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (CNB (EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This again simplifies, rewriting with CNB-INSTRN, PR-EVAL-INSTR, CDR-CONS,
CAR-CONS, PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
PR-EVAL-UNSOLV-SUBRP, PR-EVAL-NEW-TAPE, GET-TMI-FA, PR-EVAL-IF, and
PR-EVAL-FN-1, and opening up the functions UNSOLV-SUBRP, PACK, EQUAL, GET,
BTMP, UNSOLV-APPLY-SUBR, TMI-DEFN, CDR, CAR, LISTP, PAIRLIST, and INSTRN,
to the following three new goals:
Case 1.8.3.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(NOT
(CNB
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(NOT
(BTMP
(EV 'AL
'(INSTR ST (CAR (CDR TAPE)) TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE
(CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))))
(EV 'AL
'(INSTR ST (CAR (CDR TAPE)) TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N))))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
But this again simplifies, applying the lemmas CNB-CONS, CNB-INSTRN, and
CNB-NEW-TAPE, to:
T.
Case 1.8.2.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(NOT
(CNB
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(NOT
(BTMP
(EV 'AL
'(INSTR ST (CAR (CDR TAPE)) TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE
(CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))))
(NOT
(EV 'AL
'(INSTR ST (CAR (CDR TAPE)) TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))))
(EQUAL
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, applying CNB-CONS, CNB-INSTRN, and CNB-NEW-TAPE,
to:
T.
Case 1.8.1.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (EQUAL (SUB1 N) 0))
(NOT
(CNB
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(BTMP
(EV 'AL
'(INSTR ST (CAR (CDR TAPE)) TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))))
(EQUAL (BTM)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
But this again simplifies, applying CNB-CONS, CNB-INSTRN, and
CNB-NEW-TAPE, to:
T.
Case 1.7.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (CNB (EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
But this again simplifies, applying the lemmas PR-EVAL-INSTR, CDR-CONS,
CAR-CONS, PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
PR-EVAL-UNSOLV-SUBRP, and PR-EVAL-NEW-TAPE, and unfolding the functions
CNB, UNSOLV-SUBRP, PACK, EQUAL, GET, BTMP, UNSOLV-APPLY-SUBR, CONS, TMIN,
and INSTRN, to:
T.
Case 1.6.
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(NOT (CNB (EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (BTM)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, unfolding TMIN and EQUAL, to:
T.
Case 1.5.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (BTM)
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, applying the lemmas CAR-CONS, CNB-CONS, CNB-INSTRN,
and CNB-NBTM, to:
T.
Case 1.4.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (BTM)
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, opening up the functions CONS, CAR, CDR, and BTMP,
to:
T.
Case 1.3.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (BTM)
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (BTM)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))),
which again simplifies, rewriting with CAR-CONS and CDR-NLISTP, and
opening up BTMP, to:
T.
Case 1.2.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN
(CAAR
(LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(NOT (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(EQUAL (EV 'AL TAPE VA (TMI-FA TM) N)
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
However this again simplifies, applying PR-EVAL-INSTR, CDR-CONS, CAR-CONS,
PR-EVAL-NLISTP, CNB-CONS, EVLIST-CONS, CNB-NBTM, EVLIST-NIL,
PR-EVAL-UNSOLV-SUBRP, and PR-EVAL-NEW-TAPE, and expanding the functions
BTMP, CONS, CAR, CDR, CNB, UNSOLV-SUBRP, PACK, EQUAL, GET,
UNSOLV-APPLY-SUBR, TMIN, and INSTRN, to:
T.
Case 1.1.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT
(BTMP (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN
(CAAR
(LIST (CDAR (LIST (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))))
(EV 'AL
'(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EQUAL (EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN (EV 'AL ST VA (TMI-FA TM) N)
(EV 'AL TAPE VA (TMI-FA TM) N)
(EV 'AL TM-- VA (TMI-FA TM) N)
N))).
This again simplifies, rewriting with the lemmas CAR-CONS, CNB-CONS,
CNB-INSTRN, CNB-NBTM, PR-EVAL-INSTR, CDR-CONS, PR-EVAL-NLISTP, EVLIST-CONS,
EVLIST-NIL, PR-EVAL-UNSOLV-SUBRP, PR-EVAL-NEW-TAPE, GET-TMI-FA,
CNB-NEW-TAPE, PR-EVAL-IF, PR-EVAL-FN-1, and PR-EVAL-FN-0, and opening up
UNSOLV-SUBRP, PACK, EQUAL, GET, BTMP, UNSOLV-APPLY-SUBR, TMI-DEFN, CDR,
CAR, LISTP, PAIRLIST, TMIN, INSTRN, and ZEROP, to three new conjectures:
Case 1.1.3.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (EQUAL (SUB1 N) 0))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(NOT
(BTMP
(INSTRN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CADR
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 (SUB1 N)))))
(INSTRN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CADR
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 (SUB1 N))))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST
(CONS 'ST
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(CONS 'TAPE
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 (SUB1 N)))
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))),
which again simplifies, rewriting with the lemmas CNB-INSTRN,
PR-EVAL-UNSOLV-SUBRP, EVLIST-NIL, CNB-NBTM, EVLIST-CONS, CNB-CONS,
PR-EVAL-NLISTP, CAR-CONS, CDR-CONS, PR-EVAL-INSTR, PR-EVAL-NEW-TAPE,
GET-TMI-FA, CNB-NEW-TAPE, PR-EVAL-IF, and PR-EVAL-FN-1, and opening up
the functions UNSOLV-APPLY-SUBR, BTMP, GET, PACK, UNSOLV-SUBRP, EQUAL,
TMI-DEFN, CDR, CAR, LISTP, and PAIRLIST, to:
T.
Case 1.1.2.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (EQUAL (SUB1 N) 0))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(NOT
(BTMP
(INSTRN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CADR
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 (SUB1 N)))))
(NOT
(INSTRN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CADR
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 (SUB1 N)))))
(EQUAL
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))),
which again simplifies, rewriting with CNB-INSTRN, PR-EVAL-UNSOLV-SUBRP,
EVLIST-NIL, CNB-NBTM, EVLIST-CONS, CNB-CONS, PR-EVAL-NLISTP, CAR-CONS,
CDR-CONS, PR-EVAL-INSTR, PR-EVAL-NEW-TAPE, GET-TMI-FA, CNB-NEW-TAPE,
PR-EVAL-IF, and PR-EVAL-FN-1, and expanding UNSOLV-APPLY-SUBR, BTMP, GET,
PACK, UNSOLV-SUBRP, EQUAL, TMI-DEFN, CDR, CAR, LISTP, PAIRLIST, and TMIN,
to:
T.
Case 1.1.1.
(IMPLIES
(AND
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))))
(NOT (EQUAL (SUB1 N) 0))
(EQUAL
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N))
(TMIN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CNB (EV 'AL ST VA (TMI-FA TM) N))
(CNB (EV 'AL TAPE VA (TMI-FA TM) N))
(CNB (EV 'AL TM-- VA (TMI-FA TM) N))
(INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N))
(BTMP
(INSTRN
(CADR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(CADR
(NEW-TAPE (CAR (INSTRN (EV 'AL ST VA (TMI-FA TM) N)
(CADR (EV 'AL TAPE VA (TMI-FA TM) N))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 N)))
(EV 'AL TAPE VA (TMI-FA TM) N)))
(EV 'AL TM-- VA (TMI-FA TM) N)
(SUB1 (SUB1 N)))))
(EQUAL (BTM)
(EV 'AL
'(TMI (CAR (CDR (INSTR ST (CAR (CDR TAPE)) TM)))
(NEW-TAPE (CAR (INSTR ST (CAR (CDR TAPE)) TM))
TAPE)
TM)
(LIST (CONS 'ST
(EV 'AL ST VA (TMI-FA TM) N))
(CONS 'TAPE
(EV 'AL TAPE VA (TMI-FA TM) N))
(CONS 'TM
(EV 'AL TM-- VA (TMI-FA TM) N)))
(TMI-FA TM)
(SUB1 N)))).
But this again simplifies, rewriting with CNB-INSTRN,
PR-EVAL-UNSOLV-SUBRP, EVLIST-NIL, CNB-NBTM, EVLIST-CONS, CNB-CONS,
PR-EVAL-NLISTP, CAR-CONS, CDR-CONS, PR-EVAL-INSTR, PR-EVAL-NEW-TAPE,
GET-TMI-FA, CNB-NEW-TAPE, PR-EVAL-IF, and PR-EVAL-FN-1, and opening up
the definitions of UNSOLV-APPLY-SUBR, BTMP, GET, PACK, UNSOLV-SUBRP,
EQUAL, TMI-DEFN, CDR, CAR, LISTP, PAIRLIST, and TMIN, to:
T.
Q.E.D.
[ 0.0 1.3 0.1 ]
PR-EVAL-TMI
(PROVE-LEMMA PR-EVAL-TMI-X
(REWRITE)
(IMPLIES (AND (CNB ST) (CNB TAPE) (CNB TM))
(EQUAL (EV 'AL
(TMI-X ST TAPE)
NIL
(TMI-FA TM)
N)
(IF (ZEROP N)
(BTM)
(TMIN ST TAPE TM N)))))
This conjecture can be simplified, using the abbreviations AND, IMPLIES, KWOTE,
and TMI-X, to:
(IMPLIES (AND (CNB ST) (CNB TAPE) (CNB TM))
(EQUAL (EV 'AL
(CONS 'TMI
(CONS (LIST 'QUOTE ST)
(CONS (LIST 'QUOTE TAPE) '((TM)))))
NIL
(TMI-FA TM)
N)
(IF (ZEROP N)
(BTM)
(TMIN ST TAPE TM N)))).
This simplifies, unfolding ZEROP, to the following three new goals:
Case 3. (IMPLIES (AND (CNB ST)
(CNB TAPE)
(CNB TM)
(NOT (NUMBERP N)))
(EQUAL (EV 'AL
(CONS 'TMI
(CONS (LIST 'QUOTE ST)
(CONS (LIST 'QUOTE TAPE) '((TM)))))
NIL
(TMI-FA TM)
N)
(BTM))).
This again simplifies, applying PR-EVAL-QUOTE, EVLIST-CONS, EVLIST-NIL,
PR-EVAL-FN-0, and CNB-NBTM, and expanding the functions BTMP, UNSOLV-SUBRP,
EQUAL, and ZEROP, to:
T.
Case 2. (IMPLIES (AND (CNB ST)
(CNB TAPE)
(CNB TM)
(EQUAL N 0))
(EQUAL (EV 'AL
(CONS 'TMI
(CONS (LIST 'QUOTE ST)
(CONS (LIST 'QUOTE TAPE) '((TM)))))
NIL
(TMI-FA TM)
N)
(BTM))).
But this again simplifies, rewriting with PR-EVAL-QUOTE, EVLIST-CONS,
EVLIST-NIL, PR-EVAL-FN-0, and CNB-NBTM, and unfolding BTMP, UNSOLV-SUBRP,
EQUAL, and ZEROP, to:
T.
Case 1. (IMPLIES (AND (CNB ST)
(CNB TAPE)
(CNB TM)
(NOT (EQUAL N 0))
(NUMBERP N))
(EQUAL (EV 'AL
(CONS 'TMI
(CONS (LIST 'QUOTE ST)
(CONS (LIST 'QUOTE TAPE) '((TM)))))
NIL
(TMI-FA TM)
N)
(TMIN ST TAPE TM N))).
However this again simplifies, rewriting with PR-EVAL-FN-1, CAR-CONS,
CDR-CONS, GET-TMI-FA, EVLIST-NIL, PR-EVAL-QUOTE, and PR-EVAL-TMI, and
expanding the definitions of PAIRLIST, KWOTE, BTMP, EQUAL, and UNSOLV-SUBRP,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
PR-EVAL-TMI-X
(TOGGLE TMI-X-OFF TMI-X T)
[ 0.0 0.0 0.0 ]
TMI-X-OFF
(PROVE-LEMMA INSTRN-INSTR
(REWRITE)
(IMPLIES (LESSP (LENGTH TM) N)
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest five inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N)))
(p ST SYM TM N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(p ST SYM TM N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(p ST SYM (CDR TM) (SUB1 N)))
(p ST SYM TM N))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT can be used to show that the measure (COUNT N) decreases
according to the well-founded relation LESSP in each induction step of the
scheme. Note, however, the inductive instance chosen for TM. The above
induction scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(LESSP (LENGTH TM) N))
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))).
This simplifies, opening up the functions NOT, OR, LENGTH, EQUAL, and LESSP,
to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM))))
(LESSP (LENGTH TM) N))
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))).
This simplifies, unfolding the functions NOT, OR, LENGTH, EQUAL, LESSP,
INSTRN, and INSTR, to the following two new conjectures:
Case 3.2.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (ADD1 (LENGTH (CDR TM))) 0)
(LISTP TM)
(NOT (EQUAL SYM (CADAR TM))))
(EQUAL (INSTRN ST SYM (CDR TM) (SUB1 N))
(INSTR ST SYM (CDR TM)))).
However this again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL (ADD1 (LENGTH (CDR TM))) 0)
(LISTP TM)
(NOT (EQUAL ST (CAAR TM))))
(EQUAL (INSTRN ST SYM (CDR TM) (SUB1 N))
(INSTR ST SYM (CDR TM)))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(LESSP (LENGTH TM) N))
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))),
which simplifies, appealing to the lemma SUB1-ADD1, and opening up NOT, OR,
LENGTH, and LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(EQUAL (INSTRN ST SYM (CDR TM) (SUB1 N))
(INSTR ST SYM (CDR TM)))
(LESSP (LENGTH TM) N))
(EQUAL (INSTRN ST SYM TM N)
(INSTR ST SYM TM))),
which simplifies, rewriting with SUB1-ADD1, and opening up the definitions
of NOT, OR, LENGTH, LESSP, INSTRN, and INSTR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
INSTRN-INSTR
(PROVE-LEMMA NBTMP-INSTR
(REWRITE)
(IMPLIES (TURING-MACHINE TM)
(NOT (BTMP (INSTR ST SYM TM)))))
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 (NLISTP TM) (p ST SYM TM))
(IMPLIES (AND (NOT (NLISTP TM))
(p ST SYM (CDR TM)))
(p ST SYM TM))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT TM) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following three new formulas:
Case 3. (IMPLIES (AND (NLISTP TM) (TURING-MACHINE TM))
(NOT (BTMP (INSTR ST SYM TM)))).
This simplifies, expanding the definitions of NLISTP, TURING-MACHINE, LISTP,
INSTR, and BTMP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP TM))
(NOT (TURING-MACHINE (CDR TM)))
(TURING-MACHINE TM))
(NOT (BTMP (INSTR ST SYM TM)))).
This simplifies, expanding the definitions of NLISTP, TURING-MACHINE,
OPERATION, SYMBOL, CDR, CAR, LISTP, MEMBER, STATE, and TURING-4TUPLE, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP TM))
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(TURING-MACHINE TM))
(NOT (BTMP (INSTR ST SYM TM)))).
This simplifies, opening up the functions NLISTP, TURING-MACHINE, OPERATION,
SYMBOL, CDR, CAR, LISTP, MEMBER, STATE, TURING-4TUPLE, and INSTR, to the
following eight new goals:
Case 1.8.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(NOT (BTMP (CDDAR TM)))).
But this again simplifies, rewriting with the lemma CAR-NLISTP, and
unfolding the function EQUAL, to:
T.
Case 1.7.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(NOT (BTMP (CDDAR TM)))),
which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
unfolding EQUAL, CAR, and LITATOM, to:
T.
Case 1.6.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(NOT (BTMP (CDDAR TM)))).
This again simplifies, applying CAR-NLISTP, and opening up the definition
of EQUAL, to:
T.
Case 1.5.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(NOT (BTMP (CDDAR TM)))).
However this again simplifies, applying CAR-NLISTP, and unfolding the
function EQUAL, to:
T.
Case 1.4.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(NOT (BTMP (CDDAR TM)))).
This again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
opening up the functions EQUAL, CAR, and LITATOM, to:
T.
Case 1.3.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(NOT (BTMP (CDDAR TM)))).
But this again simplifies, appealing to the lemma CAR-NLISTP, and opening
up the function EQUAL, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(NOT (BTMP (CDDAR TM)))),
which again simplifies, appealing to the lemma CAR-NLISTP, and expanding
EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP TM)
(NOT (BTMP (INSTR ST SYM (CDR TM))))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(NOT (BTMP (CDDAR TM)))),
which again simplifies, applying the lemma CAR-NLISTP, and unfolding the
definition of EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
NBTMP-INSTR
(PROVE-LEMMA INSTRN-NON-F
(REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(INSTRN ST SYM TM N)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest five inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP TM) (p ST SYM TM N))
(IMPLIES (AND (NOT (NLISTP TM))
(p ST SYM (CDR TM) (SUB1 N)))
(p ST SYM TM N))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to prove that the measure (COUNT TM) decreases according to
the well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instance chosen for N. The above induction scheme
leads to the following four new goals:
Case 4. (IMPLIES (AND (NLISTP TM)
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(INSTRN ST SYM TM N)).
This simplifies, opening up the definitions of NLISTP, TURING-MACHINE,
LENGTH, EQUAL, LESSP, and INSTRN, to the following two new goals:
Case 4.2.
(IMPLIES (AND (NOT (LISTP TM))
(EQUAL TM NIL)
(EQUAL N 0))
(BTM)).
This again simplifies, obviously, to:
T.
Case 4.1.
(IMPLIES (AND (NOT (LISTP TM))
(EQUAL TM NIL)
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP TM))
(NOT (TURING-MACHINE (CDR TM)))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(INSTRN ST SYM TM N)).
This simplifies, unfolding the definitions of NLISTP, TURING-MACHINE,
OPERATION, SYMBOL, CDR, CAR, LISTP, MEMBER, STATE, and TURING-4TUPLE, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP TM))
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(INSTRN ST SYM TM N)).
This simplifies, applying SUB1-ADD1, and opening up NLISTP, TURING-MACHINE,
OPERATION, SYMBOL, CDR, CAR, LISTP, MEMBER, STATE, TURING-4TUPLE, LENGTH,
LESSP, EQUAL, and INSTRN, to 16 new conjectures:
Case 2.16.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, obviously, to:
T.
Case 2.15.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, clearly, to:
T.
Case 2.14.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.13.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, clearly, to:
T.
Case 2.12.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, trivially, to:
T.
Case 2.11.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.10.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, clearly, to:
T.
Case 2.9.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.8.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.7.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, clearly, to:
T.
Case 2.6.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, trivially, to:
T.
Case 2.5.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.4.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, obviously, to:
T.
Case 2.3.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, clearly, to:
T.
Case 2.2.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, trivially, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP TM)
(LESSP (LENGTH (CDR TM)) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP TM))
(INSTRN ST SYM (CDR TM) (SUB1 N))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(INSTRN ST SYM TM N)).
This simplifies, appealing to the lemma SUB1-ADD1, and unfolding the
definitions of NLISTP, TURING-MACHINE, OPERATION, SYMBOL, CDR, CAR, LISTP,
MEMBER, STATE, TURING-4TUPLE, LENGTH, LESSP, EQUAL, and INSTRN, to the
following 24 new formulas:
Case 1.24.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)).
This again simplifies, clearly, to:
T.
Case 1.23.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, trivially, to:
T.
Case 1.22.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(CDDAR TM)).
This again simplifies, expanding CAR and EQUAL, to:
T.
Case 1.21.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, trivially, to:
T.
Case 1.20.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, trivially, to:
T.
Case 1.19.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(CDDAR TM)).
But this again simplifies, unfolding the functions CAR, EQUAL, CDR, and
LITATOM, to:
T.
Case 1.18.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, trivially, to:
T.
Case 1.17.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, trivially, to:
T.
Case 1.16.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(CDDAR TM)).
But this again simplifies, unfolding the functions CAR and EQUAL, to:
T.
Case 1.15.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, obviously, to:
T.
Case 1.14.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, trivially, to:
T.
Case 1.13.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'L)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(CDDAR TM)).
This again simplifies, opening up the functions CAR and EQUAL, to:
T.
Case 1.12.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, obviously, to:
T.
Case 1.11.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 1.10.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 0)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(CDDAR TM)).
This again simplifies, opening up the functions CAR, EQUAL, CDR, and
LITATOM, to:
T.
Case 1.9.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, trivially, to:
T.
Case 1.8.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, trivially, to:
T.
Case 1.7.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 'R)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(CDDAR TM)).
But this again simplifies, opening up CAR and EQUAL, to:
T.
Case 1.6.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, obviously, to:
T.
Case 1.5.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, obviously, to:
T.
Case 1.4.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 0)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 0))
(CDDAR TM)).
But this again simplifies, unfolding the functions CAR and EQUAL, to:
T.
Case 1.3.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(EQUAL N 0))
(BTM)),
which again simplifies, obviously, to:
T.
Case 1.2.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (NUMBERP N)))
(BTM)).
This again simplifies, clearly, to:
T.
Case 1.1.
(IMPLIES (AND (LISTP TM)
(INSTRN ST SYM (CDR TM) (SUB1 N))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(EQUAL (CADAR TM) 1)
(EQUAL (CADDAR TM) 1)
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM))
(NOT (LESSP (LENGTH (CDR TM)) (SUB1 N)))
(NOT (EQUAL N 0))
(NUMBERP N)
(EQUAL ST (CAAR TM))
(EQUAL SYM 1))
(CDDAR TM)).
This again simplifies, expanding the definitions of CAR and EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.1 ]
INSTRN-NON-F
(PROVE-LEMMA TMIN-BTM
(REWRITE)
(IMPLIES (AND (TURING-MACHINE TM)
(LEQ N (LENGTH TM)))
(EQUAL (TMIN ST TAPE TM N) (BTM))))
Name the conjecture *1.
We will appeal to induction. The recursive terms in the conjecture
suggest four inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (OR (EQUAL N 0) (NOT (NUMBERP N)))
(p ST TAPE TM N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(p ST TAPE TM N))
(IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(p (CADR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
(NEW-TAPE (CAR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
TAPE)
TM
(SUB1 N)))
(p ST TAPE TM N))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definitions
of OR and NOT establish that the measure (COUNT N) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for ST and TAPE. The above induction
scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (OR (EQUAL N 0) (NOT (NUMBERP N)))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(EQUAL (TMIN ST TAPE TM N) (BTM))).
This simplifies, unfolding the definitions of NOT, OR, EQUAL, LESSP, and
TMIN, to:
T.
Case 3. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM))))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(EQUAL (TMIN ST TAPE TM N) (BTM))).
This simplifies, rewriting with LENGTH-0, and expanding the definitions of
NOT, OR, TURING-MACHINE, LENGTH, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(LESSP (LENGTH TM) (SUB1 N))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(EQUAL (TMIN ST TAPE TM N) (BTM))),
which simplifies, using linear arithmetic, to:
(IMPLIES (AND (LESSP N 1)
(NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(LESSP (LENGTH TM) (SUB1 N))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(EQUAL (TMIN ST TAPE TM N) (BTM))).
However this again simplifies, expanding the definitions of SUB1, NUMBERP,
EQUAL, LESSP, NOT, and OR, to:
T.
Case 1. (IMPLIES
(AND (NOT (OR (EQUAL N 0) (NOT (NUMBERP N))))
(NOT (OR (EQUAL (LENGTH TM) 0)
(NOT (NUMBERP (LENGTH TM)))))
(EQUAL (TMIN (CADR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
(NEW-TAPE (CAR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
TAPE)
TM
(SUB1 N))
(BTM))
(TURING-MACHINE TM)
(NOT (LESSP (LENGTH TM) N)))
(EQUAL (TMIN ST TAPE TM N) (BTM))),
which simplifies, applying the lemma LENGTH-0, and expanding the functions
NOT, OR, LESSP, and TMIN, to:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(LISTP TM)
(EQUAL (TMIN (CADR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
(NEW-TAPE (CAR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
TAPE)
TM
(SUB1 N))
(BTM))
(TURING-MACHINE TM)
(NOT (LESSP (SUB1 (LENGTH TM)) (SUB1 N)))
(NOT (BTMP (INSTRN ST (CADR TAPE) TM (SUB1 N))))
(NOT (INSTRN ST (CADR TAPE) TM (SUB1 N))))
(EQUAL TAPE (BTM))).
However this again simplifies, expanding BTMP, to the conjecture:
(IMPLIES
(AND (NOT (EQUAL N 0))
(NUMBERP N)
(LISTP TM)
(EQUAL (TMIN (CADR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
(NEW-TAPE (CAR (INSTRN ST (CADR TAPE) TM (SUB1 N)))
TAPE)
TM
(SUB1 N))
(BTM))
(TURING-MACHINE TM)
(NOT (LESSP (SUB1 (LENGTH TM)) (SUB1 N)))
(NOT (INSTRN ST (CADR TAPE) TM (SUB1 N))))
(EQUAL TAPE (BTM))).
This further simplifies, using linear arithmetic, applying INSTRN-NON-F, and
opening up CDR, CAR, SUB1, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
TMIN-BTM
(PROVE-LEMMA TMIN-TMI
(REWRITE)
(IMPLIES (TURING-MACHINE TM)
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM
(PLUS K (ADD1 (LENGTH TM)))))))
Give the conjecture the name *1.
We will appeal to induction. Four inductions are suggested by terms in
the conjecture. They merge into two likely candidate inductions. However,
only one is unflawed. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP K) (p ST TAPE TM K))
(IMPLIES (AND (NOT (ZEROP K))
(INSTR ST (CADR TAPE) TM)
(p (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K)))
(p ST TAPE TM K))
(IMPLIES (AND (NOT (ZEROP K))
(NOT (INSTR ST (CADR TAPE) TM)))
(p ST TAPE TM K))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to establish that the measure (COUNT K) decreases according to the
well-founded relation LESSP in each induction step of the scheme. Note,
however, the inductive instances chosen for ST and TAPE. The above induction
scheme leads to three new goals:
Case 3. (IMPLIES (AND (ZEROP K) (TURING-MACHINE TM))
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM
(PLUS K (ADD1 (LENGTH TM)))))),
which simplifies, using linear arithmetic, rewriting with TMIN-BTM,
INSTRN-NON-F, and SUB1-ADD1, and opening up the definitions of ZEROP, EQUAL,
TMI, PLUS, and TMIN, to:
T.
Case 2. (IMPLIES (AND (NOT (ZEROP K))
(INSTR ST (CADR TAPE) TM)
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(TMIN (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(TURING-MACHINE TM))
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM
(PLUS K (ADD1 (LENGTH TM)))))).
This simplifies, rewriting with SUB1-ADD1, and opening up ZEROP, TMI, PLUS,
and TMIN, to three new formulas:
Case 2.3.
(IMPLIES
(AND (NOT (EQUAL K 0))
(NUMBERP K)
(INSTR ST (CADR TAPE) TM)
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(TMIN (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(TURING-MACHINE TM)
(NOT (BTMP (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(EQUAL
(TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(TMIN (CADR (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(NEW-TAPE (CAR (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))),
which again simplifies, using linear arithmetic and applying INSTRN-INSTR
and NBTMP-INSTR, to:
T.
Case 2.2.
(IMPLIES
(AND (NOT (EQUAL K 0))
(NUMBERP K)
(INSTR ST (CADR TAPE) TM)
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(TMIN (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(TURING-MACHINE TM)
(NOT (BTMP (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(NOT (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
TAPE)).
However this again simplifies, using linear arithmetic and rewriting with
INSTRN-INSTR and NBTMP-INSTR, to:
T.
Case 2.1.
(IMPLIES (AND (NOT (EQUAL K 0))
(NUMBERP K)
(INSTR ST (CADR TAPE) TM)
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(TMIN (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(TURING-MACHINE TM)
(BTMP (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(EQUAL (TMI (CADR (INSTR ST (CADR TAPE) TM))
(NEW-TAPE (CAR (INSTR ST (CADR TAPE) TM))
TAPE)
TM
(SUB1 K))
(BTM))).
But this again simplifies, using linear arithmetic and applying
INSTRN-INSTR and NBTMP-INSTR, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP K))
(NOT (INSTR ST (CADR TAPE) TM))
(TURING-MACHINE TM))
(EQUAL (TMI ST TAPE TM K)
(TMIN ST TAPE TM
(PLUS K (ADD1 (LENGTH TM)))))).
This simplifies, rewriting with the lemma SUB1-ADD1, and opening up the
functions ZEROP, TMI, PLUS, and TMIN, to the following two new formulas:
Case 1.2.
(IMPLIES
(AND (NOT (EQUAL K 0))
(NUMBERP K)
(NOT (INSTR ST (CADR TAPE) TM))
(TURING-MACHINE TM)
(NOT (BTMP (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(EQUAL TAPE
(TMIN (CADR (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
(NEW-TAPE (CAR (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))
TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM)))))).
But this again simplifies, using linear arithmetic, applying INSTRN-INSTR,
and expanding the function BTMP, to:
T.
Case 1.1.
(IMPLIES (AND (NOT (EQUAL K 0))
(NUMBERP K)
(NOT (INSTR ST (CADR TAPE) TM))
(TURING-MACHINE TM)
(BTMP (INSTRN ST
(CADR TAPE)
TM
(PLUS (SUB1 K) (ADD1 (LENGTH TM))))))
(EQUAL TAPE (BTM))).
However this again simplifies, using linear arithmetic, rewriting with
INSTRN-INSTR, and opening up the definition of BTMP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.3 0.0 ]
TMIN-TMI
(PROVE-LEMMA SYMBOL-CNB
(REWRITE)
(IMPLIES (SYMBOL SYM) (CNB SYM)))
This formula can be simplified, using the abbreviations IMPLIES and SYMBOL, to:
(IMPLIES (MEMBER SYM '(0 1))
(CNB SYM)),
which simplifies, opening up the definitions of CDR, CAR, LISTP, MEMBER, and
CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SYMBOL-CNB
(TOGGLE SYMBOL-OFF SYMBOL T)
[ 0.0 0.0 0.0 ]
SYMBOL-OFF
(PROVE-LEMMA HALF-TAPE-CNB
(REWRITE)
(IMPLIES (HALF-TAPE X) (CNB X)))
Call the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP X) (p X))
(IMPLIES (AND (NOT (NLISTP X)) (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 produces the following three new goals:
Case 3. (IMPLIES (AND (NLISTP X) (HALF-TAPE X))
(CNB X)).
This simplifies, expanding the definitions of NLISTP, HALF-TAPE, and CNB, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X))
(NOT (HALF-TAPE (CDR X)))
(HALF-TAPE X))
(CNB X)).
This simplifies, expanding NLISTP and HALF-TAPE, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X))
(CNB (CDR X))
(HALF-TAPE X))
(CNB X)).
This simplifies, unfolding the functions NLISTP and HALF-TAPE, to the new
formula:
(IMPLIES (AND (LISTP X)
(CNB (CDR X))
(SYMBOL (CAR X))
(HALF-TAPE (CDR X)))
(CNB X)).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS V Z) to eliminate
(CDR X) and (CAR X). We would thus like to prove:
(IMPLIES (AND (CNB Z) (SYMBOL V) (HALF-TAPE Z))
(CNB (CONS V Z))),
which further simplifies, appealing to the lemmas SYMBOL-CNB and CNB-CONS,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
HALF-TAPE-CNB
(PROVE-LEMMA TAPE-CNB
(REWRITE)
(IMPLIES (TAPE X) (CNB X)))
This formula can be simplified, using the abbreviations TAPE and IMPLIES, to:
(IMPLIES (AND (LISTP X)
(HALF-TAPE (CAR X))
(HALF-TAPE (CDR X)))
(CNB X)).
Applying the lemma CAR-CDR-ELIM, replace X by (CONS Z V) to eliminate (CAR X)
and (CDR X). We thus obtain:
(IMPLIES (AND (HALF-TAPE Z) (HALF-TAPE V))
(CNB (CONS Z V))),
which simplifies, applying the lemmas HALF-TAPE-CNB and CNB-CONS, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TAPE-CNB
(TOGGLE TAPE-OFF TAPE T)
[ 0.0 0.0 0.0 ]
TAPE-OFF
(PROVE-LEMMA OPERATION-CNB
(REWRITE)
(IMPLIES (OPERATION OP) (CNB OP)))
This formula can be simplified, using the abbreviations IMPLIES and OPERATION,
to:
(IMPLIES (MEMBER OP '(L R 0 1))
(CNB OP)),
which simplifies, opening up the definitions of CDR, CAR, LISTP, MEMBER, and
CNB, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OPERATION-CNB
(TOGGLE OPERATION-OFF OPERATION T)
[ 0.0 0.0 0.0 ]
OPERATION-OFF
(PROVE-LEMMA TURING-MACHINE-CNB
(REWRITE)
(IMPLIES (TURING-MACHINE TM)
(CNB TM)))
Call the conjecture *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP TM) (p TM))
(IMPLIES (AND (NOT (NLISTP TM)) (p (CDR TM)))
(p TM))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT TM) 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 (AND (NLISTP TM) (TURING-MACHINE TM))
(CNB TM)).
This simplifies, expanding the definitions of NLISTP, TURING-MACHINE, and
CNB, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP TM))
(NOT (TURING-MACHINE (CDR TM)))
(TURING-MACHINE TM))
(CNB TM)).
This simplifies, expanding NLISTP, TURING-MACHINE, STATE, and TURING-4TUPLE,
to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP TM))
(CNB (CDR TM))
(TURING-MACHINE TM))
(CNB TM)).
This simplifies, unfolding the functions NLISTP, TURING-MACHINE, STATE, and
TURING-4TUPLE, to the new formula:
(IMPLIES (AND (LISTP TM)
(CNB (CDR TM))
(LISTP (CAR TM))
(LITATOM (CAAR TM))
(SYMBOL (CADAR TM))
(OPERATION (CADDAR TM))
(LITATOM (CADDDAR TM))
(EQUAL (CDDDDAR TM) NIL)
(TURING-MACHINE (CDR TM)))
(CNB TM)).
Applying the lemma CAR-CDR-ELIM, replace TM by (CONS Z X) to eliminate
(CDR TM) and (CAR TM), Z by (CONS V W) to eliminate (CAR Z) and (CDR Z), W
by (CONS Z D) to eliminate (CAR W) and (CDR W), D by (CONS W C) to eliminate
(CAR D) and (CDR D), and C by (CONS D X1) to eliminate (CAR C) and (CDR C).
We would thus like to prove the following four new formulas:
Case 1.4.
(IMPLIES (AND (NOT (LISTP W))
(CNB X)
(LITATOM V)
(SYMBOL (CAR W))
(OPERATION (CADR W))
(LITATOM (CADDR W))
(EQUAL (CDDDR W) NIL)
(TURING-MACHINE X))
(CNB (CONS (CONS V W) X))).
But this further simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
expanding the definitions of SYMBOL, CAR, OPERATION, CDR, and LITATOM, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (LISTP D))
(CNB X)
(LITATOM V)
(SYMBOL Z)
(OPERATION (CAR D))
(LITATOM (CADR D))
(EQUAL (CDDR D) NIL)
(TURING-MACHINE X))
(CNB (CONS (CONS V (CONS Z D)) X))).
However this further simplifies, appealing to the lemmas CAR-NLISTP and
CDR-NLISTP, and unfolding the definitions of OPERATION, CAR, and LITATOM,
to:
T.
Case 1.2.
(IMPLIES (AND (NOT (LISTP C))
(CNB X)
(LITATOM V)
(SYMBOL Z)
(OPERATION W)
(LITATOM (CAR C))
(EQUAL (CDR C) NIL)
(TURING-MACHINE X))
(CNB (CONS (CONS V (CONS Z (CONS W C)))
X))),
which further simplifies, applying CAR-NLISTP, and expanding LITATOM, to:
T.
Case 1.1.
(IMPLIES (AND (CNB X)
(LITATOM V)
(SYMBOL Z)
(OPERATION W)
(LITATOM D)
(EQUAL X1 NIL)
(TURING-MACHINE X))
(CNB (CONS (CONS V (CONS Z (CONS W (CONS D X1))))
X))).
However this further simplifies, applying CNB-LITATOM, SYMBOL-CNB,
OPERATION-CNB, and CNB-CONS, and opening up the definition of CNB, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
TURING-MACHINE-CNB
(TOGGLE TURING-MACHINE-OFF TURING-MACHINE T)
[ 0.0 0.0 0.0 ]
TURING-MACHINE-OFF
(PROVE-LEMMA TURING-COMPLETENESS-OF-LISP NIL
(IMPLIES (AND (STATE ST)
(TAPE TAPE)
(TURING-MACHINE TM))
(AND (IMPLIES (NOT (BTMP (PR-EVAL (TMI-X ST TAPE)
NIL
(TMI-FA TM)
N)))
(NOT (BTMP (TMI ST TAPE TM
(TMI-K ST TAPE TM N)))))
(IMPLIES (NOT (BTMP (TMI ST TAPE TM K)))
(EQUAL (TMI ST TAPE TM K)
(PR-EVAL (TMI-X ST TAPE)
NIL
(TMI-FA TM)
(TMI-N ST TAPE TM K))))))
NIL)
This conjecture can be simplified, using the abbreviations AND, IMPLIES, TMI-N,
TMI-K, PR-EVAL, and STATE, to the formula:
(IMPLIES
(AND (LITATOM ST)
(TAPE TAPE)
(TURING-MACHINE TM))
(AND (IMPLIES (NOT (BTMP (EV 'AL
(TMI-X ST TAPE)
NIL
(TMI-FA TM)
N)))
(NOT (BTMP (TMI ST TAPE TM
(DIFFERENCE N (ADD1 (LENGTH TM)))))))
(IMPLIES (NOT (BTMP (TMI ST TAPE TM K)))
(EQUAL (TMI ST TAPE TM K)
(EV 'AL
(TMI-X ST TAPE)
NIL
(TMI-FA TM)
(PLUS K (ADD1 (LENGTH TM)))))))).
This simplifies, applying TURING-MACHINE-CNB, TAPE-CNB, CNB-LITATOM,
PR-EVAL-TMI-X, SUB1-ADD1, PLUS-DIFFERENCE, TMIN-TMI, and PLUS-EQUAL-0, and
unfolding the definitions of NOT, LESSP, IMPLIES, and AND, to:
(IMPLIES (AND (LITATOM ST)
(TAPE TAPE)
(TURING-MACHINE TM)
(NOT (EQUAL N 0))
(NUMBERP N)
(NOT (BTMP (TMIN ST TAPE TM N)))
(NOT (LESSP (LENGTH TM) (SUB1 N))))
(NOT (BTMP (TMIN ST TAPE TM
(ADD1 (LENGTH TM)))))).
But this again simplifies, applying the lemmas TMIN-BTM and INSTRN-NON-F, and
unfolding TMIN and BTMP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
TURING-COMPLETENESS-OF-LISP