#|

 Copyright (C) 1994 by Robert S. Boyer and J Strother Moore.  All Rights
 Reserved.

 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.

 NO WARRANTY

 Robert S. Boyer and J Strother Moore PROVIDE ABSOLUTELY NO WARRANTY.  THE
 EVENT SCRIPT IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS
 OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF
 MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO
 THE QUALITY AND PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT
 PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR
 CORRECTION.

 IN NO EVENT WILL Robert S. Boyer or J Strother Moore BE LIABLE TO YOU FOR ANY
 DAMAGES, ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR
 CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT
 (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE
 OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE
 POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.

|#

(NOTE-LIB "unsolv" T)
(COMPILE-UNCOMPILED-DEFNS "tmp")
(DEFN SYMBOL (X)
 (MEMBER X (QUOTE (0 1))))
(DEFN HALF-TAPE (X)
 (IF (NLISTP X)
     (EQUAL X 0)
     (AND (SYMBOL (CAR X))
          (HALF-TAPE (CDR X)))))
(DEFN TAPE (X)
 (AND (LISTP X)
      (HALF-TAPE (CAR X))
      (HALF-TAPE (CDR X))))
(DEFN OPERATION (X)
 (MEMBER X (QUOTE (L R 0 1))))
(DEFN STATE (X)
 (LITATOM X))
(DEFN TURING-4TUPLE (X)
 (AND (LISTP X)
      (STATE (CAR X))
      (SYMBOL (CADR X))
      (OPERATION (CADDR X))
      (STATE (CADDDR X))
      (EQUAL (CDDDDR X)
             NIL)))
(DEFN TURING-MACHINE (X)
 (IF (NLISTP X) 
     (EQUAL X NIL)
     (AND (TURING-4TUPLE (CAR X))
          (TURING-MACHINE (CDR X)))))
(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))
(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)))))))
(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)))
(DEFN INSTR-DEFN NIL
 (QUOTE ((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))))
(DEFN NEW-TAPE-DEFN NIL (QUOTE ((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)))))))))
(DEFN TMI-DEFN NIL (QUOTE ((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))))
(DEFN KWOTE (X)
 (LIST 'QUOTE X))
(DEFN tmi-fa (TM)
 (LIST (LIST 'TM NIL (KWOTE TM))
       (CONS 'INSTR (INSTR-DEFN))
       (CONS 'NEW-TAPE (NEW-TAPE-DEFN))
       (CONS 'TMI (TMI-DEFN))))
(DEFN tmi-x (ST TAPE)
 (LIST 'TMI (KWOTE ST)
       (KWOTE TAPE)
       (QUOTE (TM))))
(DEFN LENGTH (X)
 (IF (NLISTP X) 0 (ADD1 (LENGTH (CDR X)))))
(DEFN tmi-k (ST TAPE TM N)
 (DIFFERENCE N (ADD1 (LENGTH TM))))
(DEFN tmi-n (ST TAPE TM K)
 (PLUS K (ADD1 (LENGTH TM))))
(PROVE-LEMMA LENGTH-0 (REWRITE)
            (EQUAL (EQUAL (LENGTH X)
                          0)
                   (NLISTP X)))
(PROVE-LEMMA PLUS-EQUAL-0 (REWRITE)
            (EQUAL (EQUAL (PLUS I J)
                          0)
                   (AND (ZEROP I)
                        (ZEROP J))))
(PROVE-LEMMA PLUS-DIFFERENCE (REWRITE)
            (EQUAL (PLUS (DIFFERENCE I J)
                         J)
                   (IF (LEQ I J)
                       (FIX J)
                       I)))
(TOGGLE DIFFERENCE-OFF DIFFERENCE T)

(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))))
(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)))))))
(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)))))
(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))))))
(PROVE-LEMMA PR-EVAL-QUOTE (REWRITE)
            (EQUAL (EV 'AL (LIST 'QUOTE X)
                       VA FA N)
                   X))
(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)
                                   (QUOTE T))
                            T
                            (IF (EQUAL (PACK X)
                                       'F)
                                F
                                (IF (EQUAL (PACK X)
                                           (QUOTE NIL))
                                    NIL
                                    (GET (PACK X)
                                         VA)))))))
