#|
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.
|#

Event: Start with the library "unsolv" using the compiled version.

Event: For efficiency, compile those definitions not yet compiled.

Definition: symbol (x) = (x ∈ '(0 1))

Definition: half-tape (x) = if x ≃ nil then x = 0

else symbol (car (x)) ∧ half-tape (cdr (x)) endif

Definition: tape (x) = (listp (x) ∧ half-tape (car (x)) ∧ half-tape (cdr (x)))

Definition: operation (x) = (x ∈ '(l r 0 1))

Definition: state (x) = litatom (x)

Definition: turing-4tuple (x) = (listp (x)

∧ state (car (x)) ∧ symbol (cadr (x)) ∧ operation (caddr (x)) ∧ state (cadddr (x)) ∧ (cddddr (x) = nil))

Definition: turing-machine (x) = if x ≃ nil then x = nil

else turing-4tuple (car (x)) ∧ turing-machine (cdr (x)) endif

Definition: instr (st, sym, tm) = if listp (tm)

then if st = car (car (tm))

then if sym = car (cdr (car (tm))) then cdr (cdr (car (tm)))

else instr (st, sym, cdr (tm)) endif else instr (st, sym, cdr (tm)) endif

else f endif

Definition: new-tape (op, tape) = if op = 'l

then cons (cdr (car (tape)), cons (car (car (tape)), cdr (tape))) elseif op = 'r then cons (cons (car (cdr (tape)), car (tape)), cdr (cdr (tape))) else cons (car (tape), cons (op, cdr (cdr (tape)))) endif

Definition: tmi (st, tape, tm, n) = if n ≃ 0 then btm

elseif instr (st, car (cdr (tape)), tm)

then tmi (car (cdr (instr (st, car (cdr (tape)), tm))), new-tape (car (instr (st, car (cdr (tape)), tm)), tape), tm, n − 1)

else tape endif

Definition: instr-defn

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

Definition: new-tape-defn

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

Definition: tmi-defn

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

Definition: kwote (x) = list ('quote, x)

Definition: tmi-fa (tm) = list (list ('tm, nil, kwote (tm)), cons ('instr, instr-defn), cons ('new-tape, new-tape-defn), cons ('tmi, tmi-defn))

Definition: tmi-x (st, tape) = list ('tmi, kwote (st), kwote (tape), '(tm))

Definition: length (x) = if x ≃ nil then 0

else 1 + length (cdr (x)) endif

Definition: tmi-k (st, tape, tm, n) = (n − (1 + length (tm)))

Definition: tmi-n (st, tape, tm, k) = (k + (1 + length (tm)))

Theorem: length-0 (length (x) = 0) = (x ≃ nil)

Theorem: plus-equal-0 ((i + j ) = 0) = ((i ≃ 0) ∧ (j ≃ 0))

Theorem: plus-difference ((i − j ) + j ) = if i ≤ j then fix (j )

else i endif

Event: Enable difference; name this event ‘difference-off’.

Theorem: pr-eval-fn-0 ((n ≃ 0)

 ∧ (fn ≠ 'quote)

∧ (fn ≠ 'if) ∧ (¬ unsolv-subrp (fn)) ∧ (vargs = ev ('list, args, va, fa, n))) → (ev ('al, cons (fn, args), va, fa, n) = btm)

Theorem: pr-eval-fn-1 ((n ≄ 0)

 ∧ (fn ≠ 'quote)

∧ (fn ≠ 'if) ∧ (¬ unsolv-subrp (fn)) ∧ (vargs = ev ('list, args, va, fa, n))) → (ev ('al, cons (fn, args), va, fa, n)

= if btmp (vargs) then btm elseif btmp (get (fn, fa)) then btm else ev ('al,

cadr (get (fn, fa)),

pairlist (car (get (fn, fa)), vargs), fa, n − 1) endif)

Theorem: pr-eval-unsolv-subrp (unsolv-subrp (fn) ∧ (vargs = ev ('list, args, va, fa, n))) → (ev ('al, cons (fn, args), va, fa, n)

= if btmp (vargs) then btm else unsolv-apply-subr (fn, vargs) endif)

Theorem: pr-eval-if (vx1 = ev ('al, x1 , va, fa, n)) → (ev ('al, list ('if, x1 , x2 , x3 ), va, fa, n)

= if btmp (vx1 ) then btm elseif vx1 then ev ('al, x2 , va, fa, n) else ev ('al, x3 , va, fa, n) endif)

Theorem: pr-eval-quote ev ('al, list ('quote, x), va, fa, n) = x

Theorem: pr-eval-nlistp (ev ('al, 0, va, fa, n) = 0) ∧ (ev ('al, 1 + n, va, fa, n) = (1 + n)) ∧ (ev ('al, pack (x), va, fa, n)

= if pack (x) = 't then t elseif pack (x) = 'f then f elseif pack (x) = 'nil then nil else get (pack (x), va) endif)

Theorem: evlist-nil ev ('list, nil, va, fa, n) = nil

Theorem: evlist-cons ((vx = ev ('al, x, va, fa, n)) ∧ (vl = ev ('list, l, va, fa, n))) → (ev ('list, cons (x, l), va, fa, n)

= if btmp (vx) then btm elseif btmp (vl) then btm else cons (vx, vl) endif)

Event: Enable unsolv-subrp; name this event ‘unsolv-subrp-off’.

Event: Enable ev; name this event ‘ev-off’.

Definition: cnb (x) = if listp (x) then cnb (car (x)) ∧ cnb (cdr (x))

else ¬ btmp (x) endif

Theorem: cnb-nbtm cnb (x) → (btmp (x) = f)

Theorem: cnb-cons (cnb (cons (a, b)) = (cnb (a) ∧ cnb (b))) ∧ (cnb (x) → cnb (car (x))) ∧ (cnb (x) → cnb (cdr (x)))

Theorem: cnb-litatom litatom (x) → cnb (x)

Theorem: cnb-numberp (x ∈ N) → cnb (x)

Event: Enable cnb; name this event ‘cnb-off’.

Theorem: get-tmi-fa (get ('tm, tmi-fa (tm)) = list (nil, kwote (tm))) ∧ (get ('instr, tmi-fa (tm)) = instr-defn) ∧ (get ('new-tape, tmi-fa (tm)) = new-tape-defn) ∧ (get ('tmi, tmi-fa (tm)) = tmi-defn)

Event: Enable tmi-fa; name this event ‘tmi-fa-off’.

Definition: instrn (st, sym, tm, n) = if n ≃ 0 then btm

elseif listp (tm)

then if st = car (car (tm))

then if sym = car (cdr (car (tm))) then cdr (cdr (car (tm))) else instrn (st, sym, cdr (tm), n − 1) endif

else instrn (st, sym, cdr (tm), n − 1) endif else f endif

Definition: pr-eval-instr-induction-scheme (st, sym, tm–, va, tm, n) = if n ≃ 0 then t

else 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, n − 1) endif

Theorem: pr-eval-instr (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))) → (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))

Theorem: pr-eval-new-tape (cnb (ev ('al, op, va, tmi-fa (tm), n)) ∧ cnb (ev ('al, tape, va, tmi-fa (tm), n))) → (ev ('al, list ('new-tape, op, tape), va, tmi-fa (tm), n)

= if n ≃ 0 then btm

else new-tape (ev ('al, op, va, tmi-fa (tm), n), ev ('al, tape, va, tmi-fa (tm), n)) endif)

Theorem: cnb-instrn ((¬ btmp (instrn (st, sym, tm, n))) ∧ cnb (tm)) → cnb (instrn (st, sym, tm, n))

Theorem: cnb-new-tape (cnb (op) ∧ cnb (tape)) → cnb (new-tape (op, tape))

Event: Enable new-tape; name this event ‘new-tape-off’.

Definition: tmin (st, tape, tm, n) = if n ≃ 0 then btm

elseif btmp (instrn (st, car (cdr (tape)), tm, n − 1)) then btm elseif instrn (st, car (cdr (tape)), tm, n − 1) then tmin (car (cdr (instrn (st, car (cdr (tape)), tm, n − 1))),

new-tape (car (instrn (st, car (cdr (tape)), tm, n − 1)), tape), tm, n − 1)

else tape endif

Definition: pr-eval-tmi-induction-scheme (st, tape, tm–, va, tm, n) = if n ≃ 0 then t

else 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,

n − 1) endif

Theorem: pr-eval-tmi (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))) → (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))

Theorem: pr-eval-tmi-x (cnb (st) ∧ cnb (tape) ∧ cnb (tm)) → (ev ('al, tmi-x (st, tape), nil, tmi-fa (tm), n)

= if n ≃ 0 then btm else tmin (st, tape, tm, n) endif)

Event: Enable tmi-x; name this event ‘tmi-x-off’.

Theorem: instrn-instr (length (tm) < n) → (instrn (st, sym, tm, n) = instr (st, sym, tm))

Theorem: nbtmp-instr turing-machine (tm) → (¬ btmp (instr (st, sym, tm)))

Theorem: instrn-non-f (turing-machine (tm) ∧ (n ≤ length (tm))) → instrn (st, sym, tm, n)

Theorem: tmin-btm (turing-machine (tm) ∧ (n ≤ length (tm))) → (tmin (st, tape, tm, n) = btm)

Theorem: tmin-tmi turing-machine (tm) → (tmi (st, tape, tm, k) = tmin (st, tape, tm, k + (1 + length (tm))))

Theorem: symbol-cnb symbol (sym) → cnb (sym)

Event: Enable symbol; name this event ‘symbol-off’.

Theorem: half-tape-cnb half-tape (x) → cnb (x)

Theorem: tape-cnb tape (x) → cnb (x)

Event: Enable tape; name this event ‘tape-off’.

Theorem: operation-cnb operation (op) → cnb (op)

Event: Enable operation; name this event ‘operation-off’.

Theorem: turing-machine-cnb turing-machine (tm) → cnb (tm)

Event: Enable turing-machine; name this event ‘turing-machine-off’.

Theorem: turing-completeness-of-lisp (state (st) ∧ tape (tape) ∧ turing-machine (tm)) → (((¬ btmp (pr-eval (tmi-x (st, tape), nil, tmi-fa (tm), n)))

→ (¬ btmp (tmi (st, tape, tm, tmi-k (st, tape, tm, n))))) ∧ ((¬ btmp (tmi (st, tape, tm, k))) → (tmi (st, tape, tm, k)

= pr-eval (tmi-x (st, tape), nil, tmi-fa (tm), tmi-n (st, tape, tm, k)))))

Index

btm, 2, 4–9 btmp, 4–10

cnb, 6, 7, 9, 10 cnb-cons, 6 cnb-instrn, 7 cnb-litatom, 6 cnb-nbtm, 6 cnb-new-tape, 7 cnb-numberp, 6 cnb-off, 6

difference-off, 4

ev, 4, 5, 7–9 ev-off, 5 evlist-cons, 5 evlist-nil, 5

get, 5, 6 get-tmi-fa, 6

half-tape, 1, 9 half-tape-cnb, 9

instr, 2, 9 instr-defn, 2, 4, 6 instrn, 6–9 instrn-instr, 9 instrn-non-f, 9

kwote, 3, 4, 6

length, 4, 9 length-0, 4

nbtmp-instr, 9 new-tape, 2, 7, 8 new-tape-defn, 3, 4, 6 new-tape-off, 7

operation, 1, 2, 10 operation-cnb, 10 operation-off, 10

plus-difference, 4 plus-equal-0, 4 pr-eval, 7, 10 pr-eval-fn-0, 4 pr-eval-fn-1, 4 pr-eval-if, 5 pr-eval-instr, 7 pr-eval-instr-induction-scheme, 6, 7 pr-eval-new-tape, 7 pr-eval-nlistp, 5 pr-eval-quote, 5 pr-eval-tmi, 9 pr-eval-tmi-induction-scheme, 8, 9 pr-eval-tmi-x, 9 pr-eval-unsolv-subrp, 5

state, 2, 10 symbol, 1, 2, 9 symbol-cnb, 9 symbol-off, 9

tape, 1, 10 tape-cnb, 10 tape-off, 10 tmi, 2, 9, 10 tmi-defn, 3, 4, 6 tmi-fa, 3, 6–10 tmi-fa-off, 6 tmi-k, 4, 10 tmi-n, 4, 10 tmi-x, 4, 9, 10 tmi-x-off, 9 tmin, 7–9 tmin-btm, 9 tmin-tmi, 9 turing-4tuple, 2 turing-completeness-of-lisp, 10 turing-machine, 2, 9, 10 turing-machine-cnb, 10 turing-machine-off, 10

unsolv-apply-subr, 5 unsolv-subrp, 4, 5 unsolv-subrp-off, 5