Event: Start with the library "bags".

;; Tue Sep 26 10:20:45 1989, from ~wilding/numerical/newnat.events
;; NATURALS Theory
;; Created by Bill Bevier 1988 (see CLI internal note 057)
;; Modifications by Bill Bevier and Matt Wilding (9/89) including
;; adding some new metalemmas for times, reorganizing the theories,
;; removing some extraneous lemmas, and removing dependence upon
;; other theories (by adding the pertinent lemmas).
;; This script requires the bags theory
;; This script sets up a theory for the NATURALS with the following subtheories
;; ADDITION
;; MULTIPLICATION
;; REMAINDER
;; QUOTIENT
;; EXPONENTIATION
;; LOGS
;; GCDS
;; The theories of EXPONENTIATION, LOGS, and GCDS still need a lot of work
; --------------------------------------------------------------------------------
; ARITHMETIC
; --------------------------------------------------------------------------------
; -------------------- PLUS & DIFFERENCE --------------------
; ---------- EQUAL ----------

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

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

Event: Disable plus-cancellation.

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

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

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

Event: Disable difference-cancellation.

; ---------- PLUS ----------

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

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

Theorem: plus-zero-arg2 (y ≃ 0) → ((x + y) = fix (x))

Theorem: plus-add1-arg1 ((1 + a) + b) = (1 + (a + b))

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

else 1 + x endif

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

Theorem: plus-difference-arg1 ((a − b) + c) = if b < a then (a + c) − b

else 0 + c endif

Theorem: plus-difference-arg2 (a + (b − c)) = if c < b then (a + b) − c

else a + 0 endif

; ---------- DIFFERENCE-PLUS cancellation rules ----------
;
; Here are the basic canonicalization rules for differences of sums. These
; are subsumed by the meta lemmas and are therefore globally disabled.
; They are here merely to prove the meta lemmas.

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

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

Event: Disable difference-plus-cancellation.

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

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

Event: Disable difference-plus-plus-cancellation.

Theorem: difference-plus-plus-cancellation-hack ((w + x + a) − (y + z + a)) = ((w + x) − (y + z))

Event: Disable difference-plus-plus-cancellation-hack.

; Here are a few more facts about difference needed to prove the meta lemmas.
; These are disabled here. We re-prove them after the proof of the meta
; lemmas so that they will fire before the meta lemmas in subsequent proofs.

Theorem: diff-sub1-arg2 (a − (b − 1)) = if b ≃ 0 then fix (a)

elseif a < b then 0 else 1 + (a − b) endif

Event: Disable diff-sub1-arg2.

Theorem: diff-diff-arg1 ((x − y) − z) = (x − (y + z))

Theorem: diff-diff-arg2 (a − (b − c)) = if b < c then fix (a)

else (a + c) − b endif

; diff-diff-diff should be removed, but since the hack lemmas for
; correctness-of-cancel-difference-plus are designed for it, we'll
; keep it around.

Theorem: diff-diff-diff ((b ≤ a) ∧ (d ≤ c)) → (((a − b) − (c − d)) = ((a + d) − (b + c)))

Event: Disable diff-diff-diff.

Theorem: difference-lessp-arg1 (a < b) → ((a − b) = 0)

Event: Disable difference-lessp-arg1.

; --------------------------------------------------------------------------------
; Meta Lemmas to Cancel PLUS and DIFFERENCE expressions
; --------------------------------------------------------------------------------
; ---------- PLUS-TREE and PLUS-FRINGE ----------

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 (listp (x) ∧ (car (x) = 'plus)) → (eval$ (t, x, a) ∈ N)

Event: Disable numberp-eval$-plus.

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

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

Event: Disable member-implies-plus-tree-greatereqp.

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

Event: Disable plus-tree-delete.

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

Event: Disable subbagp-implies-plus-tree-greatereqp.

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

Event: Disable plus-tree-bagdiff.

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

Event: Disable numberp-eval$-bridge.

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)

Event: Disable bridge-to-subbagp-implies-plus-tree-greatereqp.

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

Event: Disable eval$-plus-tree-append.

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

Event: Disable plus-tree-plus-fringe.

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

Event: Disable member-implies-numberp.

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)

Event: Disable cadr-eval$-list.

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

Event: Disable eval$-quote.

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

Event: Disable listp-eval$.

; ---------- CANCEL PLUS ----------
; CANCEL-EQUAL-PLUS cancels identical terms in a term which is the equality
; of two sums. 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)

; ---------- CANCEL-DIFFERENCE-PLUS ----------
; CANCEL-DIFFERENCE-PLUS cancels identical terms in a term which is the
; difference of two sums. For example,
;
;  (DIFFERENCE (PLUS A B C) (PLUS B D E)) => (DIFFERENCE (PLUS A C) (PLUS D E))
;
; Using rewrite rules, we canonicalize terms involving  PLUS and DIFFERENCE
; to be the DIFFERENCE of two sums. Then CANCEL-DIFFERENCE-PLUS cancels out

; like terms.

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)

; ---------- DIFFERENCE ----------
; Here are the rules for difference terms which we want to try before
; the meta lemmas. They help canonicalize terms to differences of sums.

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

Theorem: difference-leq-arg1 (a ≤ b) → ((a − b) = 0)

Theorem: difference-add1-arg2 (a − (1 + b)) = if b < a then (a − b) − 1

else 0 endif Theorem: difference-sub1-arg2 (a − (b − 1)) = if b ≃ 0 then fix (a)

elseif a < b then 0 else 1 + (a − b) endif

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

Theorem: difference-difference-arg2 (a − (b − c)) = if b < c then fix (a)

else (a + c) − b endif

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

; ---------- LESSP ----------

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

else c < b endif

Event: Disable lessp-difference-cancellation.

; CANCEL-LESSP-PLUS cancels LESSP terms whose arguments are sums.
; Examples:
; (LESSP (PLUS A B C) (PLUS A C D)) -> (LESSP (FIX B) (FIX D))
; (LESSP A (PLUS A B))  -> (NOT (ZEROP (FIX B)))
; (LESSP (PLUS A B) A)  -> F

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)

