#|
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 initial nqthm theory.

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

Definition: from-to (i, j ) = if j < i then nil

elseif fix (i) = fix (j ) then list (fix (j ))

else append (from-to (i, j − 1), list (j )) endif

Theorem: plus-right-id2 (y ∉ N) → ((x + y) = fix (x))

Theorem: plus-add1 (x + (1 + y)) = if y ∈ N then 1 + (x + y)

else 1 + x endif

Theorem: commutativity2-of-plus (x + (y + z)) = (y + (x + z))

Theorem: commutativity-of-plus (x + y) = (y + x)

Theorem: associativity-of-plus ((x + y) + z) = (x + (y + z))

Theorem: plus-equal-0 ((a + b) = 0) = ((a ≃ 0) ∧ (b ≃ 0))

Theorem: difference-x-x (x − x) = 0

Theorem: difference-plus (((x + y) − x) = fix (y)) ∧ (((y + x) − x) = fix (y))

Theorem: plus-cancellation ((a + b) = (a + c)) = (fix (b) = fix (c))

Theorem: difference-0 (y ≮ x) → ((x − y) = 0)

Theorem: equal-difference-0 (0 = (x − y)) = (y ≮ x)

Theorem: difference-cancellation-0 (x = (x − y)) = ((x ∈ N) ∧ ((x = 0) ∨ (y ≃ 0)))

Theorem: difference-cancellation-1 ((x − y) = (z − y)) = if x < y then y ≮ z

elseif z < y then y ≮ x else fix (x) = fix (z) endif

Definition: delete (x, y) = if listp (y)

then if x = car (y) then cdr (y)

else cons (car (y), delete (x, cdr (y))) endif else y endif Definition: subbagp (x, y) = if listp (x)

then if car (x) ∈ y then subbagp (cdr (x), delete (car (x), y))

else f endif else t endif

Definition: bagdiff (x, y) = if listp (y)

then if car (y) ∈ x then bagdiff (delete (car (y), x), cdr (y))

else bagdiff (x, cdr (y)) endif else x endif

Definition: bagint (x, y) = if listp (x)

then if car (x) ∈ y then cons (car (x), bagint (cdr (x), delete (car (x), y))) else bagint (cdr (x), y) endif

else nil endif

Theorem: delete-non-member (x ∉ y) → (delete (x, y) = y)

Theorem: member-delete (x ∈ delete (u, v)) → (x ∈ v)

Theorem: commutativity-of-delete delete (x, delete (y, z)) = delete (y, delete (x, z))

Theorem: subbagp-delete subbagp (x, delete (u, y)) → subbagp (x, y)

Theorem: subbagp-cdr1 subbagp (x, y) → subbagp (cdr (x), y)

Theorem: subbagp-cdr2 subbagp (x, cdr (y)) → subbagp (x, y)

Theorem: subbagp-bagint1 subbagp (bagint (x, y), x)

Theorem: subbagp-bagint2 subbagp (bagint (x, y), y)

