#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. 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 Computational Logic, Inc. 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.
|#
; William R. Bevier, Matt Kaufmann, and Matt Wilding

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

;; Jan 91 - some additional facts mostly having to do with GCD
;; added by MMW
;; Oct 90 - modified by MMW to eliminate theories
;; 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)

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

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

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

;(prove-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 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 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 if listp (bagint (times-fringe (cadr (x)), times-fringe (caddr (x)))) then list ('or, or-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)))))))

else x endif 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)

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

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

; ---------- 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 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 ('quotient,

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

                 '(zero))

else x endif 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)

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

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

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

;;; new stuff

Theorem: gcd-zero (x ≃ 0) → ((gcd (x, y) = fix (y)) ∧ (gcd (y, x) = fix (y)))

Theorem: remainder-quotient-gcd-0 ((x mod a) = 0) → ((x mod (x ÷ a)) = 0)

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

;I think this is not important
;(prove-lemma gcd-of-reduce-numbers-helper-helper (rewrite)
;            (equal
;             (remainder a (gcd (quotient a (gcd a b)) (quotient b (gcd a b))))
;             0))
; I believe that the following works just as well as this one because
; of commutativity-of-gcd
;(prove-lemma gcd-of-reduced-numbers-helper (rewrite)
;       (implies
;       (not (zerop a))
;       (and
;        (equal (gcd (quotient a (gcd a b))
;                  (quotient b (gcd a b)))
;             1)
;        (equal (gcd (quotient b (gcd a b))
;                  (quotient a (gcd a b)))
;             1)
;        (equal (gcd (quotient b (gcd b a))
;                  (quotient a (gcd b a)))
;             1)
;        (equal (gcd (quotient a (gcd b a))
;                  (quotient b (gcd b a)))
;             1))))

Theorem: gcd-quotient-gcd (a ≄ 0) → ((gcd (a ÷ gcd (a, b), b ÷ gcd (a, b)) = 1)

∧ (gcd (b ÷ gcd (b, a), a ÷ gcd (b, a)) = 1))

Theorem: lessp-gcd2 ((b < gcd (a, b)) = ((b ≃ 0) ∧ (a ≄ 0))) ∧ ((b < gcd (b, a)) = ((b ≃ 0) ∧ (a ≄ 0)))

Theorem: gcd-times-proof gcd (y, x ∗ y) = fix (y)

Theorem: gcd-times (gcd (y, x ∗ y) = fix (y)) ∧ (gcd (y, y ∗ x) = fix (y))

;; replaced by gcd-zero
;(lemma gcd-zerop (rewrite)
;       (implies
;       (zerop x)

;       (and
;        (equal (gcd x z) (fix z))
;        (equal (gcd z x) (fix z))))
;       ((enable-theory naturals)
;       (enable gcd)))
; (disable gcd-zerop) ; subsumed by gcd-remainder

Theorem: gcd-remainder ((x mod z) = 0) → ((gcd (x, z) = fix (z)) ∧ (gcd (z, x) = fix (z)))

Event: Disable gcd-zero.

; subsumed by gcd-remainder
; no longer needed
;(lemma equal-times-x-x-fact (rewrite)
;       (implies (and (not (equal x 0))
;                    (not (equal y 1)))
;               (and
;                (equal (equal (times x y) x) f)
;                (equal (equal (times y x) x) f)))
;       ((enable-theory naturals)
;       (induct (times y x))))

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

Theorem: equal-x-gcd-x-y (y ∈ N) → (((x = gcd (x, y)) = ((x ∈ N) ∧ ((y mod x) = 0)))

∧ ((x = gcd (y, x)) = ((x ∈ N) ∧ ((y mod x) = 0))))

Theorem: quotient-difference ((x − y) ÷ z) = if (x mod z) < (y mod z) then ((x ÷ z) − (y ÷ z)) − 1

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

Theorem: equal-as-remainder (((x mod y) = 0) ∧ ((y mod x) = 0) ∧ (x ∈ N) ∧ (y ∈ N)) → ((x = y) = t)

Event: Disable equal-as-remainder.

;; add so as to control rewriting equal better

Theorem: equal-gcd-gcd-as-remainder (((gcd (x, y) mod gcd (a, b)) = 0) ∧ ((gcd (a, b) mod gcd (x, y)) = 0)) → ((gcd (a, b) = gcd (x, y)) = t)

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

Theorem: remainder-gcd-arg1 ((gcd (a, b) mod c) = 0) = if (a mod c) = 0

then if (b mod c) = 0 then t

else f endif else f endif

Theorem: remainder-diff1 (((x mod d) = 0) ∧ ((w ∗ x) ≮ z)) → (((((w ∗ x) − z) mod d) = 0) = ((z mod d) = 0))

Theorem: remainder-diff2 (((x mod d) = 0) ∧ ((w ∗ x) ≮ z) ∧ ((((w ∗ x) − z) mod d) = 0)) → ((z mod d) = 0)

Theorem: remainder-gcd-difference-times-hack ((w ∗ x) ≮ z) → ((z mod gcd (x, (w ∗ x) − z)) = 0)

Theorem: gcd-difference1 ((y mod x) = 0) → (gcd (x, y − z)

= if y < z then fix (x) else gcd (x, z) endif)

Theorem: gcd-difference2 ((y mod x) = 0) → (gcd (x, z − y)

= if z < y then fix (x) else gcd (x, z) endif)

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.

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, equal-times-x-x.

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, remainder-quotient-gcd-0, remainder-gcd-0, remaindergcd-arg1, remainder-diff1, remainder-diff2.

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, quotient-difference.

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.

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.

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-idempotence, gcd-x-x, remainder-gcd, gcdplus, gcd-plus-instance, gcd-1, commutativity-of-gcd, gcd-zero, lessp-gcd2, gcdtimes, gcd-remainder, equal-x-gcd-x-y, equal-gcd-gcd-as-remainder, remaindergcd-0-means, gcd-quotient-gcd, gcd-difference1, gcd-difference2.

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, 36 and-not-zerop-tree, 14, 16, 17, 27,

28 associativity-of-gcd, 32 associativity-of-gcd-zero-case, 32 associativity-of-plus, 3 associativity-of-times, 12

bagdiff, 6–10, 17–19, 27, 28 bagint, 7–10, 17–19, 27 bridge-to-subbagp-implies-plus-t

ree-greatereqp, 6

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

uality, 18 uality-bridge, 18

cancel-lessp-plus, 10, 11 cancel-lessp-times, 16, 17 cancel-quotient-times, 27, 28 common-divisor-divides-gcd, 32 commutativity-of-gcd, 31 commutativity-of-plus, 3 commutativity-of-times, 11 commutativity2-of-gcd, 32 commutativity2-of-gcd-zero-case, 32 commutativity2-of-plus, 3 commutativity2-of-times, 11 correctness-of-cancel-difference

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

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

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

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

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

mes, 28

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

oof, 3 difference-plus-plus-cancellati

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

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

d, 32

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

equal-as-remainder, 34 equal-difference-0, 2 equal-exp-0, 29 equal-exp-1, 29 equal-gcd-0, 31 equal-gcd-gcd-as-remainder, 35 equal-log-0, 29 equal-plus-0, 2 equal-quotient-0, 23 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, 11 equal-times-1, 11 equal-times-arg1, 15 equal-times-bridge, 15 equal-times-x-x, 34 equal-x-gcd-x-y, 34 eval$-equal, 15 eval$-equal-times-tree-bagdiff, 18 eval$-if, 15 eval$-lessp, 15 eval$-lessp-times-tree-bagdiff, 17 eval$-or, 14 eval$-plus-tree-append, 6 eval$-quote, 7 eval$-quotient, 15 eval$-quotient-times-tree-bagdi

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

gcd, 28, 31–35 gcd-0, 31 gcd-1, 31 gcd-difference1, 35 gcd-difference2, 35 gcd-idempotence, 32 gcd-is-the-greatest, 32 gcd-plus, 31 gcd-plus-instance, 31 gcd-plus-instance-temp, 31 gcd-plus-instance-temp-proof, 31 gcd-plus-proof, 31 gcd-quotient-gcd, 33 gcd-remainder, 34 gcd-times, 33 gcd-times-proof, 33 gcd-x-x, 32 gcd-zero, 32 gcds, 37

infer-equality-from-not-lessp, 15

leq-log-log, 30 leq-quotient, 26 lessp-1-times, 13 lessp-difference-cancellation, 10 lessp-gcd, 31 lessp-gcd2, 33 lessp-plus-fact, 22 lessp-plus-times-proof, 13 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, 13 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$, 7 log, 28–31 log-0, 30 log-1, 30 log-exp, 31 log-quotient, 30 log-quotient-exp, 30 log-quotient-times, 30 log-quotient-times-proof, 30 log-times, 30 log-times-exp, 30 log-times-exp-proof, 30 log-times-proof, 30 logs, 37

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

reqp, 5 multiplication, 36

naturals, 37 numberp-eval$-bridge, 6 numberp-eval$-plus, 5 numberp-eval$-plus-tree, 5 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, 3 plus-add1-arg2, 3 plus-cancellation, 2 plus-difference-arg1, 3 plus-difference-arg2, 3 plus-fringe, 5–10 plus-remainder-times-quotient, 19 plus-tree, 5–10 plus-tree-bagdiff, 6 plus-tree-delete, 5 plus-tree-plus-fringe, 6 plus-zero-arg2, 3

quotient-1-arg1, 26 quotient-1-arg1-casesplit, 26 quotient-1-arg2, 26 quotient-add1, 23 quotient-difference, 34 quotient-difference1, 25 quotient-difference2, 25 quotient-difference3, 25 quotient-exp, 29 quotient-lessp-arg1, 25 quotient-noop, 23 quotient-of-non-number, 23 quotient-plus, 24 quotient-plus-fact, 26 quotient-plus-proof, 24 quotient-plus-times-times, 26 quotient-plus-times-times-insta

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

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

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

ment, 25 remainder-exp, 28 remainder-exp-exp, 28 remainder-gcd, 31 remainder-gcd-0, 32 remainder-gcd-0-means, 35 remainder-gcd-arg1, 35 remainder-gcd-difference-times-

hack, 35 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, 22 remainder-plus-times-times-proo

f, 22 remainder-quotient-elim, 19 remainder-quotient-gcd-0, 32 remainder-remainder, 23 remainder-times-times, 21 remainder-times-times-proof, 21 remainder-times1, 20 remainder-times1-instance, 21 remainder-times1-instance-proof, 21 remainder-times1-proof, 20 remainder-times2, 21 remainder-times2-instance, 21 remainder-times2-proof, 21 remainder-x-x, 23 remainder-zero, 19 remainders, 36

single-number-induction, 31 subbagp, 6, 16–18, 28 subbagp-implies-plus-tree-greate

reqp, 6

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

ce, 12

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

of, 11 times-fringe, 14, 16–19, 27 times-quotient, 12 times-quotient-proof, 12 times-tree, 14–19, 27, 28 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, 27 zerop-makes-times-tree-zero, 16 zerop-makes-times-tree-zero2, 16