; Define the available theory of addition.  To get the list of events to
; put in the theory, evaluate the following form in NQTHM at this point
; in the script. This form lists all  lemmas which are globally enabled,
; and which have non-null lemma type.
;
; (remove-if-not (function (lambda (x)
;     (and (member x (lemmas))
;  (not (assoc x disabled-lemmas))
;  (not (null (nth 2 (get x 'event)))))))
;         chronology)

Event: Let us define the theory addition to consist of the following events: equal-plus-0, equal-difference-0, commutativity-of-plus, commutativity2-of-plus, plus-zero-arg2, plus-add1-arg2, plus-add1-arg1, associativity-of-plus, plus-difference-arg1, plus-difference-arg2, diff-diff-arg1, diff-diff-arg2, correctness-of-cancel-equal-plus, correctness-of-cancel-difference-plus, difference-elim, difference-leq-arg1, differenceadd1-arg2, difference-sub1-arg2, difference-difference-arg1, difference-difference-arg2, difference-x-x, correctness-of-cancel-lessp-plus.

; ---------- TIMES ----------

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

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

;(lemma equal-sub1-times-0 (rewrite)
;       (equal (equal (sub1 (times a b)) 0)
;       (or (zerop a)
;   (zerop b)
;   (and (equal a 1) (equal b 1)))))

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

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

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

else fix (x) endif

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

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

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

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

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

Theorem: times-distributes-over-difference-proof ((a − b) ∗ c) = ((a ∗ c) − (b ∗ c))

Theorem: times-distributes-over-difference (((a − b) ∗ c) = ((a ∗ c) − (b ∗ c))) ∧ ((a ∗ (b − c)) = ((a ∗ b) − (a ∗ c)))

Theorem: times-quotient-proof ((x ≄ 0) ∧ ((y mod x) = 0)) → (((y ÷ x) ∗ x) = fix (y))

Theorem: times-quotient ((y ≄ 0) ∧ ((x mod y) = 0)) → ((((x ÷ y) ∗ y) = fix (x)) ∧ ((y ∗ (x ÷ y)) = fix (x)))

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

Theorem: lessp-times1-proof ((a < b) ∧ (c ≄ 0)) → ((a < (b ∗ c)) = t)

Theorem: lessp-times1 ((a < b) ∧ (c ≄ 0)) → (((a < (b ∗ c)) = t) ∧ ((a < (c ∗ b)) = t))

Theorem: lessp-times2-proof ((a ≤ b) ∧ (c ≄ 0)) → (((b ∗ c) < a) = f)

Theorem: lessp-times2 ((a ≤ b) ∧ (c ≄ 0)) → ((((b ∗ c) < a) = f) ∧ (((c ∗ b) < a) = f))

Theorem: lessp-times3-proof1 ((a ≄ 0) ∧ (1 < b)) → (a < (a ∗ b))

Theorem: lessp-times3-proof2 (a < (a ∗ b)) → ((a ≄ 0) ∧ (1 < b))

Theorem: lessp-times3 ((a < (a ∗ b)) = ((a ≄ 0) ∧ (1 < b))) ∧ ((a < (b ∗ a)) = ((a ≄ 0) ∧ (1 < b)))

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

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

Event: Disable lessp-times-cancellation1.

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

Theorem: lessp-plus-times1 (((a + (b ∗ c)) < b) = ((a < b) ∧ (c ≃ 0))) ∧ (((a + (c ∗ b)) < b) = ((a < b) ∧ (c ≃ 0))) ∧ ((((c ∗ b) + a) < b) = ((a < b) ∧ (c ≃ 0))) ∧ ((((b ∗ c) + a) < b) = ((a < b) ∧ (c ≃ 0)))

Theorem: lessp-plus-times2 ((a ≄ 0) ∧ (x < a)) → ((((x + (a ∗ b)) < (a ∗ c)) = (b < c))

∧ (((x + (b ∗ a)) < (a ∗ c)) = (b < c))

∧ (((x + (a ∗ b)) < (c ∗ a)) = (b < c))
∧ (((x + (b ∗ a)) < (c ∗ a)) = (b < c))
∧ ((((a ∗ b) + x) < (a ∗ c)) = (b < c))
∧ ((((b ∗ a) + x) < (a ∗ c)) = (b < c))
∧ ((((a ∗ b) + x) < (c ∗ a)) = (b < c))
∧ ((((b ∗ a) + x) < (c ∗ a)) = (b < c)))

Theorem: lessp-1-times (1 < (a ∗ b)) = (¬ ((a ≃ 0) ∨ (b ≃ 0) ∨ ((a = 1) ∧ (b = 1))))

;;; meta lemmas to cancel lessp-times and equal-times expressions
;; examples
;; (lessp (times b (times d a)) (times b (times e (times a f)))) ->
;;                                            (and (and (not (zerop a))
;;                                                      (not (zerop b)))
;;                                                 (lessp (fix d) (times e f)))
;;
;; (equal (times b (times c d)) (times b d))    ->
;;                                           (or (or (zerop b) (zerop d))
;;                                               (equal (fix c) 1))

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: 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: or-zerop-tree (x) = if x ≃ nil then '(false)

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

elseif cddr (x) ≃ nil

then list ('or, list ('zerop, car (x)), list ('zerop, cadr (x))) else list ('or, list ('zerop, car (x)), or-zerop-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)

Event: Disable numberp-eval$-times.

Theorem: eval$-times (car (x) = 'times) → (eval$ (t, x, a) = (eval$ (t, cadr (x), a) ∗ eval$ (t, caddr (x), a)))

Event: Disable eval$-times.

Theorem: eval$-or (car (x) = 'or) → (eval$ (t, x, a) = (eval$ (t, cadr (x), a) ∨ eval$ (t, caddr (x), a)))

Event: Disable eval$-or.

Theorem: eval$-equal (car (x) = 'equal) → (eval$ (t, x, a) = (eval$ (t, cadr (x), a) = eval$ (t, caddr (x), a)))

Event: Disable eval$-equal.

Theorem: eval$-lessp (car (x) = 'lessp) → (eval$ (t, x, a) = (eval$ (t, cadr (x), a) < eval$ (t, caddr (x), a)))

Event: Disable eval$-lessp.

Theorem: eval$-quotient

 (car (x) = 'quotient)

→ (eval$ (t, x, a) = (eval$ (t, cadr (x), a) ÷ eval$ (t, caddr (x), a)))

Event: Disable eval$-quotient.

Theorem: eval$-if (car (x) = 'if) → (eval$ (t, x, a)

= if eval$ (t, cadr (x), a) then eval$ (t, caddr (x), a) else eval$ (t, cadddr (x), a) endif)

Event: Disable eval$-if.

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

Event: Disable numberp-eval$-times-tree.

Theorem: lessp-times-arg1 (a ≄ 0) → (((a ∗ x) ≮ (a ∗ y)) = (x ≮ y))

Theorem: infer-equality-from-not-lessp ((a ∈ N) ∧ (b ∈ N)) → (((a ≮ b) ∧ (b ≮ a)) = (a = b))

Theorem: equal-times-arg1 (a ≄ 0) → (((a ∗ x) = (a ∗ y)) = (fix (x) = fix (y)))

Event: Disable equal-times-arg1.

Theorem: equal-times-bridge ((a ∗ b) = (c ∗ (a ∗ d))) = ((a ≃ 0) ∨ (fix (b) = (c ∗ d)))

Event: Disable equal-times-bridge.

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

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

Event: Disable eval$-times-member.

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

Event: Disable zerop-makes-times-tree-zero.

Theorem: or-zerop-tree-is-not-zerop-tree eval$ (t, or-zerop-tree (x), a) = (¬ eval$ (t, and-not-zerop-tree (x), a))

Event: Disable or-zerop-tree-is-not-zerop-tree.

Theorem: zerop-makes-times-tree-zero2 (eval$ (t, or-zerop-tree (x), a) ∧ subbagp (x, y)) → (eval$ (t, times-tree (y), a) = 0)

Event: Disable zerop-makes-times-tree-zero2.

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

Event: Disable times-tree-append.

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

Event: Disable times-tree-of-times-fringe.

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

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

then let inboth be bagint (times-fringe (cadr (x)),

times-fringe (caddr (x)))

in

if listp (inboth) then list ('and,

and-not-zerop-tree (inboth),

                 list ('lessp,

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

else x endif endlet else x endif

Theorem: eval$-lessp-times-tree-bagdiff (subbagp (x, y) ∧ subbagp (x, z) ∧ eval$ (t, and-not-zerop-tree (x), a)) → ((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)))

Event: Disable eval$-lessp-times-tree-bagdiff.

Theorem: zerop-makes-lessp-false-bridge ((car (x) = 'times) ∧ (car (y) = 'times) ∧ (¬ eval$ (t,

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

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

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

= f)

Event: Disable zerop-makes-lessp-false-bridge.

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

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

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

then let inboth be bagint (times-fringe (cadr (x)),

times-fringe (caddr (x)))

in

if listp (inboth) then list ('or,

or-zerop-tree (inboth),

                 list ('equal,

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

else x endif endlet else x endif

Theorem: zerop-makes-equal-true-bridge ((car (x) = 'times) ∧ (car (y) = 'times) ∧ eval$ (t, or-zerop-tree (bagint (times-fringe (x), times-fringe (y))), a)) → (((eval$ (t, cadr (x), a) ∗ eval$ (t, caddr (x), a))

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

= t)

Event: Disable zerop-makes-equal-true-bridge.

Theorem: eval$-equal-times-tree-bagdiff (subbagp (x, y) ∧ subbagp (x, z) ∧ (¬ eval$ (t, or-zerop-tree (x), a))) → ((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)))

Event: Disable eval$-equal-times-tree-bagdiff.

Theorem: cancel-equal-times-preserves-inequality (subbagp (z, x) ∧ subbagp (z, y) ∧ (eval$ (t, times-tree (x), a) ≠ eval$ (t, times-tree (y), a))) → (eval$ (t, times-tree (bagdiff (x, z)), a)

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

Event: Disable cancel-equal-times-preserves-inequality.

Theorem: cancel-equal-times-preserves-inequality-bridge ((car (x) = 'times) ∧ (car (y) = 'times) ∧ ((eval$ (t, cadr (x), a) ∗ eval$ (t, caddr (x), a))

≠ (eval$ (t, cadr (y), a) ∗ eval$ (t, caddr (y), a)))) → (eval$ (t,

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

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

a) ≠ eval$ (t,

times-tree (bagdiff (times-fringe (y),

bagint (times-fringe (x),

times-fringe (y)))),

a))

Event: Disable cancel-equal-times-preserves-inequality-bridge.

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

; Define the available  theory of  multiplication.   To  get the list of
; events to put in the theory,  evaluate the following  form in NQTHM at
; this point  in  the  script. This   form  lists all lemmas   which are
; globally enabled, and which have non-null lemma type.
;
; (remove-if-not (function (lambda (x)
;     (and (member x (lemmas))
;  (not (assoc x disabled-lemmas))
;  (not (null (nth 2 (get x 'event))))
;  (not (member x (nth 2 (get 'addition 'event)))))))
;         chronology)

Event: Let us define the theory multiplication to consist of the following events: equal-times-0, equal-times-1, equal-sub1-0, times-zero, times-add1, commutativityof-times, times-distributes-over-plus, commutativity2-of-times, associativity-of-times, times-distributes-over-difference, times-quotient, times-1-arg1, lessp-times1, lessp-times2, lessp-times3, lessp-plus-times1, lessp-plus-times2, lessp-1-times, correctness-of-cancel-lessp-times, correctness-of-cancel-equal-times.

; ---------- REMAINDER ----------

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

Theorem: remainder-noop (a < b) → ((a mod b) = fix (a))

Theorem: remainder-of-non-number (a ∉ N) → ((a mod n) = (0 mod n))

Theorem: remainder-zero (x ≃ 0) → ((y mod x) = fix (y))

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

Event: Disable plus-remainder-times-quotient.

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

; (lemma remainder-sub1 (rewrite)
;        (implies (and (not (zerop a))
;       (not (zerop b)))
;  (equal (remainder (sub1 a) b)
;         (if (equal (remainder a b) 0)
;     (sub1 b)
;     (sub1 (remainder a b)))))
;        ((enable lessp-remainder
;  remainder-noop
;  remainder-quotient-elim)
;  (enable-theory addition)
;  (induct (remainder a b))))

Theorem: remainder-add1 ((a mod b) = 0) → (((1 + a) mod b) = (1 mod b))

Theorem: remainder-plus-proof ((b mod c) = 0) → (((a + b) mod c) = (a mod c))

Theorem: remainder-plus ((a mod c) = 0) → ((((a + b) mod c) = (b mod c))

∧ (((b + a) mod c) = (b mod c))

∧ (((x + y + a) mod c) = ((x + y) mod c)))

Theorem: equal-remainder-plus-0-proof ((a mod c) = 0) → ((((a + b) mod c) = 0) = ((b mod c) = 0))

Theorem: equal-remainder-plus-0 ((a mod c) = 0) → (((((a + b) mod c) = 0) = ((b mod c) = 0))

∧ ((((b + a) mod c) = 0) = ((b mod c) = 0)) ∧ ((((x + y + a) mod c) = 0)

= (((x + y) mod c) = 0)))

Theorem: equal-remainder-plus-remainder-proof (a < c) → ((((a + b) mod c) = (b mod c)) = (a ≃ 0))

Theorem: equal-remainder-plus-remainder (a < c) → (((((a + b) mod c) = (b mod c)) = (a ≃ 0))

∧ ((((b + a) mod c) = (b mod c)) = (a ≃ 0)))

Event: Disable equal-remainder-plus-remainder.

Theorem: remainder-times1-proof ((b mod c) = 0) → (((a ∗ b) mod c) = 0)

Theorem: remainder-times1 ((b mod c) = 0) → ((((a ∗ b) mod c) = 0) ∧ (((b ∗ a) mod c) = 0))

Theorem: remainder-times1-instance-proof ((x ∗ y) mod y) = 0

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

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

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

Event: Disable remainder-times-times.

Theorem: remainder-times2-proof ((a mod z) = 0) → ((a mod (z ∗ y)) = (z ∗ ((a ÷ z) mod y)))

Theorem: remainder-times2 ((a mod z) = 0) → (((a mod (y ∗ z)) = (z ∗ ((a ÷ z) mod y)))

∧ ((a mod (z ∗ y)) = (z ∗ ((a ÷ z) mod y))))

Theorem: remainder-times2-instance (((x ∗ y) mod (x ∗ z)) = (x ∗ (y mod z))) ∧ (((x ∗ z) mod (y ∗ z)) = ((x mod y) ∗ z))

Theorem: remainder-difference1 ((a mod c) = (b mod c)) → (((a − b) mod c) = ((a mod c) − (b mod c)))

Definition: double-remainder-induction (a, b, c) = if c ≃ 0 then 0

elseif a < c then 0 elseif b < c then 0 else double-remainder-induction (a − c, b − c, c) endif Theorem: remainder-difference2 (((a mod c) = 0) ∧ ((b mod c) ≠ 0)) → (((a − b) mod c)

= if b < a then c − (b mod c) else 0 endif)

Theorem: remainder-difference3 (((b mod c) = 0) ∧ ((a mod c) ≠ 0)) → (((a − b) mod c)

= if b < a then a mod c else 0 endif)

Event: Disable remainder-difference3.

Theorem: equal-remainder-difference-0 (((a − b) mod c) = 0) = if b ≤ a then (a mod c) = (b mod c)

else t endif

Event: Disable equal-remainder-difference-0.

Theorem: lessp-plus-fact (((b mod x) = 0) ∧ ((c mod x) = 0) ∧ (b < c) ∧ (a < x)) → (((a + b) < c) = t)

Event: Disable lessp-plus-fact.

Theorem: remainder-plus-fact (((b mod x) = 0) ∧ ((c mod x) = 0) ∧ (a < x)) → (((a + b) mod c) = (a + (b mod c)))

Theorem: remainder-plus-times-times-proof (a < b) → (((a + (b ∗ c)) mod (b ∗ d))

= (a + ((b ∗ c) mod (b ∗ d))))

Theorem: remainder-plus-times-times (a < b) → ((((a + (b ∗ c)) mod (b ∗ d))

= (a + ((b ∗ c) mod (b ∗ d)))) ∧ (((a + (c ∗ b)) mod (d ∗ b))

= (a + ((c ∗ b) mod (d ∗ b)))))

; REMAINDER-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; TIMES-DISTRIBUTES-OVER-PLUS, REMAINDER-TIMES-TIMES and REMAINDER-PLUS-TIMES-TIMES

Theorem: remainder-plus-times-times-instance (a < b) → ((((a + (b ∗ c) + (b ∗ d)) mod (b ∗ e))

= (a + (b ∗ ((c + d) mod e))))

∧ (((a + (c ∗ b) + (d ∗ b)) mod (e ∗ b)) = (a + (b ∗ ((c + d) mod e)))))

Theorem: remainder-remainder ((b mod a) = 0) → (((n mod b) mod a) = (n mod a))

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

else 1 endif

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

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

Theorem: transitivity-of-divides (((a mod b) = 0) ∧ ((b mod c) = 0)) → ((a mod c) = 0)

; Define the available  theory of  remainder.   To  get the list of
; events to put in the theory,  evaluate the following  form in NQTHM at
; this point  in  the  script. This   form  lists all lemmas   which are
; globally enabled, and which have non-null lemma type.
;
;
; (let ((lemmas (lemmas)))
;   (remove-if-not (function (lambda (x)
;       (and (member x lemmas)
;    (not (assoc x disabled-lemmas))
;    (not (null (nth 2 (get x 'event))))
;    (not (member x (nth 2 (get 'addition 'event))))
;    (not (member x (nth 2 (get 'multiplication 'event)))))))
;   chronology))

Event: Let us define the theory remainders to consist of the following events: lessp-remainder, remainder-noop, remainder-of-non-number, remainder-zero, remainderquotient-elim, remainder-add1, remainder-plus, equal-remainder-plus-0, remaindertimes1, remainder-times1-instance, remainder-times2, remainder-times2-instance, remainder-difference1, remainder-difference2, remainder-plus-times-times, remainderplus-times-times-instance, remainder-remainder, remainder-1-arg1, remainder-1-arg2, remainder-x-x.

; ---------- QUOTIENT, DIVIDES  ----------

Theorem: quotient-noop (b = 1) → ((a ÷ b) = fix (a))

Theorem: quotient-of-non-number (a ∉ N) → ((a ÷ n) = (0 ÷ n))

Theorem: quotient-zero (x ≃ 0) → ((y ÷ x) = 0)

Theorem: quotient-add1 ((a mod b) = 0) → (((1 + a) ÷ b)

= if b = 1 then 1 + (a ÷ b) else a ÷ b endif)

Theorem: equal-quotient-0 ((a ÷ b) = 0) = ((b ≃ 0) ∨ (a < b))

Theorem: quotient-sub1 ((a ≄ 0) ∧ (b ≄ 0)) → (((a − 1) ÷ b)

= if (a mod b) = 0 then (a ÷ b) − 1 else a ÷ b endif)

Theorem: quotient-plus-proof ((b mod c) = 0) → (((a + b) ÷ c) = ((a ÷ c) + (b ÷ c)))

Theorem: quotient-plus ((a mod c) = 0) → ((((a + b) ÷ c) = ((a ÷ c) + (b ÷ c)))

∧ (((b + a) ÷ c) = ((a ÷ c) + (b ÷ c)))

∧ (((x + y + a) ÷ c)
= (((x + y) ÷ c) + (a ÷ c))))

; I need QUOTIENT-TIMES-INSTANCE to prove the more general QUOTIENT-TIMES,
; but I want QUOTIENT-TIMES-INSTANCE to be tried first (i.e. come after
; QUOTIENT-TIMES in the event list.) So first, prove QUOTIENT-TIMES-INSTANCE-TEMP,
; then prove QUOTIENT-TIMES, and finally give QUOTIENT-TIMES-INSTANCE.

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

else fix (x) endif

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

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

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

Event: Disable quotient-times-instance-temp.

Theorem: quotient-times-proof ((a mod c) = 0) → (((a ∗ b) ÷ c) = (b ∗ (a ÷ c)))

Theorem: quotient-times ((a mod c) = 0) → ((((a ∗ b) ÷ c) = (b ∗ (a ÷ c)))

∧ (((b ∗ a) ÷ c) = (b ∗ (a ÷ c))))

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

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

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

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

else y ÷ z endif

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

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

= if z ≃ 0 then 0 else x ÷ y endif)

Event: Disable quotient-times-times.

Theorem: quotient-difference1 ((a mod c) = (b mod c)) → (((a − b) ÷ c) = ((a ÷ c) − (b ÷ c)))

Theorem: quotient-lessp-arg1 (a < b) → ((a ÷ b) = 0)

Theorem: quotient-difference2 (((a mod c) = 0) ∧ ((b mod c) ≠ 0)) → (((a − b) ÷ c)

= if b < a then (a ÷ c) − (1 + (b ÷ c)) else 0 endif)

Theorem: quotient-difference3 (((b mod c) = 0) ∧ ((a mod c) ≠ 0)) → (((a − b) ÷ c)

= if b < a then (a ÷ c) − (b ÷ c) else 0 endif)

Theorem: remainder-equals-its-first-argument (a = (a mod b)) = ((a ∈ N) ∧ ((b ≃ 0) ∨ (a < b)))

Event: Disable remainder-equals-its-first-argument.

Theorem: quotient-remainder-times ((x mod (a ∗ b)) ÷ a) = ((x ÷ a) mod b)

Theorem: quotient-remainder ((c mod a) = 0) → (((b mod c) ÷ a) = ((b ÷ a) mod (c ÷ a)))

Theorem: quotient-remainder-instance ((x mod (a ∗ b)) ÷ a) = ((x ÷ a) mod b)

Theorem: quotient-plus-fact (((b mod x) = 0) ∧ ((c mod x) = 0) ∧ (a < x)) → (((a + b) ÷ c) = (b ÷ c))

Theorem: quotient-plus-times-times-proof (a < b) → (((a + (b ∗ c)) ÷ (b ∗ d)) = ((b ∗ c) ÷ (b ∗ d)))

Theorem: quotient-plus-times-times (a < b) → ((((a + (b ∗ c)) ÷ (b ∗ d)) = ((b ∗ c) ÷ (b ∗ d)))

∧ (((a + (b ∗ c)) ÷ (b ∗ d))

= ((b ∗ c) ÷ (b ∗ d))))

; QUOTIENT-PLUS-TIMES-TIMES-INSTANCE is the completion of the rules
; QUOTIENT-TIMES-TIMES, QUOTIENT-PLUS-TIMES-TIMES and TIMES-DISTRIBUTES-OVER-PLUS

Theorem: quotient-plus-times-times-instance (a < b) → ((((a + (b ∗ c) + (b ∗ d)) ÷ (b ∗ e))

= if b ≃ 0 then 0

else (c + d) ÷ e endif) ∧ (((a + (c ∗ b) + (d ∗ b)) ÷ (e ∗ b))

= if b ≃ 0 then 0 else (d + c) ÷ e endif))

Theorem: quotient-quotient ((b ÷ a) ÷ c) = (b ÷ (a ∗ c))

Theorem: leq-quotient (a < b) → ((a ÷ c) ≤ (b ÷ c))

Theorem: quotient-1-arg2 (n ÷ 1) = fix (n)

Theorem: quotient-1-arg1-casesplit (n ≃ 0) ∨ (n = 1) ∨ (1 < n)

Theorem: quotient-1-arg1 (1 ÷ n) = if n = 1 then 1

else 0 endif

Theorem: quotient-x-x (x ≄ 0) → ((x ÷ x) = 1)

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

;; Metalemma to cancel quotient-times expressions
;; ex.
;; (quotient (times a b) (times c (times d a)))  ->
;;                                           (if (not (zerop a))
;;                                               (quotient (fix b) (times c d))
;;                                            (zero))
;;

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

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

then let inboth be bagint (times-fringe (cadr (x)),

times-fringe (caddr (x)))

in

if listp (inboth) then list ('if,

and-not-zerop-tree (inboth),

                 list ('quotient,

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

                 '(zero))

else x endif endlet else x endif

Theorem: zerop-makes-quotient-zero-bridge ((car (x) = 'times) ∧ (car (y) = 'times) ∧ (¬ eval$ (t,

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

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

÷ (eval$ (t, cadr (y), a) ∗ eval$ (t, caddr (y), a))) = 0)

Event: Disable zerop-makes-quotient-zero-bridge.

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

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

Event: Disable eval$-quotient-times-tree-bagdiff.

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

; Define the available theory of quotient.  To get the list of events to
; put in the theory, evaluate the following form in NQTHM at  this point
; in the script. This form lists all  lemmas which are globally enabled,
; and which have non-null lemma type.
;
;
; (let ((lemmas (lemmas)))
;   (remove-if-not (function (lambda (x)
;       (and (member x lemmas)
;    (not (assoc x disabled-lemmas))
;    (not (null (nth 2 (get x 'event))))
;    (not (member x (nth 2 (get 'addition 'event))))
;    (not (member x (nth 2 (get 'multiplication 'event))))
;    (not (member x (nth 2 (get 'remainders 'event)))))))
;   chronology))

Event: Let us define the theory quotients to consist of the following events: quotient-noop, quotient-of-non-number, quotient-zero, quotient-add1, equal-quotient-0, quotient-sub1, quotient-plus, quotient-times, quotient-times-instance, quotientdifference1, quotient-lessp-arg1, quotient-difference2, quotient-difference3, quotientremainder-times, quotient-remainder, quotient-remainder-instance, quotient-plus-times-times, quotient-plus-times-times-instance, quotient-quotient, quotient-1-arg2, quotient-1-arg1, quotient-x-x, lessp-quotient, correctness-of-cancel-quotient-times.

;;; exp, log, and gcd

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

else i ∗ exp (i, j − 1) endif Definition: log (base, n) = if base < 2 then 0

elseif n ≃ 0 then 0

else 1 + log (base, n ÷ base) endif

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: remainder-exp (k ≄ 0) → ((exp (n, k) mod n) = 0)

Definition: double-number-induction (i, j ) = if i ≃ 0 then 0

elseif j ≃ 0 then 0

else double-number-induction (i − 1, j − 1) endif

Theorem: remainder-exp-exp (i ≤ j ) → ((exp (a, j ) mod exp (a, i)) = 0)

Theorem: quotient-exp (k ≄ 0) → ((exp (n, k) ÷ n)

= if n ≃ 0 then 0 else exp (n, k − 1) endif)

Theorem: exp-zero (k ≃ 0) → (exp (n, k) = 1)

Theorem: exp-add1 exp (n, 1 + k) = (n ∗ exp (n, k))

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

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

else 0 endif

Theorem: exp-1-arg1 exp (1, k) = 1 Theorem: exp-0-arg2 exp (n, 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: equal-exp-0 (exp (n, k) = 0) = ((n ≃ 0) ∧ (k ≄ 0))

Theorem: equal-exp-1 (exp (n, k) = 1) = if k ≃ 0 then t

else n = 1 endif

Theorem: exp-difference ((c ≤ b) ∧ (a ≄ 0)) → (exp (a, b − c) = (exp (a, b) ÷ exp (a, c)))

Event: Let us define the theory exponentiation to consist of the following events: equal-exp-0, equal-exp-1, exp-exp, exp-add1, exp-times, exp-1-arg1, exp-zero, exp-0-arg2, exp-0-arg1, exp-difference, exp-plus, quotient-exp, remainderexp-exp, remainder-exp.

Theorem: equal-log-0 (log (base, n) = 0) = ((base < 2) ∨ (n ≃ 0))

Theorem: log-0 (n ≃ 0) → (log (base, n) = 0)

Theorem: log-1 (1 < base) → (log (base, 1) = 1)

Definition: double-log-induction (base, a, b) = if base < 2 then 0

elseif a ≃ 0 then 0 elseif b ≃ 0 then 0 else double-log-induction (base, a ÷ base, b ÷ base) endif

Theorem: leq-log-log (n ≤ m) → (log (c, n) ≤ log (c, m))

Theorem: log-quotient (1 < c) → (log (c, n ÷ c) = (log (c, n) − 1))

Theorem: log-quotient-times-proof (1 < c) → (log (c, n ÷ (c ∗ m)) = (log (c, n ÷ m) − 1))

Theorem: log-quotient-times (1 < c) → ((log (c, n ÷ (c ∗ m)) = (log (c, n ÷ m) − 1))

∧ (log (c, n ÷ (m ∗ c)) = (log (c, n ÷ m) − 1)))

Theorem: log-quotient-exp (1 < c) → (log (c, n ÷ exp (c, m)) = (log (c, n) − m))

Theorem: log-times-proof ((1 < c) ∧ (n ≄ 0)) → (log (c, c ∗ n) = (1 + log (c, n)))

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

∧ (log (c, n ∗ c) = (1 + log (c, n))))

Theorem: log-times-exp-proof ((1 < c) ∧ (n ≄ 0)) → (log (c, n ∗ exp (c, m)) = (log (c, n) + m))

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

∧ (log (c, exp (c, m) ∗ n) = (log (c, n) + m)))

Theorem: log-exp (1 < c) → (log (c, exp (c, n)) = (1 + n))

Event: Let us define the theory logs to consist of the following events: log-exp, log-times-exp, log-times, log-quotient-exp, log-quotient-times, log-quotient, log-1, log-0, equal-log-0, exp-exp.

Theorem: commutativity-of-gcd gcd (b, a) = gcd (a, b)

Definition: single-number-induction (n) = if n ≃ 0 then 0

else single-number-induction (n − 1) endif

Theorem: gcd-0 (gcd (0, x) = fix (x)) ∧ (gcd (x, 0) = fix (x))

Theorem: gcd-1 (gcd (1, x) = 1) ∧ (gcd (x, 1) = 1)

Theorem: equal-gcd-0 (gcd (a, b) = 0) = ((a ≃ 0) ∧ (b ≃ 0))

Theorem: lessp-gcd (b ≄ 0) → (((b < gcd (a, b)) = f) ∧ ((b < gcd (b, a)) = f))

Theorem: gcd-plus-instance-temp-proof gcd (a, a + b) = gcd (a, b)

Theorem: gcd-plus-instance-temp (gcd (a, a + b) = gcd (a, b)) ∧ (gcd (a, b + a) = gcd (a, b))

Theorem: gcd-plus-proof ((b mod a) = 0) → (gcd (a, b + c) = gcd (a, c))

Theorem: gcd-plus ((b mod a) = 0) → ((gcd (a, b + c) = gcd (a, c))

∧ (gcd (a, c + b) = gcd (a, c)) ∧ (gcd (b + c, a) = gcd (a, c)) ∧ (gcd (c + b, a) = gcd (a, c)))

Theorem: gcd-plus-instance (gcd (a, a + b) = gcd (a, b)) ∧ (gcd (a, b + a) = gcd (a, b))

Theorem: remainder-gcd ((a mod gcd (a, b)) = 0) ∧ ((b mod gcd (a, b)) = 0)

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

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

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

Theorem: common-divisor-divides-gcd (((x mod z) = 0) ∧ ((y mod z) = 0)) → ((gcd (x, y) mod z) = 0)

; We prove ASSOCIATIVITY-OF-GCD and COMMUTATIVITY2-OF-GCD roughly the same way.
; Use GCD-IS-THE-GREATEST twice to show that each side of the equality is
; less than or equal to the other side.

Theorem: associativity-of-gcd-zero-case ((a ≃ 0) ∨ (b ≃ 0) ∨ (c ≃ 0)) → (gcd (gcd (a, b), c) = gcd (a, gcd (b, c)))

Theorem: associativity-of-gcd gcd (gcd (a, b), c) = gcd (a, gcd (b, c))

Theorem: commutativity2-of-gcd-zero-case ((a ≃ 0) ∨ (b ≃ 0) ∨ (c ≃ 0)) → (gcd (b, gcd (a, c)) = gcd (a, gcd (b, c)))

Theorem: commutativity2-of-gcd gcd (b, gcd (a, c)) = gcd (a, gcd (b, c))

Theorem: gcd-x-x gcd (x, x) = fix (x)

Theorem: gcd-idempotence (gcd (x, gcd (x, y)) = gcd (x, y)) ∧ (gcd (y, gcd (x, y)) = gcd (x, y))

Event: Let us define the theory gcds to consist of the following events: commutativity2of-gcd, associativity-of-gcd, common-divisor-divides-gcd, distributivity-of-times-over-gcd, lessp-gcd, equal-gcd-0, gcd-0, gcd-idempotence, gcd-x-x, remaindergcd, gcd-plus, gcd-plus-instance, gcd-1, commutativity-of-gcd.

Event: Let us define the theory naturals to consist of the following events: addition, multiplication, remainders, quotients, exponentiation, logs, gcds.

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

Index

addition, 10 and-not-zerop-tree, 14, 16, 17, 28 associativity-of-gcd, 34 associativity-of-gcd-zero-case, 34 associativity-of-plus, 2 associativity-of-times, 11

bagdiff, 5, 7–10, 16–18, 28, 29 bagint, 7–10, 16–18, 28 bridge-to-subbagp-implies-plus-t

ree-greatereqp, 5

cadr-eval$-list, 6 cancel-difference-plus, 8 cancel-equal-plus, 6, 7 cancel-equal-times, 17, 19 cancel-equal-times-preserves-ineq

uality, 18 uality-bridge, 18

cancel-lessp-plus, 9, 10 cancel-lessp-times, 16, 17 cancel-quotient-times, 28, 29 common-divisor-divides-gcd, 33 commutativity-of-gcd, 32 commutativity-of-plus, 2 commutativity-of-times, 11 commutativity2-of-gcd, 34 commutativity2-of-gcd-zero-case, 34 commutativity2-of-plus, 2 commutativity2-of-times, 11 correctness-of-cancel-difference

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

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

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

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

s, 17 correctness-of-cancel-quotient-ti

mes, 29

delete, 5, 7, 8, 10, 15 diff-diff-arg1, 3 diff-diff-arg2, 3 diff-diff-diff, 4 diff-sub1-arg2, 3 difference-add1-arg2, 8 difference-cancellation, 2 difference-difference-arg1, 9 difference-difference-arg2, 9 difference-elim, 8 difference-leq-arg1, 8 difference-lessp-arg1, 4 difference-plus-cancellation, 3 difference-plus-cancellation-pr

oof, 3 difference-plus-plus-cancellati

on, 3 on-hack, 3 on-proof, 3

difference-sub1-arg2, 9 difference-x-x, 9 distributivity-of-times-over-gc

d, 33

d-proof, 33 double-log-induction, 31 double-number-induction, 30 double-remainder-induction, 21

equal-difference-0, 2 equal-exp-0, 31 equal-exp-1, 31 equal-gcd-0, 33 equal-log-0, 31 equal-plus-0, 1 equal-quotient-0, 24 equal-remainder-difference-0, 22 equal-remainder-plus-0, 20 equal-remainder-plus-0-proof, 20 equal-remainder-plus-remainder, 20 equal-remainder-plus-remainder-p

roof, 20 equal-sub1-0, 11 equal-times-0, 10 equal-times-1, 11 equal-times-arg1, 15 equal-times-bridge, 15 eval$-equal, 14 eval$-equal-times-tree-bagdiff, 18 eval$-if, 15 eval$-lessp, 14 eval$-lessp-times-tree-bagdiff, 17 eval$-or, 14 eval$-plus-tree-append, 5 eval$-quote, 6 eval$-quotient, 15 eval$-quotient-times-tree-bagdi

ff, 28 eval$-times, 14 eval$-times-member, 15 exp, 29–32 exp-0-arg1, 30 exp-0-arg2, 31 exp-1-arg1, 30 exp-add1, 30 exp-difference, 31 exp-exp, 31 exp-plus, 30 exp-times, 31 exp-zero, 30 exponentiation, 31

gcd, 30, 32–34 gcd-0, 32 gcd-1, 33 gcd-idempotence, 34 gcd-is-the-greatest, 33 gcd-plus, 33 gcd-plus-instance, 33 gcd-plus-instance-temp, 33 gcd-plus-instance-temp-proof, 33 gcd-plus-proof, 33 gcd-x-x, 34 gcds, 34 infer-equality-from-not-lessp, 15

leq-log-log, 31 leq-quotient, 27 lessp-1-times, 13 lessp-difference-cancellation, 9 lessp-gcd, 33 lessp-plus-fact, 22 lessp-plus-times-proof, 12 lessp-plus-times1, 13 lessp-plus-times2, 13 lessp-quotient, 27 lessp-remainder, 19 lessp-times-arg1, 15 lessp-times-cancellation-proof, 12 lessp-times-cancellation1, 12 lessp-times1, 12 lessp-times1-proof, 12 lessp-times2, 12 lessp-times2-proof, 12 lessp-times3, 12 lessp-times3-proof1, 12 lessp-times3-proof2, 12 listp-eval$, 6 log, 30–32 log-0, 31 log-1, 31 log-exp, 32 log-quotient, 31 log-quotient-exp, 32 log-quotient-times, 32 log-quotient-times-proof, 32 log-times, 32 log-times-exp, 32 log-times-exp-proof, 32 log-times-proof, 32 logs, 32

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

reqp, 5 multiplication, 19

naturals, 34 numberp-eval$-bridge, 5 numberp-eval$-plus, 4 numberp-eval$-plus-tree, 4 numberp-eval$-times, 14 numberp-eval$-times-tree, 15

or-zerop-tree, 14, 16–18 or-zerop-tree-is-not-zerop-tree, 16

plus-add1-arg1, 2 plus-add1-arg2, 2 plus-cancellation, 1 plus-difference-arg1, 2 plus-difference-arg2, 2 plus-fringe, 4–10 plus-remainder-times-quotient, 19 plus-tree, 4–10 plus-tree-bagdiff, 5 plus-tree-delete, 5 plus-tree-plus-fringe, 6 plus-zero-arg2, 2

quotient-1-arg1, 27 quotient-1-arg1-casesplit, 27 quotient-1-arg2, 27 quotient-add1, 24 quotient-difference1, 26 quotient-difference2, 26 quotient-difference3, 26 quotient-exp, 30 quotient-lessp-arg1, 26 quotient-noop, 24 quotient-of-non-number, 24 quotient-plus, 24 quotient-plus-fact, 26 quotient-plus-proof, 24 quotient-plus-times-times, 27 quotient-plus-times-times-insta

nce, 27 quotient-plus-times-times-proof, 27 quotient-quotient, 27 quotient-remainder, 26 quotient-remainder-instance, 26 quotient-remainder-times, 26 quotient-sub1, 24 quotient-times, 25 quotient-times-instance, 25 quotient-times-instance-temp, 25 quotient-times-instance-temp-pr

oof, 25 quotient-times-proof, 25 quotient-times-times, 25 quotient-times-times-proof, 25 quotient-x-x, 27 quotient-zero, 24 quotients, 29

remainder-1-arg1, 23 remainder-1-arg2, 23 remainder-add1, 20 remainder-difference1, 21 remainder-difference2, 22 remainder-difference3, 22 remainder-equals-its-first-argu

ment, 26 remainder-exp, 30 remainder-exp-exp, 30 remainder-gcd, 33 remainder-noop, 19 remainder-of-non-number, 19 remainder-plus, 20 remainder-plus-fact, 22 remainder-plus-proof, 20 remainder-plus-times-times, 22 remainder-plus-times-times-inst

ance, 23 remainder-plus-times-times-proo

f, 22 remainder-quotient-elim, 20 remainder-remainder, 23 remainder-times-times, 21 remainder-times-times-proof, 21 remainder-times1, 21 remainder-times1-instance, 21 remainder-times1-instance-proof, 21 remainder-times1-proof, 21 remainder-times2, 21 remainder-times2-instance, 21 remainder-times2-proof, 21 remainder-x-x, 23 remainder-zero, 19 remainders, 24

single-number-induction, 32 subbagp, 5, 16–18, 28 subbagp-implies-plus-tree-greate

reqp, 5

times-1-arg1, 12 times-add1, 11 times-distributes-over-differen

ce, 11

ce-proof, 11 times-distributes-over-plus, 11 times-distributes-over-plus-pro

of, 11 times-fringe, 13, 16–18, 28 times-quotient, 12 times-quotient-proof, 11 times-tree, 13, 15–18, 28, 29 times-tree-append, 16 times-tree-of-times-fringe, 16 times-zero, 11 transitivity-of-divides, 23

zerop-makes-equal-true-bridge, 18 zerop-makes-lessp-false-bridge, 17 zerop-makes-quotient-zero-bridge, 28 zerop-makes-times-tree-zero, 16 zerop-makes-times-tree-zero2, 16