Definition: plus-fringe (x) = if listp (x) ∧ (car (x) = 'plus)

then append (plus-fringe (cadr (x)), plus-fringe (caddr (x))) else cons (x, nil) endif

Definition: plus-tree (l) = if l ≃ nil then ''0

elseif cdr (l) ≃ nil then list ('fix, car (l))

elseif cddr (l) ≃ nil then list ('plus, car (l), cadr (l)) else list ('plus, car (l), plus-tree (cdr (l))) endif

Definition: cancel (x) = if listp (x) ∧ (car (x) = 'equal)

then if listp (cadr (x))

∧ (caadr (x) = 'plus) ∧ listp (caddr (x)) ∧ (caaddr (x) = 'plus)

then list ('equal,

plus-tree (bagdiff (plus-fringe (cadr (x)),

bagint (plus-fringe (cadr (x)),

plus-fringe (caddr (x))))),

plus-tree (bagdiff (plus-fringe (caddr (x)),

bagint (plus-fringe (cadr (x)),

plus-fringe (caddr (x))))))

elseif listp (cadr (x)) ∧ (caadr (x) = 'plus) ∧ (caddr (x) ∈ plus-fringe (cadr (x)))

then list ('if, list ('numberp, caddr (x)),

                 list ('equal,

plus-tree (delete (caddr (x), plus-fringe (cadr (x)))),

                     ''0),

list ('quote, f))

elseif listp (caddr (x)) ∧ (caaddr (x) = 'plus) ∧ (cadr (x) ∈ plus-fringe (caddr (x)))

then list ('if, list ('numberp, cadr (x)),

                 list ('equal,
                     ''0,

plus-tree (delete (cadr (x), plus-fringe (caddr (x))))),

list ('quote, f))

else x endif else x endif

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

Theorem: numberp-eval$-plus (listp (x) ∧ (car (x) = 'plus)) → (eval$ (t, x, a) ∈ N)

Theorem: numberp-eval$-plus-tree eval$ (t, plus-tree (l), a) ∈ N

Theorem: member-implies-plus-tree-greatereqp (x ∈ y) → (eval$ (t, plus-tree (y), a) ≮ eval$ (t, x, a))

Theorem: plus-tree-delete eval$ (t, plus-tree (delete (x, y)), a) = if x ∈ y then eval$ (t, plus-tree (y), a) − eval$ (t, x, a)

else eval$ (t, plus-tree (y), a) endif

Theorem: subbagp-implies-plus-tree-greatereqp subbagp (x, y) → (eval$ (t, plus-tree (y), a) ≮ eval$ (t, plus-tree (x), a))

Theorem: plus-tree-bagdiff subbagp (x, y) → (eval$ (t, plus-tree (bagdiff (y, x)), a)

= (eval$ (t, plus-tree (y), a) − eval$ (t, plus-tree (x), a)))

Theorem: numberp-eval$-bridge (eval$ (t, z, a) = eval$ (t, plus-tree (x), a)) → (eval$ (t, z, a) ∈ N)

Theorem: bridge-to-subbagp-implies-plus-tree-greatereqp (subbagp (y, plus-fringe (z)) ∧ (eval$ (t, z, a) = eval$ (t, plus-tree (plus-fringe (z)), a))) → ((eval$ (t, z, a) < eval$ (t, plus-tree (y), a)) = f)

Theorem: eval$-plus-tree-append eval$ (t, plus-tree (append (x, y)), a) = (eval$ (t, plus-tree (x), a) + eval$ (t, plus-tree (y), a))

Theorem: plus-tree-plus-fringe eval$ (t, plus-tree (plus-fringe (x)), a) = fix (eval$ (t, x, a))

Theorem: member-implies-numberp ((c ∈ plus-fringe (x)) ∧ (eval$ (t, c, a) ∈ N)) → (eval$ (t, x, a) ∈ N)

Theorem: cadr-eval$-list (car (eval$ ('list, x, a)) = eval$ (t, car (x), a)) ∧ (cdr (eval$ ('list, x, a))

= if listp (x) then eval$ ('list, cdr (x), a) else 0 endif)

Theorem: eval$-quote eval$ (t, cons ('quote, args), a) = car (args)

Theorem: listp-eval$ listp (eval$ ('list, x, a)) = listp (x)

Theorem: correctness-of-cancel eval$ (t, x, a) = eval$ (t, cancel (x), a)

Definition: reverse (x) = if listp (x) then append (reverse (cdr (x)), cons (car (x), nil))

else nil endif

Theorem: associativity-of-append append (append (x, y), z) = append (x, append (y, z))

Definition: plistp (x) = if x ≃ nil then x = nil

else plistp (cdr (x)) endif

Theorem: append-right-id plistp (x) → (append (x, nil) = x)

Theorem: plistp-reverse plistp (reverse (x))

Theorem: append-reverse reverse (append (a, b)) = append (reverse (b), reverse (a))

Theorem: times-zero2 (y ∉ N) → ((x ∗ y) = 0)

Theorem: distributivity-of-times-over-plus (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-add1 (x ∗ (1 + y)) = if y ∈ N then x + (x ∗ y)

else fix (x) endif Theorem: commutativity-of-times (x ∗ y) = (y ∗ x)

Theorem: commutativity2-of-times (x ∗ (y ∗ z)) = (y ∗ (x ∗ z))

Theorem: associativity-of-times ((x ∗ y) ∗ z) = (x ∗ (y ∗ z))

Theorem: equal-times-0 ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

Event: Add the shell push, with recognizer function symbol stackp and 2 accessors: top, with type restriction (none-of) and default value zero; pop, with type restriction (none-of) and default value zero.

Conservative Axiom: numberp-call call (fn, x, y) ∈ N

Simultaneously, we introduce the new function symbols call and getvalue.

Definition: expressionp (x) = if listp (x)

then if listp (car (x)) then f elseif listp (cdr (x)) then if listp (cddr (x))

then if expressionp (cadr (x)) then expressionp (caddr (x))

else f endif else f endif

else f endif else t endif

Theorem: cadr-crock listp (cddr (x)) → (count (cadr (x)) < count (x))

Definition: term-eval (form, envrn) = if form ∈ N then form

elseif listp (cddr (form)) then call (car (form),

term-eval (cadr (form), envrn), term-eval (caddr (form), envrn))

else getvalue (form, envrn) endif Definition: optimize (form) = if listp (cddr (form))

then if optimize (cadr (form)) ∈ N

then if optimize (caddr (form)) ∈ N then call (car (form),

optimize (cadr (form)), optimize (caddr (form)))

else list (car (form), optimize (cadr (form)), optimize (caddr (form))) endif

else list (car (form), optimize (cadr (form)), optimize (caddr (form))) endif

else form endif

Definition: codegen (form, ins) = if form ∈ N then cons (list ('pushi, form), ins)

elseif listp (cddr (form))

then cons (car (form), codegen (caddr (form), codegen (cadr (form), ins))) else cons (list ('pushv, form), ins) endif

Definition: compile (form) = reverse (codegen (optimize (form), nil))

Theorem: formp-optimize expressionp (x) → expressionp (optimize (x))

Theorem: correctness-of-optimize expressionp (x) → (term-eval (optimize (x), envrn) = term-eval (x, envrn))

Definition: exec (pc, pds, envrn) = if pc ≃ nil then pds

elseif listp (car (pc))

then if caar (pc) = 'pushi then exec (cdr (pc), push (cadar (pc), pds), envrn) else exec (cdr (pc),

push (getvalue (cadar (pc), envrn), pds), envrn) endif

else exec (cdr (pc),

push (call (car (pc), top (pop (pds)), top (pds)),

pop (pop (pds))), envrn) endif Theorem: sequential-execution exec (append (x, y), pds, envrn) = exec (y, exec (x, pds, envrn), envrn)

Theorem: correctness-of-codegen expressionp (x) → (exec (reverse (codegen (x, ins)), pds, envrn)

= push (term-eval (x, envrn), exec (reverse (ins), pds, envrn)))

Theorem: correctness-of-optimizing-compiler expressionp (x) → (exec (compile (x), pds, envrn) = push (term-eval (x, envrn), pds))

Theorem: transitivity-of-lessp ((x < y) ∧ (y < z)) → (x < z)

Theorem: lessp-not-reflexive x ≮ x

Definition: eqp (x, y) = (fix (x) = fix (y))

Theorem: trichotomy-of-lessp ((¬ eqp (x, y)) ∧ (y ≮ x)) → (x < y)

Theorem: reverse-reverse plistp (x) → (reverse (reverse (x)) = x)

Definition: flatten (x) = if listp (x) then append (flatten (car (x)), flatten (cdr (x)))

else cons (x, nil) endif

Definition: mc-flatten (x, y) = if listp (x) then mc-flatten (car (x), mc-flatten (cdr (x), y))

else cons (x, y) endif

Theorem: flatten-mc-flatten mc-flatten (x, y) = append (flatten (x), y)

Theorem: member-append (x ∈ append (a, b)) = ((x ∈ a) ∨ (x ∈ b))

Theorem: member-reverse (x ∈ reverse (y)) = (x ∈ y)

Definition: length (x) = if listp (x) then 1 + length (cdr (x))

else 0 endif

Theorem: length-reverse length (reverse (x)) = length (x)

Definition: intersect (x, y) = for x1 in x

when x1 ∈ y collect x1 endfor

Theorem: member-intersect litatom (v) → ((a ∈ for (v,

lst, p,

             'collect,

v, alist))

= ((a ∈ lst) ∧ eval$ (t, p, cons (cons (v, a), alist))))

Theorem: member-union (a ∈ (b ∪ c)) = ((a ∈ b) ∨ (a ∈ c))

Definition: subsetp (x, y) = if listp (x)

then if car (x) ∈ y then subsetp (cdr (x), y)

else f endif else t endif

Theorem: subsetp-union subsetp (a, b) → ((a ∪ b) = b)

Theorem: subsetp-intersect (plistp (a) ∧ subsetp (a, b)) → (intersect (a, b) = a)

Definition: nth (x, n) = if n ≃ 0 then x

else nth (cdr (x), n − 1) endif

Definition: greatereqp (x, y) = (x ≮ y)

Theorem: transitivity-of-leq ((x ≤ y) ∧ (y ≤ z)) → (x ≤ z)

Definition: ordered (l) = if listp (l)

then if listp (cdr (l))

then if cadr (l) < car (l) then f

else ordered (cdr (l)) endif else t endif

else t endif

Definition: addtolist (x, l) = if listp (l)

then if x < car (l) then cons (x, l)

else cons (car (l), addtolist (x, cdr (l))) endif else cons (x, nil) endif

Definition: sort (l) = if listp (l) then addtolist (car (l), sort (cdr (l)))

else nil endif

Definition: boolean (x) = ((x = t) ∨ (x = f))

Theorem: iff-equal-equal (boolean (p) ∧ boolean (q)) → ((p ↔ q) = (p = q))

Theorem: nth-0 nth (0, i) = 0

Theorem: nth-nil nth (nil, i) = if i ≃ 0 then nil

else 0 endif

Theorem: nth-append1 nth (a, i + j ) = nth (nth (a, i), j )

Theorem: associativity-of-equal (boolean (a) ∧ (boolean (b) ∧ boolean (c))) → (((a = b) = c) = (a = (b = c)))

Definition: odd (x) = if x ≃ 0 then f

elseif (x − 1) ≃ 0 then t else odd ((x − 1) − 1) endif

Definition: even1 (x) = if x ≃ 0 then t

else odd (x − 1) endif

Definition: even2 (x) = if x ≃ 0 then t

elseif (x − 1) ≃ 0 then f else even2 ((x − 1) − 1) endif

Definition: double (i) = if i ≃ 0 then 0

else 1 + (1 + double (i − 1)) endif

Theorem: even1-double even1 (double (i))

Definition: half (i) = if i ≃ 0 then 0

elseif (i − 1) ≃ 0 then 0

else 1 + half ((i − 1) − 1) endif

Theorem: half-double (i ∈ N) → (half (double (i)) = i)

Theorem: double-half ((i ∈ N) ∧ even1 (i)) → (double (half (i)) = i)

Theorem: double-times-2 double (i) = (2 ∗ i)

Theorem: subsetp-cons subsetp (x, y) → subsetp (x, cons (z, y))

Definition: last (x) = if listp (x)

then if listp (cdr (x)) then last (cdr (x))

else x endif else x endif Theorem: last-append last (append (a, b)) = if listp (b) then last (b)

elseif listp (a) then cons (car (last (a)), b) else b endif

Theorem: last-reverse listp (a) → (last (reverse (a)) = cons (car (a), nil))

Definition: exp (i, j ) = if j ≃ 0 then 1

else i ∗ exp (i, j − 1) endif

Theorem: exp-plus exp (i, j + k) = (exp (i, j ) ∗ exp (i, k))

Theorem: even1-even2 even1 (x) = even2 (x)

Theorem: leq-nth length (nth (l, i)) ≤ length (l)

Theorem: member-sort (a ∈ sort (b)) = (a ∈ b)

Theorem: length-sort length (sort (a)) = length (a)

Definition: count-list (a, l) = for x in l

count a = x endfor

Theorem: count-list-sort count-list (a, sort (l)) = count-list (a, l)

Theorem: ordered-append ordered (append (a, b)) → ordered (a)

Theorem: leq-half half (i) ≤ i

Definition: number-listp (l) = if listp (l) then (car (l) ∈ N) ∧ number-listp (cdr (l))

else l = nil endif Theorem: ordered-sort ordered (sort (x))

Theorem: addtolist-of-ordered-number-list (ordered (x) ∧ number-listp (x) ∧ (i ∈ N) ∧ (car (x) ≮ i)) → (addtolist (i, x) = cons (i, x))

Theorem: sort-of-ordered-number-list (ordered (x) ∧ number-listp (x)) → (sort (x) = x)

Definition: xor (p, q) = if q

then if p then f

else t endif else p = t endif

Theorem: crock-due-to-lack-of-bounce (x = sort (l)) → ordered (x)

Theorem: sort-ordered number-listp (l) → ((sort (l) = l) = ordered (l))

Definition: subst (x, y, z) = if y = z then x

elseif listp (z) then cons (subst (x, y, car (z)), subst (x, y, cdr (z))) else z endif

Theorem: subst-a-a subst (a, a, b) = b

Definition: occur (x, y) = if x = y then t

elseif listp (y)

then if occur (x, car (y)) then t

else occur (x, cdr (y)) endif else f endif

Theorem: occur-subst (¬ occur (a, b)) → (subst (c, a, b) = b)

Definition: countps-loop (l, pred, ans) = if listp (l) then if apply$ (pred, list (car (l)))

then countps-loop (cdr (l), pred, 1 + ans) else countps-loop (cdr (l), pred, ans) endif

else ans endif

Definition: countps- (l, pred) = countps-loop (l, pred, 0)

Theorem: countps-countps ((n ∈ N) ∧ litatom (x) ∧ (pred ≠ 'quote)) → (countps-loop (l, pred, n)

= (n + for (x, l, list ('quote, t),

                 'count,

list (pred, x),

nil)))

Definition: fact (i) = if i ≃ 0 then 1

else i ∗ fact (i − 1) endif

Definition: fact-loop (i, ans) = if i ≃ 0 then ans

else fact-loop (i − 1, i ∗ ans) endif

Definition: fact- (i) = fact-loop (i, 1)

Theorem: fact-loop-fact (i ∈ N) → (fact-loop (j , i) = (i ∗ fact (j )))

Theorem: fact-fact fact- (i) = fact (i)

Theorem: fact-from-to fact (n) = for i in from-to (1, n)

multiply i endfor

Definition: reverse-loop (x, ans) = if listp (x) then reverse-loop (cdr (x), cons (car (x), ans))

else ans endif

Definition: reverse- (x) = reverse-loop (x, nil)

Theorem: reverse-loop-append-reverse reverse-loop (x, y) = append (reverse (x), y)

Theorem: reverse-loop-reverse reverse-loop (x, nil) = reverse (x)

Theorem: reverse-append reverse- (append (a, b)) = append (reverse- (b), reverse- (a))

Theorem: reverse-reverse-plistp (x) → (reverse- (reverse- (x)) = x)

Definition: sort-lp (x, y) = if listp (x) then sort-lp (cdr (x), addtolist (car (x), y))

else y endif

Theorem: ordered-addtolist ordered (y) → ordered (addtolist (x, y))

Theorem: ordered-sort-lp ordered (y) → ordered (sort-lp (x, y))

Theorem: numberp-count for (x,

l, p,

    'count,

b, a)∈ N

Theorem: count-sort-lp count-list (z, sort-lp (x, y)) = (count-list (z, x) + count-list (z, y))

Theorem: append-cancellation (append (a, b) = append (a, c)) = (b = c)

Theorem: equal-lessp ((x < y) = z) = if x < y then t = z

else f = z endif

Theorem: difference-elim ((y ∈ N) ∧ (y ≮ x)) → ((x + (y − x)) = y)

Definition: power-eval (l, base) = if listp (l) then car (l) + (base ∗ power-eval (cdr (l), base))

else 0 endif

Definition: big-plus1 (l, i, base) = if listp (l)

then if i ≃ 0 then l

else cons ((car (l) + i) mod base,

big-plus1 (cdr (l), (car (l) + i) ÷ base, base)) endif

else cons (i, nil) endif

Theorem: remainder-quotient ((x mod y) + (y ∗ (x ÷ y))) = fix (x)

Theorem: power-eval-big-plus1 power-eval (big-plus1 (l, i, base), base) = (power-eval (l, base) + i)

Definition: big-plus (x, y, i, base) = if listp (x)

then if listp (y)

then cons ((i + (car (x) + car (y))) mod base,

big-plus (cdr (x), cdr (y), (i + (car (x) + car (y))) ÷ base, base))

else big-plus1 (x, i, base) endif else big-plus1 (y, i, base) endif

Theorem: power-eval-big-plus power-eval (big-plus (x, y, i, base), base) = (i + (power-eval (x, base) + power-eval (y, base)))

Theorem: remainder-wrt-1 (y mod 1) = 0

Theorem: remainder-wrt-12 (x ∉ N) → ((y mod x) = fix (y))

Theorem: lessp-remainder2 ((x mod y) < y) = (y ≄ 0)

Theorem: remainder-x-x (x mod x) = 0 Theorem: remainder-quotient-elim ((y ≄ 0) ∧ (x ∈ N)) → (((x mod y) + (y ∗ (x ÷ y))) = x)

Theorem: lessp-times-1 (i ≄ 0) → ((i ∗ j ) ≮ j )

Theorem: lessp-times-2 (i ≄ 0) → ((j ∗ i) ≮ j )

Theorem: lessp-quotient1 ((i ÷ j ) < i) = ((i ≄ 0) ∧ ((j ≃ 0) ∨ (j ≠ 1)))

Theorem: lessp-remainder1 ((x mod y) < x) = ((y ≄ 0) ∧ (x ≄ 0) ∧ (x ≮ y))

Definition: power-rep (i, base) = if i ≃ 0 then nil

elseif base ≃ 0 then cons (i, nil) elseif base = 1 then cons (i, nil) else cons (i mod base, power-rep (i ÷ base, base)) endif

Theorem: power-eval-power-rep power-eval (power-rep (i, base), base) = fix (i)

Theorem: correctness-of-big-plus power-eval (big-plus (power-rep (i, base), power-rep (j , base), 0, base), base) = (i + j )

Definition: gcd (x, y) = if x ≃ 0 then fix (y)

elseif y ≃ 0 then x

elseif x < y then gcd (x, y − x)

else gcd (x − y, y) endif

Theorem: numberp-gcd gcd (x, y) ∈ N

Theorem: gcd-equal-0 (gcd (x, y) = 0) = ((x ≃ 0) ∧ (y ≃ 0))

Theorem: gcd-0 gcd (0, y) = fix (y)

Theorem: commutativity-of-gcd gcd (x, y) = gcd (y, x)

Theorem: nth-append nth (append (a, b), i) = append (nth (a, i), nth (b, i − length (a)))

Theorem: difference-plus1 ((x + y) − x) = fix (y)

Theorem: difference-plus2 ((y + x) − x) = fix (y)

Theorem: difference-plus-cancelation ((x + y) − (x + z)) = (y − z)

Theorem: times-difference (x ∗ (c − w)) = ((c ∗ x) − (w ∗ x))

Definition: divides (x, y) = ((y mod x) ≃ 0)

Theorem: divides-times ((x ∗ z) mod z) = 0

Theorem: difference-plus3 ((b + (a + c)) − a) = (b + c)

Theorem: difference-add1-cancellation ((1 + (y + z)) − z) = (1 + y)

Theorem: remainder-add1 ((y ≄ 0) ∧ (y ≠ 1)) → (((1 + (x ∗ y)) mod y) ≠ 0)

Theorem: divides-plus-rewrite1 (((x mod z) = 0) ∧ ((y mod z) = 0)) → (((x + y) mod z) = 0)

Theorem: divides-plus-rewrite2 (((x mod z) = 0) ∧ ((y mod z) ≠ 0)) → (((x + y) mod z) ≠ 0)

Theorem: divides-plus-rewrite ((x mod z) = 0) → ((((x + y) mod z) = 0) = ((y mod z) = 0))

Theorem: lessp-plus-cancelation ((x + y) < (x + z)) = (y < z)

Theorem: divides-plus-rewrite-commuted ((x mod z) = 0) → ((((y + x) mod z) = 0) = ((y mod z) = 0))

Theorem: euclid ((x mod z) = 0) → ((((y − x) mod z) = 0)

= if x < y then (y mod z) = 0 else t endif)

Theorem: lessp-times-cancellation ((x ∗ z) < (y ∗ z)) = ((z ≄ 0) ∧ (x < y))

Theorem: lessp-plus-cancellation3 (y < (x + y)) = (x ≄ 0)

Theorem: distributivity-of-times-over-gcd gcd (x ∗ z, y ∗ z) = (z ∗ gcd (x, y))

Theorem: gcd-divides-both ((x mod gcd (x, y)) = 0) ∧ ((y mod gcd (x, y)) = 0)

Theorem: gcd-is-the-greatest ((x ≄ 0) ∧ (y ≄ 0) ∧ divides (z, x) ∧ divides (z, y)) → (z ≤ gcd (x, y))

Event: Add the shell cons-if , with recognizer function symbol if-exprp and 3 accessors: test, with type restriction (none-of) and default value zero; leftbranch, with type restriction (none-of) and default value zero; right-branch, with type restriction (none-of) and default value zero.

Definition: assignment (var, alist) = if var = t then t

elseif var = f then f elseif alist ≃ nil then f elseif var = caar (alist) then cdar (alist) else assignment (var, cdr (alist)) endif

Definition: value (x, alist) = if if-exprp (x)

then if value (test (x), alist) then value (left-branch (x), alist)

else value (right-branch (x), alist) endif else assignment (x, alist) endif

Definition: if-depth (x) = if if-exprp (x) then 1 + if-depth (test (x))

else 0 endif

Definition: if-complexity (x) = if if-exprp (x)

then if-complexity (test (x))

∗ (if-complexity (left-branch (x))

+ if-complexity (right-branch (x)))

else 1 endif

Theorem: if-complexity-not-0 if-complexity (x) ≠ 0

Theorem: if-complexity-goes-down1 if-exprp (x) → (if-complexity (left-branch (x)) < if-complexity (x))

Theorem: if-complexity-goes-down2 if-exprp (x) → (if-complexity (right-branch (x)) < if-complexity (x))

Definition: normalize (x) = if if-exprp (x)

then if if-exprp (test (x))

then normalize (cons-if (test (test (x)),

cons-if (left-branch (test (x)), left-branch (x), right-branch (x)), cons-if (right-branch (test (x)), left-branch (x), right-branch (x))))

else cons-if (test (x), normalize (left-branch (x)), normalize (right-branch (x))) endif

else x endif

Definition: normalized-if-exprp (x) = if if-exprp (x)

then (¬ if-exprp (test (x)))

∧ normalized-if-exprp (left-branch (x)) ∧ normalized-if-exprp (right-branch (x))

else t endif

Definition: assignedp (var, alist) = if var = t then t

elseif var = f then t elseif alist ≃ nil then f elseif var = caar (alist) then t else assignedp (var, cdr (alist)) endif

Definition: assume-true (var, alist) = cons (cons (var, t), alist)

Definition: assume-false (var, alist) = cons (cons (var, f), alist)

Definition: tautologyp (x, alist) = if if-exprp (x)

then if assignedp (test (x), alist)

then if assignment (test (x), alist)

then tautologyp (left-branch (x), alist)

else tautologyp (right-branch (x), alist) endif else tautologyp (left-branch (x), assume-true (test (x), alist))

∧ tautologyp (right-branch (x),

assume-false (test (x), alist)) endif

else assignment (x, alist) endif

Theorem: assignment-append assignment (x, append (a, b)) = if assignedp (x, a) then assignment (x, a)

else assignment (x, b) endif

Theorem: value-can-ignore-redundant-assignments (((val ↔ assignment (var, a)) ∧ value (x, a)) → value (x, cons (cons (var, val), a))) ∧ (((val ↔ assignment (var, a)) ∧ (¬ value (x, a)))

→ (¬ value (x, cons (cons (var, val), a))))

Theorem: value-short-cut (if-exprp (x) ∧ normalized-if-exprp (x)) → (value (test (x), a) = assignment (test (x), a))

Theorem: assignment-implies-assigned assignment (x, a) → assignedp (x, a)

Theorem: tautologyp-is-sound (normalized-if-exprp (x) ∧ tautologyp (x, a1 )) → value (x, append (a1 , a2 ))

Definition: tautology-checker (x) = tautologyp (normalize (x), nil)

Definition: falsify1 (x, alist) = if if-exprp (x)

then if assignedp (test (x), alist)

then if assignment (test (x), alist)

then falsify1 (left-branch (x), alist)

else falsify1 (right-branch (x), alist) endif elseif falsify1 (left-branch (x), assume-true (test (x), alist)) then falsify1 (left-branch (x), assume-true (test (x), alist)) else falsify1 (right-branch (x), assume-false (test (x), alist)) endif

elseif assignedp (x, alist)

then if assignment (x, alist) then f

else alist endif else cons (cons (x, f), alist) endif

Definition: falsify (x) = falsify1 (normalize (x), nil)

Theorem: falsify1-extends-models assignedp (x, a) → (assignment (x, falsify1 (y, a))

= if falsify1 (y, a) then assignment (x, a) else x = t endif)

Theorem: falsify1-falsifies (normalized-if-exprp (x) ∧ falsify1 (x, a)) → (value (x, falsify1 (x, a)) = f)

Theorem: tautologyp-fails-means-falsify1-wins (normalized-if-exprp (x) ∧ (¬ tautologyp (x, a)) ∧ a) → falsify1 (x, a)

Theorem: normalize-is-sound value (normalize (x), a) = value (x, a)

Theorem: normalize-normalizes normalized-if-exprp (normalize (x))

Theorem: tautology-checker-completeness-bridge ((value (y, falsify1 (x, a)) = value (x, falsify1 (x, a))) ∧ falsify1 (x, a) ∧ normalized-if-exprp (x)) → (value (y, falsify1 (x, a)) = f)

Theorem: tautology-checker-is-complete (¬ tautology-checker (x)) → (value (x, falsify (x)) = f)

Theorem: tautology-checker-soundness-bridge (tautologyp (y, a1 ) ∧ normalized-if-exprp (y) ∧ (value (x, a2 ) = value (y, append (a1 , a2 )))) → value (x, a2 )

Theorem: tautology-checker-is-sound tautology-checker (x) → value (x, a)

Theorem: flatten-singleton (flatten (x) = cons (y, nil)) = ((x ≃ nil) ∧ (x = y))

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

else 1 + leftcount (car (x)) endif

Definition: gopher (x) = if (x ≃ nil) ∨ (car (x) ≃ nil) then x

else gopher (cons (caar (x), cons (cdar (x), cdr (x)))) endif

Theorem: gopher-preserves-count count (x) ≮ count (gopher (x))

Theorem: listp-gopher listp (gopher (x)) = listp (x)

Definition: samefringe (x, y) = if (x ≃ nil) ∨ (y ≃ nil) then x = y

else (car (gopher (x)) = car (gopher (y)))

∧ samefringe (cdr (gopher (x)), cdr (gopher (y))) endif

Theorem: gopher-returns-leftmost-atom car (gopher (x)) = if listp (x) then car (flatten (x))

else 0 endif

Theorem: gopher-returns-correct-state flatten (cdr (gopher (x))) = if listp (x) then cdr (flatten (x))

else cons (0, nil) endif

Theorem: correctness-of-samefringe samefringe (x, y) = (flatten (x) = flatten (y))

Definition: prime1 (x, y) = if y ≃ 0 then f

elseif y = 1 then t

else (¬ divides (y, x)) ∧ prime1 (x, y − 1) endif

Definition: prime (x) = ((x ≄ 0) ∧ (x ≠ 1) ∧ prime1 (x, x − 1))

Definition: greatest-factor (x, y) = if (y ≃ 0) ∨ (y = 1) then x

elseif divides (y, x) then y

else greatest-factor (x, y − 1) endif

Theorem: greatest-factor-lessp ((y < x) ∧ (¬ prime1 (x, y)) ∧ (x ≄ 0) ∧ ((x − 1) ≠ 0) ∧ (y ≄ 0)) → (greatest-factor (x, y) < x)

Theorem: greatest-factor-divides ((y < x) ∧ (¬ prime1 (x, y)) ∧ (x ≄ 0) ∧ (x ≠ 1) ∧ (y ≄ 0)) → ((x mod greatest-factor (x, y)) = 0)

Theorem: greatest-factor-0 (greatest-factor (x, y) = 0) = (((y ≃ 0) ∨ (y = 1)) ∧ (x = 0))

Theorem: remainder-0-crock (0 mod y) = 0

Theorem: greatest-factor-1 (greatest-factor (x, y) = 1) = (x = 1)

Theorem: numberp-greatest-factor (greatest-factor (x, y) ∈ N) = (¬ (((y ≃ 0) ∨ (y = 1)) ∧ (x ∉ N)))

Definition: prime-factors (x) = if (x ≃ 0) ∨ ((x − 1) = 0) then nil

elseif prime1 (x, x − 1) then cons (x, nil)

else append (prime-factors (greatest-factor (x, x − 1)), prime-factors (x ÷ greatest-factor (x, x − 1))) endif

Definition: prime-list (l) = if l ≃ nil then t

else prime (car (l)) ∧ prime-list (cdr (l)) endif

Definition: times-list (l) = if l ≃ nil then 1

else car (l) ∗ times-list (cdr (l)) endif Theorem: times-list-append times-list (append (x, y)) = (times-list (x) ∗ times-list (y))

Theorem: prime-list-append prime-list (append (x, y)) = (prime-list (x) ∧ prime-list (y))

Theorem: prime-list-prime-factors prime-list (prime-factors (x))

Theorem: quotient-times1 ((y ∈ N) ∧ (x ∈ N) ∧ (x ≠ 0) ∧ divides (x, y)) → ((x ∗ (y ÷ x)) = y)

Theorem: quotient-lessp ((x ≄ 0) ∧ (x < y)) → ((y ÷ x) ≠ 0)

Theorem: enough-factors (x ≄ 0) → (times-list (prime-factors (x)) = x)

Theorem: prime-factorization-existence (x ≄ 0) → ((times-list (prime-factors (x)) = x)

∧ prime-list (prime-factors (x)))

Definition: greatereqpr (w, z) = if w ≃ 0 then z ≃ 0

elseif w = z then t

else greatereqpr (w − 1, z) endif

Theorem: times-id-iff-1 (z = (w ∗ z)) = ((z ∈ N) ∧ ((z = 0) ∨ (w = 1)))

Theorem: prime1-basic ((z ≠ 1) ∧ (z ≠ 0) ∧ (z ∈ N) ∧ greatereqpr (u, z)) → (¬ prime1 (w ∗ z, u))

Theorem: greatereqpr-lessp greatereqpr (x, y) = (x ≮ y)

Theorem: greatereqpr-remainder ((z ≠ (1 + v)) ∧ divides (z, 1 + v)) → greatereqpr (v, z)

Theorem: prime-basic ((z ≠ 1) ∧ (z ≠ x) ∧ (x ≄ 0) ∧ (x ≠ 1) ∧ divides (z, x)) → (¬ prime1 (x, x − 1))

Theorem: remainder-gcd (gcd (b, x) = y) → ((b mod y) = 0)

Theorem: remainder-gcd-1 ((b mod x) ≠ 0) → (gcd (b, x) ≠ x)

Theorem: divides-times1 (a = (z ∗ y)) → ((a mod z) = 0)

Theorem: times-identity1 ((y ∈ N) ∧ (y ≠ 1) ∧ (y ≠ 0) ∧ (x ≠ 0)) → (x ≠ (x ∗ y))

Theorem: times-identity (x = (x ∗ y)) = ((x = 0) ∨ ((x ∈ N) ∧ (y = 1)))

Theorem: kludge-bridge (y = (k ∗ x)) → (gcd (y, a ∗ x) = (x ∗ gcd (a, k)))

Theorem: hack1 ((¬ divides (x, a)) ∧ (a = gcd (x ∗ a, b ∗ a))) → ((k ∗ x) ≠ (b ∗ a))

Theorem: prime-gcd ((¬ divides (x, b)) ∧ (x ≄ 0) ∧ ((x − 1) ≠ 0) ∧ prime1 (x, x − 1)) → ((gcd (b, x) = 1) = t)

Theorem: gcd-distributes-over-an-opened-up-times ((x ∈ N) ∧ (x ≠ 0) ∧ (free = (x ∗ z))) → (gcd (b ∗ z, free) = (z ∗ gcd (b, x)))

Theorem: prime-key ((z ∈ N) ∧ prime (x) ∧ (¬ divides (x, z)) ∧ (¬ divides (x, b))) → ((x ∗ k) ≠ (b ∗ z))

Theorem: quotient-divides ((y ∈ N) ∧ ((x ∗ (y ÷ x)) ≠ y)) → ((y mod x) ≠ 0)

Theorem: little-step (prime (x) ∧ (y ≠ 1) ∧ (x ≠ y)) → ((x mod y) ≠ 0)

Theorem: lessp-count-delete (n ∈ l) → (count (delete (n, l)) < count (l))

Definition: perm (a, b) = if a ≃ nil then b ≃ nil

elseif car (a) ∈ b then perm (cdr (a), delete (car (a), b))

else f endif Theorem: remainder-times ((y ∗ x) mod y) = 0

Theorem: prime-list-delete prime-list (l2 ) → prime-list (delete (x, l2 ))

Theorem: divides-times-list ((c ≄ 0) ∧ (c ∈ l)) → ((times-list (l) mod c) = 0)

Theorem: quotient-times ((y ∗ x) ÷ y) = if y ≃ 0 then 0

else fix (x) endif

Theorem: distributivity-of-divides ((a ≄ 0) ∧ divides (a, w)) → ((c ∗ (w ÷ a)) = ((c ∗ w) ÷ a))

Theorem: times-list-delete ((c ≄ 0) ∧ (c ∈ l)) → (times-list (delete (c, l)) = (times-list (l) ÷ c))

Theorem: prime-list-times-list (prime (c) ∧ prime-list (l2 ) ∧ (c ∉ l2 )) → ((times-list (l2 ) mod c) ≠ 0)

Theorem: if-times-then-divides ((c ≄ 0) ∧ (¬ divides (c, x))) → ((c ∗ y) ≠ x)

Theorem: times-equal-1 ((a ∗ b) = 1) = ((a ≠ 0)

∧ (b ≠ 0)

∧ (a ∈ N)
∧ (b ∈ N)
∧ ((a − 1) = 0)
∧ ((b − 1) = 0))

Theorem: prime-member (((c ∗ times-list (l1 )) = times-list (l2 )) ∧ prime (c) ∧ prime-list (l2 )) → (c ∈ l2 )

Theorem: divides-implies-times ((a ≄ 0) ∧ (c ∈ N) ∧ ((a ∗ c) = b)) → ((c = (b ÷ a)) = t)

Theorem: prime-factorization-uniqueness (prime-list (l1 ) ∧ prime-list (l2 ) ∧ (times-list (l1 ) = times-list (l2 ))) → perm (l1 , l2 )

Definition: maximum (l) = if l ≃ nil then 0

elseif car (l) < maximum (cdr (l)) then maximum (cdr (l)) else car (l) endif

Theorem: member-maximum listp (x) → (maximum (x) ∈ x)

Theorem: lessp-delete-rewrite (count (delete (x, l)) < count (l)) = (x ∈ l)

Definition: ordered2 (l) = if listp (l)

then if listp (cdr (l))

then if car (l) < cadr (l) then f

else ordered2 (cdr (l)) endif else t endif

else t endif

Definition: dsort (l) = if l ≃ nil then nil

else cons (maximum (l), dsort (delete (maximum (l), l))) endif

Definition: addtolist2 (x, l) = if listp (l)

then if x < car (l) then cons (car (l), addtolist2 (x, cdr (l)))

else cons (x, l) endif else cons (x, nil) endif

Definition: sort2 (l) = if l ≃ nil then nil

else addtolist2 (car (l), sort2 (cdr (l))) endif

Theorem: sort2-gen-1 plistp (sort2 (x))

Theorem: sort2-gen-2 ordered2 (sort2 (x))

Theorem: sort2-gen plistp (sort2 (x)) ∧ ordered2 (sort2 (x))

Theorem: addtolist2-delete (plistp (y) ∧ ordered2 (y) ∧ (x ≠ v)) → (addtolist2 (v, delete (x, y)) = delete (x, addtolist2 (v, y)))

Theorem: delete-addtolist2 plistp (y) → (delete (v, addtolist2 (v, y)) = y)

Theorem: addtolist2-kludge ((v ≮ w) ∧ (addtolist2 (v, y) = cons (v, y))) → (addtolist2 (v, addtolist2 (w, y)) = cons (v, addtolist2 (w, y)))

Theorem: lessp-maximum-addtolist2 (v ≮ maximum (z)) → (addtolist2 (v, sort2 (z)) = cons (v, sort2 (z)))

Theorem: sort2-delete-cons listp (x) → (cons (maximum (x), delete (maximum (x), sort2 (x))) = sort2 (x))

Theorem: sort2-delete sort2 (delete (x, l)) = delete (x, sort2 (l))

Theorem: dsort-sort2 dsort (x) = sort2 (x)

Theorem: count-list-sort2 count-list (a, sort2 (l)) = count-list (a, l)

;   The next segment of this XXX illustrates three different program
;   verification methods:  the functional approach, the inductive assertion
;   approach, and the interpreter approach.  The program considered is a simple
;   loop for summing the numbers from I down to 0

Definition: sigma (m, n) = if m < n then n + sigma (m, n − 1)

else 0 endif

Theorem: difference-1 (x − 1) = (x − 1)

Definition: prog-trans-of-sigma (i, ac) = if i ≃ 0 then ac

else prog-trans-of-sigma (i − 1, ac + i) endif

Theorem: functional-loop-invrt (ac ∈ N) → (prog-trans-of-sigma (i, ac) = (ac + sigma (0, i)))

Theorem: correctness-of-functional-sigma prog-trans-of-sigma (i, 0) = sigma (0, i)

Theorem: sigma-input-path (0 = sigma (k, k)) ∧ (k ≤ k)

Theorem: sigma-loop-invrt ((i ≄ 0) ∧ (i ≤ k)) → (((sigma (i, k) + i) = sigma (i − 1, k)) ∧ ((i − 1) ≤ k))

Theorem: sigma-output-path ((i ≃ 0) ∧ (i ≤ k)) → (sigma (i, k) = sigma (0, k))

;   The interpreter we consider fetches instructions out of the same memory
;   being modified by the execution.  Earlier we proved a simpler version in
;   which the program was in read-only memory.  The new approach is almost
;   identical but we have to force the opening up of certain functions because
;   instead of doing CDR recursion the interpreter EXECUTE1 has to count the PC
;   up and the theorem prover doesn't handle counting up very well yet.

Definition: set (addr, val, mem) = if addr ≃ 0 then cons (val, cdr (mem))

else cons (car (mem), set (addr − 1, val, cdr (mem))) endif

Definition: get (addr, mem) = if addr ≃ 0 then car (mem)

else get (addr − 1, cdr (mem)) endif

Theorem: get-set get (j , set (i, val, mem)) = if eqp (j , i) then val

else get (j , mem) endif

Definition: execute1 (pc, mem, max) = if pc ≮ max then list (f, mem)

elseif get (pc, mem) = '(stop) then list (f, mem)

elseif car (get (pc, mem)) = 'jumpa then list (cadr (get (pc, mem)), mem)

elseif car (get (pc, mem)) = 'skipne

then if get (cadr (get (pc, mem)), mem) ≃ 0 then execute1 (1 + pc, mem, max)

else execute1 (1 + (1 + pc), mem, max) endif elseif car (get (pc, mem)) = 'subi then execute1 (1 + pc,

set (cadr (get (pc, mem)), get (cadr (get (pc, mem)), mem) − caddr (get (pc, mem)), mem),

max)

elseif car (get (pc, mem)) = 'addi then execute1 (1 + pc,

set (cadr (get (pc, mem)), caddr (get (pc, mem)) + get (cadr (get (pc, mem)), mem), mem),

max)

elseif car (get (pc, mem)) = 'add then execute1 (1 + pc,

set (cadr (get (pc, mem)), get (caddr (get (pc, mem)), mem) + get (cadr (get (pc, mem)), mem), mem),

max)

elseif car (get (pc, mem)) = 'movei then execute1 (1 + pc,

set (cadr (get (pc, mem)), caddr (get (pc, mem)), mem), max)

else list (f, mem) endif

Definition: execute (pc, mem, clk) = if clk ≃ 0 then mem

elseif pc ∈ N then execute (car (execute1 (pc, mem, length (mem))),

cadr (execute1 (pc, mem, length (mem))), clk − 1)

else mem endif

Definition: get-simplifier (x) = if listp (x)

∧ (car (x) = 'get)

∧ listp (cadr (x))

∧ (car (cadr (x)) = 'quote) then if cadr (cadr (x)) ≃ 0 then list ('car, caddr (x))

else list ('get, list ('quote, cadr (cadr (x)) − 1), list ('cdr, caddr (x))) endif

else x endif Theorem: correctness-of-get-simplifier eval$ (t, x, a) = eval$ (t, get-simplifier (x), a)

Definition: set-simplifier (x) = if listp (x)

∧ (car (x) = 'set) ∧ listp (cadr (x)) ∧ (car (cadr (x)) = 'quote)

then if cadr (cadr (x)) ≃ 0 then list ('cons, caddr (x), list ('cdr, cadddr (x))) else list ('cons,

list ('car, cadddr (x)), list ('set,

list ('quote, cadr (cadr (x)) − 1), caddr (x), list ('cdr, cadddr (x)))) endif

else x endif

Theorem: correctness-of-set-simplifier eval$ (t, x, a) = eval$ (t, set-simplifier (x), a)

Theorem: length-5 (caddddr (x) = '(jumpa 1)) → (length (x) = (5 + length (cdddddr (x))))

Theorem: length-cons6 length (cons (x1 , cons (x2 , cons (x3 , cons (x4 , cons (x5 , cons (x6 , x7 ))))))) = (6 + length (x7 ))

Theorem: execute1-1 (max ≮ 6) → (execute1 (1,

              cons ('(movei 7 0),
                  cons ('(skipne 6),
                       cons ('(stop),
                            cons ('(add 7 6),
                                cons ('(subi 6 1),

cons ('(jumpa 1), l)))))),

max)

= if car (l) ≃ 0

then execute1 (2,

                      cons ('(movei 7 0),
                           cons ('(skipne 6),
                                cons ('(stop),

                                    cons ('(add 7 6),
                                        cons ('(subi 6 1),

cons ('(jumpa 1), l)))))),

max)

else execute1 (3,

                     cons ('(movei 7 0),
                         cons ('(skipne 6),
                              cons ('(stop),
                                   cons ('(add 7 6),
                                       cons ('(subi 6 1),
                                            cons ('(jumpa 1),

l)))))),

max) endif)

Theorem: execute1-3 (max ≮ 6) → (execute1 (3,

             cons ('(movei 7 0),
                  cons ('(skipne 6),
                      cons ('(stop),
                           cons ('(add 7 6),
                                cons ('(subi 6 1),

cons ('(jumpa 1), l)))))),

max)

= execute1 (4,

                 cons ('(movei 7 0),
                     cons ('(skipne 6),
                          cons ('(stop),
                               cons ('(add 7 6),
                                   cons ('(subi 6 1),
                                        cons ('(jumpa 1),

cons (car (l),

cons (car (l) + cadr (l), cddr (l))))))))),

max))

Theorem: execute1-4 (max ≮ 6) → (execute1 (4,

             cons ('(movei 7 0),
                  cons ('(skipne 6),
                      cons ('(stop),
                           cons ('(add 7 6),

                       cons ('(subi 6 1),

cons ('(jumpa 1), l)))))),

max)

= execute1 (5,

        cons ('(movei 7 0),
             cons ('(skipne 6),
                  cons ('(stop),
                      cons ('(add 7 6),
                           cons ('(subi 6 1),
                                cons ('(jumpa 1),

cons (car (l) − 1,

cdr (l)))))))),

max))

(PROVE-LEMMA
EXECUTE1-OPENED-UP
(REWRITE)
(IMPLIES
(AND (NOT (LESSP MAX 6))
(EQUAL (CAR MEM)
       (QUOTE (MOVEI 7 0)))
(EQUAL (CADR MEM)
       (QUOTE (SKIPNE 6)))
(EQUAL (CADDR MEM)
       (QUOTE (STOP)))
(EQUAL (CADDDR MEM)
       (QUOTE (ADD 7 6)))
(EQUAL (CADDDDR MEM)
       (QUOTE (SUBI 6 1)))
(EQUAL (CADDDDDR MEM)
       (QUOTE (JUMPA 1))))
(EQUAL
(EXECUTE1 1 MEM MAX)
(IF
(ZEROP (CADDDDDDR MEM))
(LIST
 F
 (CONS
   (QUOTE (MOVEI 7 0))
   (CONS
     (QUOTE (SKIPNE 6))
     (CONS (QUOTE (STOP))
           (CONS (QUOTE (ADD 7 6))

                         (CONS (QUOTE (SUBI 6 1))
                               (CONS (QUOTE (JUMPA 1))
                                     (CDDDDDDR MEM))))))))
       (LIST
         1
         (CONS
           (QUOTE (MOVEI 7 0))
           (CONS
             (QUOTE (SKIPNE 6))
             (CONS
               (QUOTE (STOP))
               (CONS
                 (QUOTE (ADD 7 6))
                 (CONS
                   (QUOTE (SUBI 6 1))
                   (CONS
                     (QUOTE (JUMPA 1))
                     (CONS (SUB1 (CADDDDDDR MEM))
                           (CONS (PLUS (CADDDDDDR MEM)
                                       (CADDDDDDDR MEM))
                                 (CDDDDDDDDR MEM))))))))))))))

Theorem: execute-opened-up ((pc ∈ N) ∧ (clk ≄ 0)) → (execute (pc, mem, clk)

= execute (car (execute1 (pc, mem, length (mem))), cadr (execute1 (pc, mem, length (mem))), clk − 1))

Theorem: interpreter-loop-invrt ((clk ≮ caddddddr (mem)) ∧ (car (mem) = '(movei 7 0)) ∧ (cadr (mem) = '(skipne 6)) ∧ (caddr (mem) = '(stop)) ∧ (cadddr (mem) = '(add 7 6)) ∧ (caddddr (mem) = '(subi 6 1)) ∧ (cadddddr (mem) = '(jumpa 1))) → (cadddddddr (execute (1, mem, clk))

= if caddddddr (mem) ≃ 0 then cadddddddr (mem) else cadddddddr (mem) + sigma (0, caddddddr (mem)) endif)

Theorem: interpreter-input-path execute (0,

       cons ('(movei 7 0),
           cons ('(skipne 6),

                 cons ('(stop),
                     cons ('(add 7 6),

cons ('(subi 6 1), cons ('(jumpa 1), mem)))))),

clk) = if clk ≃ 0

    then cons ('(movei 7 0),
             cons ('(skipne 6),
                  cons ('(stop),
                       cons ('(add 7 6),

cons ('(subi 6 1), cons ('(jumpa 1), mem))))))

else execute (1,

               cons ('(movei 7 0),
                    cons ('(skipne 6),
                        cons ('(stop),
                             cons ('(add 7 6),
                                  cons ('(subi 6 1),
                                      cons ('(jumpa 1),

cons (car (mem), cons (0,

cddr (mem))))))))),

clk) endif

Theorem: correctness-of-interpreted-sigma ((mem = append ('((movei 7 0)

                  (skipne 6)
                  (stop)
                  (add 7 6)
                  (subi 6 1)
                  (jumpa 1)),

tl))

∧ (i = get (6, mem)) ∧ (clk ≮ i)) → (get (7, execute (0, mem, clk))

= if clk ≃ 0 then get (7, mem) else sigma (0, i) endif)

Theorem: difference-2 ((1 + (1 + x)) − 2) = fix (x)

Theorem: half-plus ((x + (x + y)) ÷ 2) = (x + (y ÷ 2))

Theorem: sigma-is-half-product sigma (0, i) = ((i ∗ (1 + i)) ÷ 2)

Conservative Axiom: h-commutivity2 h (x, h (y, z)) = h (y, h (x, z))

Simultaneously, we introduce the new function symbol h.

Definition: h-pr (l, ac) = if l ≃ nil then ac

else h (car (l), h-pr (cdr (l), ac)) endif

Definition: h-ac (l, ac) = if l ≃ nil then ac

else h-ac (cdr (l), h (car (l), ac)) endif

Theorem: h-lemma h-pr (x, h (z, a)) = h (z, h-pr (x, a))

Theorem: h-eq h-ac (l, ac) = h-pr (l, ac)

Definition: f0 (x) = if 100 < x then x − 10

else 91 endif

#|
(COMMENT
 (DEFN F91 (X)
       (EVAL$ T '(IF (LESSP 100 X)
                   (DIFFERENCE X 10)
                   (F91 (F91 (PLUS X 11))))
              (LIST (CONS 'X X))))
 (REFLECT F91 F0-SATISFIES-F91-EQUATION
          ((LESSP (DIFFERENCE 101 X))))
 (DEFN FOO (A) (IF (LESSP 100 (CDR (ASSOC 'X A)))
                 T
                 (FOO A)))
 (DEFN F91-INDUCTION-HINT (X A)
       (IF (LESSP 100 (CDR (ASSOC 'X A)))
         T
         (AND (F91-INDUCTION-HINT '(PLUS X 11) A)

              (F91-INDUCTION-HINT '(F0 (PLUS X 11)) A)))
       ((LESSP (DIFFERENCE 101 (EVAL$ T X A)))))
 (PROVE-LEMMA F91-TERMINATES ()
              (IMPLIES (V&C$ T X A)
                       (AND  (V&C$ T (LIST 'F91 X) A)
                             (EQUAL (CAR (V&C$ T (LIST 'F91 X) A))
                                    (F0 (CAR (V&C$ T X A))))))
              ((INDUCT (F91-INDUCTION-HINT X A))))
 (PROVE-LEMMA F91-IS-F0 ()
              (EQUAL (F91 X) (F0 X))))
|#

Definition: even (x) = (0 = (x mod 2))

Definition: square (x) = (x ∗ x)

Theorem: times-1 (1 ∗ x) = fix (x)

Theorem: times-2 (2 ∗ x) = (x + x)

Theorem: exp-of-0 exp (0, k) = if k ≃ 0 then 1

else 0 endif

Theorem: exp-of-1 exp (1, k) = 1

Theorem: exp-by-0 exp (x, 0) = 1

Theorem: exp-times exp (i ∗ j , k) = (exp (i, k) ∗ exp (j , k))

Theorem: exp-exp exp (exp (i, j ), k) = exp (i, j ∗ k)

Theorem: remainder-plus-times-1 ((x + (i ∗ j )) mod j ) = (x mod j )

Theorem: remainder-plus-times-2 ((x + (j ∗ i)) mod j ) = (x mod j )

Theorem: remainder-times-1 ((b ∗ (a ∗ c)) mod a) = 0

Theorem: remainder-of-1 (1 mod x) = if x = 1 then 0

else 1 endif

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

Theorem: length-delete length (delete (x, l)) = if x ∈ l then length (cdr (l))

else length (l) endif

Theorem: remainder-difference-times (((p ∗ x) − (p ∗ y)) mod p) = 0

Theorem: prime-key-rewrite prime (p) → ((((a ∗ b) mod p) = 0)

= (((a mod p) = 0) ∨ ((b mod p) = 0)))

Theorem: times-times-list-delete (x ∈ l) → ((x ∗ times-list (delete (x, l))) = times-list (l))

Theorem: lessp-remainder-divisor (y ≄ 0) → ((x mod y) < y)

Event: Introduce the function symbol apply2 of 3 arguments.

Definition: eval2 (form, envrn) = if form ∈ N then form

elseif litatom (form) then cdr (assoc (form, envrn))

elseif listp (form)

then apply2 (car (form), eval2 (cadr (form), envrn), eval2 (caddr (form), envrn))

else form endif

Definition: subst2 (new, old, term) = if term ∈ N then term elseif litatom (term) then if old = term then new

else term endif elseif listp (term) then list (car (term),

subst2 (new, old, cadr (term)), subst2 (new, old, caddr (term)))

else term endif

Theorem: subst2-ok eval2 (subst2 (new, old, term), a) = eval2 (term, cons (cons (old, eval2 (new, a)), a))

Event: Make the library "proveall" and compile it.

Index

addtolist, 11, 14, 16 addtolist-of-ordered-number-list, 14 addtolist2, 29, 30 addtolist2-delete, 30 addtolist2-kludge, 30 append-cancellation, 16 append-reverse, 6 append-right-id, 6 apply2, 40 assignedp, 21–23 assignment, 20, 22, 23 assignment-append, 22 assignment-implies-assigned, 22 associativity-of-append, 6 associativity-of-equal, 11 associativity-of-plus, 2 associativity-of-times, 7 assume-false, 22, 23 assume-true, 21–23

bagdiff, 3–5 bagint, 3, 4 big-plus, 17, 18 big-plus1, 17 boolean, 11 bridge-to-subbagp-implies-plus-t

ree-greatereqp, 5

cadr-crock, 7 cadr-eval$-list, 6 call, 7, 8 cancel, 4, 6 codegen, 8, 9 commutativity-of-delete, 3 commutativity-of-gcd, 18 commutativity-of-plus, 2 commutativity-of-times, 7 commutativity2-of-plus, 2 commutativity2-of-times, 7 compile, 8, 9 cons-if, 20, 21 correctness-of-big-plus, 18 correctness-of-cancel, 6 correctness-of-codegen, 9 correctness-of-functional-sigma, 31 correctness-of-get-simplifier, 33 correctness-of-interpreted-sigm

a, 37 correctness-of-optimize, 8 correctness-of-optimizing-compi

ler, 9 correctness-of-samefringe, 24 correctness-of-set-simplifier, 33 count-list, 13, 16, 30 count-list-sort, 13 count-list-sort2, 30 count-sort-lp, 16 countps-, 15 countps-countps, 15 countps-loop, 14, 15 crock-due-to-lack-of-bounce, 14

delete, 2–5, 27–30, 40 delete-addtolist2, 30 delete-non-member, 3 difference-0, 2 difference-1, 30 difference-2, 37 difference-add1-cancellation, 19 difference-cancellation-0, 2 difference-cancellation-1, 2 difference-elim, 16 difference-plus, 2 difference-plus-cancelation, 19 difference-plus1, 19 difference-plus2, 19 difference-plus3, 19 difference-x-x, 2 distributivity-of-divides, 28 distributivity-of-times-over-gc

d, 20 distributivity-of-times-over-pl

us, 6 divides, 19, 20, 24–28 divides-implies-times, 28 divides-plus-rewrite, 19 divides-plus-rewrite-commuted, 19 divides-plus-rewrite1, 19 divides-plus-rewrite2, 19 divides-times, 19 divides-times-list, 28 divides-times1, 27 double, 12 double-half, 12 double-times-2, 12 dsort, 29, 30 dsort-sort2, 30

enough-factors, 26 eqp, 9, 31 equal-difference-0, 2 equal-length-0, 40 equal-lessp, 16 equal-times-0, 7 euclid, 19 eval2, 40, 41 eval$-plus-tree-append, 5 eval$-quote, 6 even, 39 even1, 12, 13 even1-double, 12 even1-even2, 13 even2, 12, 13 exec, 8, 9 execute, 32, 36, 37 execute-opened-up, 36 execute1, 31–36 execute1-1, 33 execute1-3, 34 execute1-4, 34 exp, 13, 39 exp-by-0, 39 exp-exp, 39 exp-of-0, 39 exp-of-1, 39 exp-plus, 13 exp-times, 39 expressionp, 7–9

f0, 38 fact, 15 fact-, 15 fact-fact, 15 fact-from-to, 15 fact-loop, 15 fact-loop-fact, 15 falsify, 23 falsify1, 22, 23 falsify1-extends-models, 23 falsify1-falsifies, 23 flatten, 9, 24 flatten-mc-flatten, 9 flatten-singleton, 24 formp-optimize, 8 from-to, 1, 15 functional-loop-invrt, 30

gcd, 18, 20, 27 gcd-0, 18 gcd-distributes-over-an-opened-

up-times, 27 gcd-divides-both, 20 gcd-equal-0, 18 gcd-is-the-greatest, 20 get, 31, 32, 37 get-set, 31 get-simplifier, 32, 33 getvalue, 7, 8 gopher, 24 gopher-preserves-count, 24 gopher-returns-correct-state, 24 gopher-returns-leftmost-atom, 24 greatereqp, 10 greatereqpr, 26 greatereqpr-lessp, 26 greatereqpr-remainder, 26 greatest-factor, 25 greatest-factor-0, 25 greatest-factor-1, 25 greatest-factor-divides, 25 greatest-factor-lessp, 25

h, 38 h-ac, 38 h-commutivity2, 38 h-eq, 38 h-lemma, 38 h-pr, 38 hack1, 27 half, 12, 13 half-double, 12 half-plus, 37

if-complexity, 20, 21 if-complexity-goes-down1, 21 if-complexity-goes-down2, 21 if-complexity-not-0, 21 if-depth, 20 if-exprp, 20–22 if-times-then-divides, 28 iff-equal-equal, 11 interpreter-input-path, 36 interpreter-loop-invrt, 36 intersect, 10

kludge-bridge, 27

last, 12, 13 last-append, 13 last-reverse, 13 left-branch, 20–23 leftcount, 24 length, 10, 13, 19, 32, 33, 36, 40 length-5, 33 length-cons6, 33 length-delete, 40 length-reverse, 10 length-sort, 13 leq-half, 13 leq-nth, 13 lessp-count-delete, 27 lessp-delete-rewrite, 29 lessp-maximum-addtolist2, 30 lessp-not-reflexive, 9 lessp-plus-cancelation, 19 lessp-plus-cancellation3, 20 lessp-quotient1, 18 lessp-remainder-divisor, 40 lessp-remainder1, 18 lessp-remainder2, 17 lessp-times-1, 18 lessp-times-2, 18 lessp-times-cancellation, 20 listp-eval$, 6 listp-gopher, 24 little-step, 27

maximum, 29, 30 mc-flatten, 9 member-append, 9 member-delete, 3 member-implies-numberp, 5 member-implies-plus-tree-greate

reqp, 5 member-intersect, 10 member-maximum, 29 member-reverse, 9 member-sort, 13 member-union, 10

normalize, 21–23 normalize-is-sound, 23 normalize-normalizes, 23 normalized-if-exprp, 21–23 nth, 10, 11, 13, 19 nth-0, 11 nth-append, 19 nth-append1, 11 nth-nil, 11 number-listp, 13, 14 numberp-call, 7 numberp-count, 16 numberp-eval$-bridge, 5 numberp-eval$-plus, 5 numberp-eval$-plus-tree, 5 numberp-gcd, 18 numberp-greatest-factor, 25

occur, 14 occur-subst, 14 odd, 12 optimize, 8 ordered, 11, 13, 14, 16 ordered-addtolist, 16 ordered-append, 13 ordered-sort, 14 ordered-sort-lp, 16 ordered2, 29, 30

perm, 27, 28 plistp, 6, 9, 10, 16, 29, 30 plistp-reverse, 6 plus-add1, 1 plus-cancellation, 2 plus-equal-0, 2 plus-fringe, 4, 5 plus-right-id2, 1 plus-tree, 4, 5 plus-tree-bagdiff, 5 plus-tree-delete, 5 plus-tree-plus-fringe, 5 pop, 8 power-eval, 17, 18 power-eval-big-plus, 17 power-eval-big-plus1, 17 power-eval-power-rep, 18 power-rep, 18 prime, 24, 25, 27, 28, 40 prime-basic, 26 prime-factorization-existence, 26 prime-factorization-uniqueness, 28 prime-factors, 25, 26 prime-gcd, 27 prime-key, 27 prime-key-rewrite, 40 prime-list, 25, 26, 28 prime-list-append, 26 prime-list-delete, 28 prime-list-prime-factors, 26 prime-list-times-list, 28 prime-member, 28 prime1, 24–27 prime1-basic, 26 prog-trans-of-sigma, 30, 31 push, 7–9

quotient-divides, 27 quotient-lessp, 26 quotient-times, 28 quotient-times1, 26

remainder-0-crock, 25 remainder-add1, 19 remainder-difference-times, 40 remainder-gcd, 27 remainder-gcd-1, 27 remainder-of-1, 40 remainder-plus-times-1, 39 remainder-plus-times-2, 39 remainder-quotient, 17 remainder-quotient-elim, 18 remainder-times, 28 remainder-times-1, 40 remainder-wrt-1, 17 remainder-wrt-12, 17 remainder-x-x, 17 reverse, 6, 8–10, 13, 16 reverse-, 15, 16 reverse-append, 16 reverse-loop, 15, 16 reverse-loop-append-reverse, 16 reverse-loop-reverse, 16 reverse-reverse, 9 reverse-reverse-, 16 right-branch, 20–23

samefringe, 24

sequential-execution, 9

set, 31, 32

set-simplifier, 33 sigma, 30, 31, 36, 37 sigma-input-path, 31 sigma-is-half-product, 37 sigma-loop-invrt, 31 sigma-output-path, 31 sort, 11, 13, 14 sort-lp, 16 sort-of-ordered-number-list, 14 sort-ordered, 14 sort2, 29, 30 sort2-delete, 30 sort2-delete-cons, 30 sort2-gen, 29 sort2-gen-1, 29 sort2-gen-2, 29 square, 39 subbagp, 3, 5 subbagp-bagint1, 3 subbagp-bagint2, 3 subbagp-cdr1, 3 subbagp-cdr2, 3 subbagp-delete, 3 subbagp-implies-plus-tree-greate

reqp, 5 subsetp, 10, 12 subsetp-cons, 12 subsetp-intersect, 10 subsetp-union, 10 subst, 14 subst-a-a, 14 subst2, 40, 41 subst2-ok, 41

tautology-checker, 22, 23 tautology-checker-completeness-

bridge, 23 tautology-checker-is-complete, 23 tautology-checker-is-sound, 23 tautology-checker-soundness-bri

dge, 23 tautologyp, 22, 23 tautologyp-fails-means-falsify1

-wins, 23 tautologyp-is-sound, 22 term-eval, 7–9 test, 20–23 times-1, 39 times-2, 39 times-add1, 6 times-difference, 19 times-equal-1, 28 times-id-iff-1, 26 times-identity, 27 times-identity1, 27 times-list, 25, 26, 28, 40 times-list-append, 26 times-list-delete, 28 times-times-list-delete, 40 times-zero2, 6 top, 8 transitivity-of-leq, 11 transitivity-of-lessp, 9 trichotomy-of-lessp, 9

value, 20, 22, 23

value-can-ignore-redundant-assi

gnments, 22 value-short-cut, 22

xor, 14