#|
Copyright (C) 1994 by Yuan Yu.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Yuan Yu PROVIDES 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 Yuan Yu 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.

#|
----------------------------------------------------------------------------
Date:      Jan, 1991
Modified:  May 18, 1992.
File:      mc20-0.events
----------------------------------------------------------------------------
                 AN ARITHMETIC SUBLIBRARY
|#
; before we start to write our specification, some preliminary theories
; have to be established.
;              THEOREMS ABOUT SET AND BAG
; subset relation.

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

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

else f endif else t endif

; delete the elements of x from the set y.

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

; determines whether x is a subbag of y.

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

; the difference.

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

; the intersection.

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: delete-commutativity 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)

;             THEOREMS ABOUT NATURAL NUMBERS
; lemmas about lessp.

Theorem: lessp-of-1 (x < 1) = (x ≃ 0)

Theorem: lessp-sub1 ((x − 1) < x) = (x ≄ 0)

; lemmas about plus.

Theorem: plus-add1 (1 + x) = (1 + x)

Theorem: plus-add1-1 (x + (1 + y)) = (1 + (x + y))

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

Theorem: plus-commutativity1 (x + (y + z)) = (y + (x + z))

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

Theorem: plus-equal-cancel0 ((x + y) = x) = ((x ∈ N) ∧ (y ≃ 0))

Theorem: plus-equal-cancel ((x + y) = (x + z)) = (fix (y) = fix (z))

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

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

Theorem: plus-lessp-cancel-add1 ((y + x) < (1 + y)) = (x ≃ 0)

Theorem: plus-equal-0 ((x + y) = 0) = ((x ≃ 0) ∧ (y ≃ 0))

; lemmas about difference.

Theorem: sub1-of-1 ((x − 1) = 0) = ((x ≃ 0) ∨ (x = 1))

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

Theorem: difference-sub1-sub1 ((x − (y − 1)) − 1) = if y ≃ 0 then x − 1

elseif x < y then 0 else x − y endif

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

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

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

Theorem: difference-plus1 (x ≮ y) → (((x − y) + z) = ((x + z) − y))

Theorem: difference-plus2 (y ≮ z) → ((x + (y − z)) = ((x + y) − z))

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

Theorem: difference-difference2 (y ≮ z) → ((x − (y − z)) = ((x + z) − y))

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

Theorem: difference-plus-cancel-add1 ((y + x) − (1 + y)) = (x − 1)

Theorem: difference-lessp ((m − n) < m) = ((m ≄ 0) ∧ (n ≄ 0))

Theorem: difference-lessp1 (x < z) → (((x − y) < z) = t)

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

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

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

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

Theorem: difference-lessp-cancel ((a − c) < (b − c)) = if c ≤ a then a < b

else c < b endif