(PROVE-LEMMA EVLIST-NIL (REWRITE)
            (EQUAL (EV 'LIST NIL VA FA N)
                   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))))))
(TOGGLE UNSOLV-SUBRP-OFF UNSOLV-SUBRP T)
(TOGGLE EV-OFF EV T)
(DEFN CNB (X)
 (IF (LISTP X)
     (AND (CNB (CAR X))
          (CNB (CDR X)))
     (NOT (BTMP X))))
(PROVE-LEMMA CNB-NBTM (REWRITE)
            (IMPLIES (CNB X)
                     (EQUAL (BTMP X) F)))
(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)))))
(PROVE-LEMMA CNB-LITATOM (REWRITE)
            (IMPLIES (LITATOM X)
                     (CNB X)))
(PROVE-LEMMA CNB-NUMBERP (REWRITE)
            (IMPLIES (NUMBERP X)
                     (CNB X)))
(TOGGLE CNB-OFF CNB T)
(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))))
(TOGGLE tmi-fa-OFF tmi-fa T)
(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)))
(DEFN PR-EVAL-INSTR-INDUCTION-SCHEME (st sym tm-- VA TM N)
 (IF (ZEROP N)
     T
     (PR-EVAL-INSTR-INDUCTION-SCHEME 'ST 'SYM (QUOTE (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))))
(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))))
(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))))))
(PROVE-LEMMA CNB-INSTRN (REWRITE)
            (IMPLIES (AND (NOT (BTMP (INSTRN ST SYM TM N)))
                          (CNB TM))
                     (CNB (INSTRN ST SYM TM N))))
(PROVE-LEMMA CNB-NEW-TAPE (REWRITE)
            (IMPLIES (AND (CNB OP)
                          (CNB TAPE))
                     (CNB (NEW-TAPE OP TAPE))))
(TOGGLE NEW-TAPE-OFF NEW-TAPE T)
(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))))
(DEFN PR-EVAL-TMI-INDUCTION-SCHEME (st tape tm-- VA TM N)
 (IF (ZEROP N)
     T
     (PR-EVAL-TMI-INDUCTION-SCHEME
      (QUOTE (CAR (CDR (INSTR ST (CAR (CDR TAPE))
                              TM))))
      (QUOTE (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))))
(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))))
(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)))))
(TOGGLE tmi-x-OFF tmi-x T)

(PROVE-LEMMA INSTRN-INSTR (REWRITE)
            (IMPLIES (LESSP (LENGTH TM)
                            N)
                     (EQUAL (INSTRN ST SYM TM N)
                            (INSTR ST SYM TM))))
(PROVE-LEMMA NBTMP-INSTR (REWRITE)
            (IMPLIES (TURING-MACHINE TM)
                     (NOT (BTMP (INSTR ST SYM TM)))))
(PROVE-LEMMA INSTRN-NON-F (REWRITE)
            (IMPLIES (AND (TURING-MACHINE TM)
                          (LEQ N (LENGTH TM)))
                     (INSTRN ST SYM TM N)))
(PROVE-LEMMA TMIN-BTM (REWRITE)
            (IMPLIES (AND (TURING-MACHINE TM)
                          (LEQ N (LENGTH TM)))
                     (EQUAL (TMIN ST TAPE TM N)
                            (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)))))))
(PROVE-LEMMA SYMBOL-CNB (REWRITE)
            (IMPLIES (SYMBOL SYM)
                     (CNB SYM)))
(TOGGLE SYMBOL-OFF SYMBOL T)
(PROVE-LEMMA HALF-TAPE-CNB (REWRITE)
            (IMPLIES (HALF-TAPE X)
                     (CNB X)))
(PROVE-LEMMA TAPE-CNB (REWRITE)
            (IMPLIES (TAPE X)
                     (CNB X)))
(TOGGLE TAPE-OFF TAPE T)
(PROVE-LEMMA OPERATION-CNB (REWRITE)
            (IMPLIES (OPERATION OP)
                     (CNB OP)))
(TOGGLE OPERATION-OFF OPERATION T)
(PROVE-LEMMA TURING-MACHINE-CNB (REWRITE)
            (IMPLIES (TURING-MACHINE TM)
                     (CNB TM)))
(TOGGLE TURING-MACHINE-OFF TURING-MACHINE T)

(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)