; meta lemmas for plus and difference.  Stolen from basic.events.

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 Theorem: numberp-eval$-plus (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-geq 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-geq (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)

; the meta lemma to cancel identical plus terms in equality.  For example,
;   (EQUAL (PLUS A B C) (PLUS B D E)) => (EQUAL (PLUS A C) (PLUS D E)).

Definition: cancel-equal-plus (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

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

; the meta lemma to cancel identical plus terms in lessp.  For example,
; (DIFFERENCE (PLUS A B C) (PLUS B D E)) => (DIFFERENCE (PLUS A C) (PLUS D E)).

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

then if listp (cadr (x)) ∧ (caadr (x) = 'plus) ∧ listp (caddr (x)) ∧ (caaddr (x) = 'plus)

         then list ('difference,

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 plus-tree (delete (caddr (x), plus-fringe (cadr (x)))) elseif listp (caddr (x))

∧ (caaddr (x) = 'plus)

∧ (cadr (x) ∈ plus-fringe (caddr (x))) then ''0 else x endif

else x endif

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

; the meta lemma to cancel identical plus terms in lessp.  For example,
;   (LESSP (PLUS A B C) (PLUS B D E)) => (LESSP (PLUS A C) (PLUS D E)).

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

then if listp (cadr (x)) ∧ (caadr (x) = 'plus) ∧ listp (caddr (x)) ∧ (caaddr (x) = 'plus)

then list ('lessp,

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 ('quote, f) elseif listp (caddr (x))

∧ (caaddr (x) = 'plus)

∧ (cadr (x) ∈ plus-fringe (caddr (x))) then list ('not,

                 list ('zerop,

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

else x endif else x endif

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

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

; lemmas about times.

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

Theorem: times-distributes-plus (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-add1 (x ∗ (1 + y)) = (x + (x ∗ y))

Theorem: times-commutativity (x ∗ z) = (z ∗ x)

Theorem: times-commutativity1 (x ∗ (y ∗ z)) = (y ∗ (x ∗ z))

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

Theorem: times-equal-1 ((x ∗ y) = 1) = ((x = 1) ∧ (y = 1))

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

Theorem: times-add1-sub1 (1 + (a ∗ (b − 1))) = if (a ≃ 0) ∨ (b ≃ 0) then 1

else (a ∗ b) − (a − 1) endif

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

; x is a boolean value, iff x is either T or F.

Definition: boolean (x) = (truep (x) ∨ falsep (x))

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

Theorem: times-equal-cancel0 (((x ∗ y) = y) = ((y ∈ N)

∧ if y = 0 then t

else x = 1 endif))

∧ (((y ∗ x) = y)

= ((y ∈ N)

∧ if y = 0 then t else x = 1 endif))

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

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

Theorem: times-lessp-1 (1 < (x ∗ y)) = ((x ≄ 0) ∧ (y ≄ 0) ∧ (¬ ((x = 1) ∧ (y = 1))))

Theorem: times-lessp-cancel0 (((x ∗ y) < x) = ((x ≄ 0) ∧ (y ≃ 0))) ∧ ((x < (x ∗ y)) = ((x ≄ 0) ∧ (y ≄ 0) ∧ (y ≠ 1)))

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

Event: Disable equal-iff.

Theorem: times-lessp-cancel-1 ((x ∗ y) < (x + (x ∗ z))) = ((x ≄ 0) ∧ (y ≤ z))

Theorem: times-lessp-linear (i ≮ j ) → ((a ∗ i) ≮ (a ∗ j ))

Theorem: times-distributes-difference ((x ∗ y) − (x ∗ z)) = (x ∗ (y − z))

Theorem: times-distributes-difference1 ((y ∗ x) − (z ∗ x)) = (x ∗ (y − z))

Theorem: times2-add1-lessp-cancel ((1 + (2 ∗ i)) < (2 ∗ j )) = (i < j )

; meta lemmas for times.  Stolen and modified from naturals.events.

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

then append (times-fringe (cadr (x)), times-fringe (caddr (x)))

else cons (x, nil) endif

Definition: times-tree (x) = if x ≃ nil then ''1

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

elseif cddr (x) ≃ nil then list ('times, car (x), cadr (x))

else list ('times, car (x), times-tree (cdr (x))) endif

Definition: and-not-zerop-tree (x) = if x ≃ nil then '(true)

elseif cdr (x) ≃ nil then list ('not, list ('zerop, car (x)))

else list ('and, list ('not, list ('zerop, car (x))), and-not-zerop-tree (cdr (x))) endif

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

Theorem: eval$-times-tree-numberp eval$ (t, times-tree (x), a) ∈ N

Theorem: eval$-times-member (e ∈ x) → (eval$ (t, times-tree (x), a)

= (eval$ (t, e, a) ∗ eval$ (t, times-tree (delete (e, x)), a)))

Theorem: zerop-makes-times-tree-zero ((¬ eval$ (t, and-not-zerop-tree (x), a)) ∧ subbagp (x, y)) → (eval$ (t, times-tree (y), a) = 0)

Theorem: eval$-times-tree-append eval$ (t, times-tree (append (x, y)), a) = (eval$ (t, times-tree (x), a) ∗ eval$ (t, times-tree (y), a))

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

Theorem: eval$-lessp-times-tree-bagdiff (eval$ (t, and-not-zerop-tree (x), a) ∧ subbagp (x, y) ∧ subbagp (x, z)) → ((eval$ (t, times-tree (bagdiff (y, x)), a)

< eval$ (t, times-tree (bagdiff (z, x)), a))

= (eval$ (t, times-tree (y), a) < eval$ (t, times-tree (z), a)))

Theorem: zerop-makes-lessp-false-bridge (¬ eval$ (t,

and-not-zerop-tree (bagint (times-fringe (cons ('times, x)),

times-fringe (cons ('times, y)))),

a))

→ (((eval$ (t, car (x), a) ∗ eval$ (t, cadr (x), a))

< (eval$ (t, car (y), a) ∗ eval$ (t, cadr (y), a)))

= f)

Theorem: and-not-zerop-tree-lessp eval$ (t, and-not-zerop-tree (x), a) = (eval$ (t, times-tree (x), a) ≮ 1)

Definition: eval$-and-not-zerop-tree-end (w, x, a) = eval$ (t, and-not-zerop-tree (delete (w, x)), a)

Theorem: and-not-zerop-tree-delete (w ∈ x) → (eval$ (t, and-not-zerop-tree (delete (w, x)), a)

= if eval$ (t, w, a) ≃ 0 then eval$-and-not-zerop-tree-end (w, x, a) else eval$ (t, times-tree (x), a) ≮ eval$ (t, w, a) endif)

Event: Disable and-not-zerop-tree-lessp.

Definition: lessp-1-times-tree-delete-end (w, x, a) = (1 < eval$ (t, times-tree (delete (w, x)), a))

Theorem: lessp-1-times-tree-delete (w ∈ x) → ((1 < eval$ (t, times-tree (delete (w, x)), a))

= if eval$ (t, w, a) ≃ 0 then lessp-1-times-tree-delete-end (w, x, a) else eval$ (t, w, a) < eval$ (t, times-tree (x), a) endif)

Theorem: eval$-times-fringe-member-zero ((e ∈ times-fringe (cons ('times, x))) ∧ (eval$ (t, e, a) ≃ 0)) → ((eval$ (t, car (x), a) ∗ eval$ (t, cadr (x), a)) = 0)

Definition: cancel-lessp-times (x) = if listp (x) ∧ (car (x) = 'lessp)

then if (caadr (x) = 'times) ∧ (caaddr (x) = 'times)

then if listp (bagint (times-fringe (cadr (x)),

times-fringe (caddr (x))))

then list ('and,

and-not-zerop-tree (bagint (times-fringe (cadr (x)),

times-fringe (caddr (x)))),

              list ('lessp,

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

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

times-fringe (caddr (x))))),

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

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

times-fringe (caddr (x)))))))

else x endif elseif listp (cadr (x))

∧ (caadr (x) = 'times)

∧ (caddr (x) ∈ times-fringe (cadr (x))) then list ('and,

list ('not, list ('zerop, caddr (x))), list ('not,

and-not-zerop-tree (delete (caddr (x),

times-fringe (cadr (x))))))

elseif listp (caddr (x))

∧ (caaddr (x) = 'times)

∧ (cadr (x) ∈ times-fringe (caddr (x))) then list ('and,

list ('not, list ('zerop, cadr (x))),

         list ('lessp,
            ''1,

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

else x endif else x endif

; the meta lemma to cancel identical times terms in lessp. For example,
; (lessp (times b (times c d)) (times b d)) =>
;         (and (and (not (zerop b)) (not (zerop d))) (lessp (fix c) 1))

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

Event: Disable and-not-zerop-tree-delete.

Event: Disable lessp-1-times-tree-delete.

Theorem: eval$-equal-times-tree-bagdiff (eval$ (t, and-not-zerop-tree (x), a) ∧ subbagp (x, y) ∧ subbagp (x, z)) → ((eval$ (t, times-tree (bagdiff (y, x)), a)

= eval$ (t, times-tree (bagdiff (z, x)), a))

= (eval$ (t, times-tree (y), a) = eval$ (t, times-tree (z), a)))

Theorem: zerop-makes-equal-true-bridge (¬ eval$ (t,

and-not-zerop-tree (bagint (times-fringe (cons ('times, x)),

times-fringe (cons ('times, y)))),

a))

→ (((eval$ (t, car (x), a) ∗ eval$ (t, cadr (x), a))

= (eval$ (t, car (y), a) ∗ eval$ (t, cadr (y), a)))

= t)

Definition: equal-1-eval$-times-tree-delete-end (w, x, a) = (eval$ (t, times-tree (delete (w, x)), a) = 1)

Theorem: equal-1-times-tree-delete (w ∈ x) → ((eval$ (t, times-tree (delete (w, x)), a) = 1)

= if eval$ (t, w, a) ≃ 0 then equal-1-eval$-times-tree-delete-end (w, x, a) else eval$ (t, times-tree (x), a) = eval$ (t, w, a) endif)

Definition: cancel-equal-times (x) = if car (x) = 'equal

then if (caadr (x) = 'times) ∧ (caaddr (x) = 'times) then if listp (bagint (times-fringe (cadr (x)),

times-fringe (caddr (x))))

then list ('if, and-not-zerop-tree (bagint (times-fringe (cadr (x)),

times-fringe (caddr (x)))),

              list ('equal,

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

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

times-fringe (caddr (x))))),

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

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

times-fringe (caddr (x)))))),

              '(true))

else x endif elseif listp (cadr (x))

∧ (caadr (x) = 'times)

∧ (caddr (x) ∈ times-fringe (cadr (x))) then list ('and,

list ('numberp, caddr (x)), list ('or,

list ('equal, caddr (x), ''0),

            list ('equal,

times-tree (delete (caddr (x),

times-fringe (cadr (x)))),

                ''1)))

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

then list ('and, list ('numberp, cadr (x)), list ('or,

list ('equal, cadr (x), ''0),

            list ('equal,

times-tree (delete (cadr (x),

times-fringe (caddr (x)))),

                ''1)))

else x endif else x endif

; the meta lemma to cancel identical times term in equality.  For example,
;     (equal (times b (times c d)) (times b d)) =>
;          (or (or (zerop b) (zerop d)) (equal (fix c) 1))

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

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

; lemmas about exp.

Definition: exp (x, y) = if y ≃ 0 then 1

else x ∗ exp (x, y − 1) endif

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-plus (exp (x, y) ∗ exp (x, z)) = exp (x, y + z)

Theorem: exp-times exp (x ∗ y, z) = (exp (x, z) ∗ exp (y, z))

Theorem: exp-exp exp (exp (x, y), z) = exp (x, y ∗ z)

Theorem: exp-of-2-0 (m ≄ 0) → (exp (m, n) ≮ 1)

Theorem: exp-of-2-1 (1 < exp (2, n)) = (n ≄ 0)

Theorem: exp-lessp (exp (x, y) < exp (x, z)) = if x ≃ 0 then (y ≄ 0) ∧ (z ≃ 0)

elseif x = 1 then f else y < z endif

Event: Disable times.

Theorem: times-exp2-lessp ((i ∗ exp (2, j )) < exp (2, k)) = (i < exp (2, k − j ))

; lemmas about remainder and quotient.

Theorem: remainder-exit (i < j ) → ((i mod j ) = fix (i))

Theorem: quotient-exit (i < j ) → ((i ÷ j ) = 0)

Theorem: remainder-0 ((0 mod x) = 0) ∧ ((x mod 0) = fix (x))

Theorem: quotient-0 ((0 ÷ x) = 0) ∧ ((x ÷ 0) = 0)

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

else 1 endif) ∧ ((x mod 1) = 0)

Theorem: quotient-1 ((1 ÷ x) = if x = 1 then 1

else 0 endif) ∧ ((m ÷ 1) = fix (m))

Theorem: remainder-x-x (x mod x) = 0

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

else 1 endif

Theorem: quotient-equal-0 ((m ÷ n) = 0) = ((m ≃ 0) ∨ (n ≃ 0) ∨ (m < n))

Theorem: remainder-2x ((x + x) mod 2) = 0

Theorem: quotient-2x ((x + x) ÷ 2) = fix (x)

Theorem: remainder-2x-add1 ((x + (1 + x)) mod 2) = 1

Theorem: quotient-2x-add1 ((x + (1 + x)) ÷ 2) = fix (x)

; A generalization lemma about quotient.

Theorem: quotient-generalize ((m ÷ n) = 0) = if (m ≃ 0) ∨ (n ≃ 0) then t

else m < n endif

Event: Disable quotient-generalize.

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

Theorem: quotient-lessp ((m ÷ n) < m) = ((m ≄ 0) ∧ ((n ≃ 0) ∨ (n ≠ 1)))

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

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

Theorem: quotient-leq i ≮ (i ÷ j )

Theorem: remainder-wrt-2 (n mod 2) < 2

Theorem: remainder-plus1 ((i mod j ) = 0) → (((x + i) mod j ) = (x mod j ))

Theorem: remainder-plus2 ((i mod j ) = 0) → (((i + x) mod j ) = (x mod j ))

Theorem: remainder-times (((x ∗ y) mod y) = 0) ∧ (((y ∗ x) mod y) = 0)

Theorem: remainder-plus-times1 ((x + (y ∗ z)) mod y) = (x mod y)

Theorem: remainder-plus-times2 ((x + (z ∗ y)) mod y) = (x mod y)

Theorem: remainder-plus-plus ((i mod j ) = 0) → (((x + y + i) mod j ) = ((x + y) mod j ))

Theorem: remainder-plus-add1 ((i mod j ) = 0) → (((1 + (x + i)) mod j ) = ((1 + x) mod j ))

Theorem: remainder-plus-difference1 ((x ≮ z) ∧ ((y mod w) = 0)) → ((((x + y) − z) mod w) = ((x − z) mod w))

Theorem: remainder-plus-difference2 ((y ≮ z) ∧ ((x mod w) = 0)) → ((((x + y) − z) mod w) = ((y − z) mod w))

Theorem: remainder-plus-plus-times1 ((x + w + (y ∗ z)) mod y) = ((x + w) mod y)

Theorem: remainder-plus-plus-times2 ((x + w + (z ∗ y)) mod y) = ((x + w) mod y)

Theorem: remainder-difference ((y mod z) = 0) → (((x − y) mod z)

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

Theorem: remainder-difference-times1 ((x − (y ∗ z)) mod z) = if x < (y ∗ z) then 0

else x mod z endif

Theorem: remainder-difference-times2 ((x − (y ∗ z)) mod y) = if x < (y ∗ z) then 0

else x mod y endif

Theorem: quotient-plus1 ((i mod j ) = 0) → (((x + i) ÷ j ) = ((x ÷ j ) + (i ÷ j )))

Theorem: quotient-plus2 ((i mod j ) = 0) → (((i + x) ÷ j ) = ((i ÷ j ) + (x ÷ j )))

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

else fix (x) endif) ∧ (((y ∗ x) ÷ y)

= if y ≃ 0 then 0 else fix (x) endif)

Theorem: quotient-plus-times1 ((x + (y ∗ z)) ÷ y) = ((x ÷ y)

+ if y ≃ 0 then 0 else fix (z) endif)

Theorem: quotient-plus-times2 ((x + (z ∗ y)) ÷ y) = ((x ÷ y)

+ if y ≃ 0 then 0 else fix (z) endif)

Theorem: quotient-plus-plus ((i mod j ) = 0) → (((x + y + i) ÷ j ) = (((x + y) ÷ j ) + (i ÷ j )))

Theorem: quotient-plus-add1 ((i mod j ) = 0) → (((1 + (x + i)) ÷ j ) = (((1 + x) ÷ j ) + (i ÷ j )))

Theorem: quotient-difference-plus1 ((x ≮ z) ∧ ((y mod w) = 0)) → ((((x + y) − z) ÷ w) = (((x − z) ÷ w) + (y ÷ w)))

Theorem: quotient-difference-plus2 ((y ≮ z) ∧ ((x mod w) = 0)) → ((((x + y) − z) ÷ w) = (((y − z) ÷ w) + (x ÷ w)))

Theorem: quotient-difference ((y mod z) = 0) → (((x − y) ÷ z)

= if x < y then 0 else (x ÷ z) − (y ÷ z) endif)

Theorem: quotient-difference-times1 ((x − (y ∗ z)) ÷ z) = if x < (y ∗ z) then 0

else (x ÷ z) − fix (y) endif

Theorem: quotient-difference-times2 ((x − (y ∗ z)) ÷ y) = if x < (y ∗ z) then 0

else (x ÷ y) − fix (z) endif

Event: Disable remainder-difference.

Event: Disable quotient-difference.

Theorem: remainder-sub1 ((m − 1) mod n) = if n ≃ 0 then m − 1

elseif (m mod n) = 0 then if m ≃ 0 then 0

else n − 1 endif else (m mod n) − 1 endif

Theorem: quotient-sub1 ((m − 1) ÷ n) = if (m mod n) = 0 then (m ÷ n) − 1

else m ÷ n endif

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

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

Theorem: remainder-add1 ((1 + m) mod n) = if n ≃ 0 then 1 + m

elseif (m mod n) = (n − 1) then 0

else 1 + (m mod n) endif

Theorem: quotient-add1 ((1 + m) ÷ n) = if n ≃ 0 then 0

elseif (m mod n) = (n − 1) then 1 + (m ÷ n)

else m ÷ n endif

Theorem: times-plus-lessp (x < d) → (((x + (b ∗ d)) < (c ∗ d)) = (b < c))

Theorem: quotient-shrink-fast x ≮ (y ∗ (x ÷ y))

Theorem: remainder-plus-remainder1 ((x + (y mod z)) mod z) = ((x + y) mod z)

Theorem: remainder-difference-remainder1 if x < y then f else t endif → (((x − (y mod z)) mod z) = ((x − y) mod z))

Theorem: remainder-plus-remainder2 ((x + y + (z mod k)) mod k) = ((x + y + z) mod k)

Theorem: remainder-plus-remainder (((x mod z) + (y mod z)) mod z) = ((x + y) mod z)

Theorem: remainder-crock (y < z) → (((y ∗ x) mod (x ∗ z)) = (y ∗ x))

Theorem: times-distributes-remainder ((x ∗ y) mod (x ∗ z)) = (x ∗ (y mod z))

Theorem: quotient-crock (y < z) → (((y ∗ x) ÷ (x ∗ z)) = 0)

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

else y ÷ z endif

Event: Disable remainder-crock.

Event: Disable quotient-crock.

Theorem: remainder-distributes-times2-add1 ((1 + (2 ∗ y)) mod (2 ∗ z)) = (1 + (2 ∗ (y mod z)))

Theorem: quotient-distributes-times2-add1 ((1 + (2 ∗ y)) ÷ (2 ∗ z)) = (y ÷ z)

Theorem: quotient-exp (1 < i) → ((exp (i, j ) ÷ exp (i, k))

= if j < k then 0 else exp (i, j − k) endif)

Theorem: remainder-exp (1 < i) → ((exp (i, j ) mod exp (i, k))

= if j < k then exp (i, j ) else 0 endif)

Theorem: remainder-plus-cancel0 (((i + j ) mod n) = i) = if n ≃ 0 then (i ∈ N) ∧ (j ≃ 0)

elseif i < n then (i ∈ N) ∧ ((j mod n) = 0)

else f endif Theorem: remainder-plus-cancel (((i + j ) mod n) = ((i + k) mod n)) = ((j mod n) = (k mod n))

Theorem: quotient-times-lessp ((x ÷ z) < y) = if z ≃ 0 then y ≄ 0

else x < (z ∗ y) endif

Theorem: quotient-quotient ((x ÷ z) ÷ y) = (x ÷ (z ∗ y))

; we redefine the distribution law of times and plus, and disable the old one.

Theorem: times-distributes-plus-new ((x ∗ y) + (x ∗ z)) = (x ∗ (y + z))

Event: Disable times-distributes-plus.

; an induction hint for the next event.

Definition: quot2-sub12-induct (x, y, i, j ) = if i ≃ 0 then t

else quot2-sub12-induct (x ÷ 2, y ÷ 2, i − 1, j − 1) endif

Theorem: lessp-plus-times-exp2 (x < exp (2, i)) → (((x + (y ∗ exp (2, i))) < exp (2, n))

= if y ≃ 0 then x < exp (2, n) else y < exp (2, n − i) endif)

Theorem: lessp-plus-exp2 (x < exp (2, i)) → (((x + exp (2, i)) < exp (2, n)) = (i < n))

Theorem: remainder-times-exp2-1 ((x ∗ exp (2, i)) mod exp (2, j )) = ((x mod exp (2, j − i)) ∗ exp (2, i))

Theorem: remainder-times-exp2-2 ((exp (2, i) ∗ x) mod exp (2, j )) = ((x mod exp (2, j − i)) ∗ exp (2, i))

; special cases of remainder-times-exp2.

Theorem: remainder-times-exp2-3 (((x ∗ exp (2, i)) mod 2) = if i ≃ 0 then x mod 2

else 0 endif) ∧ (((exp (2, i) ∗ x) mod 2)

= if i ≃ 0 then x mod 2 else 0 endif)

Theorem: remainder-times-exp2-4 (((x ∗ exp (2, i) ∗ y) mod 2) = if i ≃ 0 then (x ∗ y) mod 2

else 0 endif) ∧ (((x ∗ y ∗ exp (2, i)) mod 2)

= if i ≃ 0 then (x ∗ y) mod 2 else 0 endif)

Theorem: quotient-times-exp2-1 ((x ∗ exp (2, i)) ÷ exp (2, j )) = if i < j then x ÷ exp (2, j − i)

else x ∗ exp (2, i − j ) endif

Theorem: quotient-times-exp2-2 ((exp (2, i) ∗ x) ÷ exp (2, j )) = if i < j then x ÷ exp (2, j − i)

else x ∗ exp (2, i − j ) endif

Theorem: quotient-times-exp2-3 (((x ∗ exp (2, i)) ÷ 2) = if i ≃ 0 then x ÷ 2

else x ∗ exp (2, i − 1) endif) ∧ (((exp (2, i) ∗ x) ÷ 2)

= if i ≃ 0 then x ÷ 2 else x ∗ exp (2, i − 1) endif)

Theorem: quotient-times-exp2-4 (((x ∗ exp (2, i) ∗ y) ÷ 2) = if i ≃ 0 then (x ∗ y) ÷ 2

else x ∗ y ∗ exp (2, i − 1) endif) ∧ (((x ∗ y ∗ exp (2, i)) ÷ 2)

= if i ≃ 0 then (x ∗ y) ÷ 2 else x ∗ y ∗ exp (2, i − 1) endif)

Theorem: remainder-remainder-exp2 ((x mod exp (2, i)) mod exp (2, j )) = if i < j then x mod exp (2, i)

else x mod exp (2, j ) endif

; a lemma for the event add-evenp.

Theorem: remainder-remainder-2 ((x mod exp (2, i)) mod 2) = if i ≃ 0 then 0

else x mod 2 endif

; logarithm is not used in the specification or the lemma library.  It
; comes in when we'd like to reason about the time complexity of programs.

Theorem: times-lessp (x ≤ z) → ((x < (y ∗ z))

= if (y ≃ 0) ∨ (z ≃ 0) then f elseif y = 1 then x < z else t endif)

Definition: log (b, x) = if (b ≃ 0) ∨ (b = 1) then 0

elseif x < b then 0

else 1 + log (b, x ÷ b) endif

Theorem: log-of-0 log (b, 0) = 0

Theorem: log-of-1 (1 < b) → (log (b, 1) = 0)

Theorem: log-equal-0 (log (b, x) = 0) = ((b ≃ 0) ∨ (b = 1) ∨ (x < b))

Theorem: log-exp (1 < b) → (log (b, exp (b, n)) = fix (n))

Theorem: log-times-exp ((1 < b) ∧ (x ≄ 0)) → ((log (b, x ∗ exp (b, n)) = (n + log (b, x)))

∧ (log (b, exp (b, n) ∗ x) = (n + log (b, x))))

Theorem: log-times-exp-1 ((1 < b) ∧ (x ≄ 0)) → ((log (b, x ∗ b) = (1 + log (b, x)))

∧ (log (b, b ∗ x) = (1 + log (b, x))))

Theorem: log-quotient-exp (1 < b) → (log (b, x ÷ exp (b, i)) = (log (b, x) − i))

Definition: quotient2-induct (b, x, y) = if (b ≃ 0) ∨ (b = 1) then 0

elseif (x ≃ 0) ∨ (y ≃ 0) then 0

else quotient2-induct (b, x ÷ b, y ÷ b) endif Theorem: log-leq (x ≤ y) → (log (b, y) ≮ log (b, x))

; these two lemmas are useful in time analysis.

Theorem: ta-lemma-1 (a ≤ a1 ) → ((x + (y ∗ log (2, a))) ≤ (x + (y ∗ log (2, a1 ))))

Theorem: ta-lemma-2 ((a ≤ a1 ) ∧ (b ≤ b1 )) → ((x + (y ∗ (log (2, a) + log (2, b))))

≤ (x + (y ∗ (log (2, a1 ) + log (2, b1 )))))

Event: Make the library "mc20-0" and compile it.

Index

and-not-zerop-tree, 11–15 and-not-zerop-tree-delete, 12 and-not-zerop-tree-lessp, 12

bagdiff, 2, 6–9, 12–15 bagint, 2, 3, 7–9, 12–15 boolean, 10 bridge-to-subbagp-implies-plus-t

ree-geq, 6

cadr-eval$-list, 6 cancel-difference-plus, 8 cancel-equal-plus, 7 cancel-equal-times, 14, 15 cancel-lessp-plus, 8, 9 cancel-lessp-times, 13, 14 correctness-of-cancel-difference

-plus, 8 correctness-of-cancel-equal-plu

s, 7 correctness-of-cancel-equal-time

s, 15 correctness-of-cancel-lessp-plu

s, 9 correctness-of-cancel-lessp-time

s, 14

delete, 2, 3, 6–9, 11–15 delete-commutativity, 3 delete-non-member, 2 difference-0, 4 difference-difference1, 5 difference-difference2, 5 difference-equal-cancel-0, 5 difference-equal-cancel-1, 5 difference-lessp, 5 difference-lessp-cancel, 5 difference-lessp1, 5 difference-plus-cancel-add1, 5 difference-plus-cancel0, 4 difference-plus-cancel1, 5 difference-plus1, 4 difference-plus2, 4 difference-sub1, 4 difference-sub1-sub1, 4 difference-x-x, 4 difference=0, 5

equal-1-eval$-times-tree-delete

-end, 14 equal-1-times-tree-delete, 14 equal-iff, 10 eval$-and-not-zerop-tree-end, 12 eval$-equal-times-tree-bagdiff, 14 eval$-lessp-times-tree-bagdiff, 12 eval$-plus-tree-append, 6 eval$-quote, 7 eval$-times-fringe-member-zero, 13 eval$-times-member, 11 eval$-times-tree-append, 12 eval$-times-tree-numberp, 11 exp, 16, 22–25 exp-exp, 16 exp-lessp, 16 exp-of-0, 16 exp-of-1, 16 exp-of-2-0, 16 exp-of-2-1, 16 exp-plus, 16 exp-times, 16

lessp-1-times-tree-delete, 13 lessp-1-times-tree-delete-end, 12, 13 lessp-of-1, 3 lessp-plus-exp2, 23 lessp-plus-times-exp2, 23 lessp-sub1, 3 listp-eval$, 7 log, 25, 26 log-equal-0, 25 log-exp, 25 log-leq, 26 log-of-0, 25 log-of-1, 25 log-quotient-exp, 25 log-times-exp, 25 log-times-exp-1, 25

member-delete, 3 member-implies-numberp, 6 member-implies-plus-tree-greate

reqp, 6

numberp-eval$-bridge, 6 numberp-eval$-plus, 6 numberp-eval$-plus-tree, 6 numberp-eval$-times, 11

plus-add1, 3 plus-add1-1, 3 plus-associativity, 3 plus-commutativity, 3 plus-commutativity1, 3 plus-equal-0, 4 plus-equal-cancel, 4 plus-equal-cancel0, 4 plus-fringe, 5–9 plus-lessp-cancel-0, 4 plus-lessp-cancel-1, 4 plus-lessp-cancel-2, 9 plus-lessp-cancel-add1, 4 plus-tree, 5–9 plus-tree-bagdiff, 6 plus-tree-delete, 6 plus-tree-plus-fringe, 6

quot2-sub12-induct, 23 quotient-0, 17 quotient-1, 17 quotient-2x, 17 quotient-2x-add1, 17 quotient-add1, 21 quotient-crock, 22 quotient-difference, 20 quotient-difference-plus1, 20 quotient-difference-plus2, 20 quotient-difference-times1, 20 quotient-difference-times2, 20 quotient-distributes-times2-add

1, 22 quotient-equal-0, 17 quotient-exit, 17 quotient-exp, 22 quotient-generalize, 18 quotient-leq, 18 quotient-lessp, 18 quotient-lessp-linear, 18 quotient-plus-add1, 20 quotient-plus-plus, 20 quotient-plus-times1, 20 quotient-plus-times2, 20 quotient-plus1, 19 quotient-plus2, 19 quotient-quotient, 23 quotient-shrink-fast, 21 quotient-sub1, 21 quotient-times, 19 quotient-times-cancel, 22 quotient-times-exp2-1, 24 quotient-times-exp2-2, 24 quotient-times-exp2-3, 24 quotient-times-exp2-4, 24 quotient-times-lessp, 23 quotient-x-x, 17 quotient2-induct, 25

remainder-0, 17 remainder-1, 17 remainder-2x, 17 remainder-2x-add1, 17 remainder-add1, 21 remainder-crock, 22 remainder-difference, 19 remainder-difference-remainder1, 21 remainder-difference-times1, 19 remainder-difference-times2, 19 remainder-distributes-times2-ad

d1, 22 remainder-exit, 16 remainder-exp, 22 remainder-lessp, 18 remainder-lessp-linear, 18 remainder-plus-add1, 18 remainder-plus-cancel, 23 remainder-plus-cancel0, 22 remainder-plus-difference1, 19 remainder-plus-difference2, 19 remainder-plus-plus, 18 remainder-plus-plus-times1, 19 remainder-plus-plus-times2, 19 remainder-plus-remainder, 22 remainder-plus-remainder1, 21 remainder-plus-remainder2, 21 remainder-plus-times1, 18 remainder-plus-times2, 18 remainder-plus1, 18 remainder-plus2, 18 remainder-quotient, 21 remainder-quotient-elim, 21 remainder-remainder-2, 24 remainder-remainder-exp2, 24 remainder-sub1, 21 remainder-times, 18 remainder-times-exp2-1, 23 remainder-times-exp2-2, 23 remainder-times-exp2-3, 23 remainder-times-exp2-4, 24 remainder-wrt-2, 18 remainder-x-x, 17

sub1-of-1, 4 subbagp, 2, 3, 6, 12, 14 subbagp-bagint1, 3 subbagp-bagint2, 3 subbagp-cdr1, 3 subbagp-cdr2, 3 subbagp-delete, 3 subbagp-implies-plus-tree-geq, 6 subset, 2

ta-lemma-1, 26 ta-lemma-2, 26 times-1, 9 times-add1, 9 times-add1-sub1, 10 times-associativity, 10 times-commutativity, 9 times-commutativity1, 9 times-distributes-difference, 11 times-distributes-difference1, 11 times-distributes-plus, 9 times-distributes-plus-new, 23 times-distributes-remainder, 22 times-equal-0, 9 times-equal-1, 9 times-equal-cancel, 10 times-equal-cancel0, 10 times-exp2-lessp, 16 times-fringe, 11–15 times-lessp, 25 times-lessp-0, 10 times-lessp-1, 10 times-lessp-cancel, 10 times-lessp-cancel-1, 10 times-lessp-cancel0, 10 times-lessp-linear, 11 times-plus-lessp, 21 times-tree, 11–15 times-tree-times-fringe, 12 times-zero, 9 times2-add1-lessp-cancel, 11

zerop-makes-equal-true-bridge, 14 zerop-makes-lessp-false-bridge, 12 zerop-makes-times-tree-zero, 12