Event: Start with the initial nqthm theory.

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

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

else cons (car (l), delete (x, cdr (l))) endif else l endif

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

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

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

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

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

else nil endif

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

then if x = car (l) then 1 + occurrences (x, cdr (l))

else occurrences (x, cdr (l)) endif else 0 endif

Definition: permutation (a, b) = if listp (a)

then (car (a) ∈ b) ∧ permutation (cdr (a), delete (car (a), b)) else ¬ listp (b) endif

Definition: setp (l) = if listp (l) then (car (l) ∉ cdr (l)) ∧ setp (cdr (l))

else t endif

Definition: subbagp (x, y) = if listp (x) then if car (x) ∈ y then subbagp (cdr (x), delete (car (x), y))

else f endif else t endif

Theorem: listp-delete listp (delete (x, l)) = if listp (l) then (x ≠ car (l)) ∨ listp (cdr (l))

else f endif

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

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

Theorem: equal-occurrences-zero (occurrences (x, l) = 0) = (x ∉ l)

Theorem: occurrences-in-a-set setp (l) → (occurrences (x, l)

= if x ∈ l then 1 else 0 endif)

Theorem: occurrences-cons occurrences (x, cons (y, l)) = if x = y then 1 + occurrences (x, l)

else occurrences (x, l) endif

Theorem: occurrences-delete occurrences (x, delete (y, l)) = if x = y

then if x ∈ l then occurrences (x, l) − 1

else 0 endif else occurrences (x, l) endif

Theorem: occurrences-bagdiff occurrences (x, bagdiff (a, b)) = (occurrences (x, a) − occurrences (x, b))

Theorem: occurrences-bagint occurrences (x, bagint (a, b)) = if occurrences (x, a) < occurrences (x, b) then occurrences (x, a)

else occurrences (x, b) endif

Theorem: member-non-list (¬ listp (l)) → (x ∉ l)

Theorem: member-cons (x ∈ cons (y, l)) = ((x = y) ∨ (x ∈ l))

Theorem: member-delete-implies-membership (x ∈ delete (y, l)) → (x ∈ l)

Theorem: member-delete (x ∈ delete (y, l)) = if x ∈ l

then if x = y then 1 < occurrences (x, l)

else t endif else f endif

Theorem: permutation-implies-membership-equivalence permutation (a, b) → ((x ∈ a) = (x ∈ b))

Theorem: member-bagdiff (x ∈ bagdiff (a, b)) = (occurrences (x, b) < occurrences (x, a))

Theorem: member-bagint (x ∈ bagint (a, b)) = ((x ∈ a) ∧ (x ∈ b))

Theorem: not-permutation (listp (b) ∧ (car (b) ∉ a)) → (¬ permutation (a, b))

Theorem: permutation-right-cons1 (listp (b) ∧ (car (b) ∈ a)) → (permutation (a, b) = permutation (delete (car (b), a), cdr (b)))

Theorem: permutation-right-cons permutation (a, cons (x, b)) = if x ∈ a then permutation (delete (x, a), b)

else f endif

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

Theorem: permutation-reflexivity permutation (l, l)

Theorem: permutation-delete-delete (permutation (a, b) ∧ (x ∈ a) ∧ (x ∈ b)) → permutation (delete (x, a), delete (x, b))

Definition: transitivity-of-permutation-induction (a, b, c) = if listp (a)

then transitivity-of-permutation-induction (cdr (a), delete (car (a), b), delete (car (a), c))

else 0 endif

Theorem: transitivity-of-permutation-base-case ((a ≃ nil) ∧ permutation (a, b) ∧ permutation (b, c)) → permutation (a, c)

Theorem: transitivity-of-permutation-induction-step (listp (a) ∧ ((permutation (cdr (a), delete (car (a), b))

∧ permutation (delete (car (a), b), delete (car (a), c))) → permutation (cdr (a), delete (car (a), c)))

∧ permutation (a, b) ∧ permutation (b, c)) → permutation (a, c)

Theorem: transitivity-of-permutation (permutation (a, b) ∧ permutation (b, c)) → permutation (a, c)

Theorem: setp-delete setp (a) → setp (delete (x, a))

Definition: setp-permutation-induction (a, b) = if listp (a) then setp-permutation-induction (cdr (a), delete (car (a), b))

else 0 endif

Theorem: setp-permutation-base-case (¬ listp (a)) → setp (a)

Theorem: setp-permutation-induction-step (listp (a) ∧ setp (b) ∧ permutation (a, b) ∧ ((setp (delete (car (a), b)) ∧ permutation (cdr (a), delete (car (a), b)))

→ setp (cdr (a)))) → setp (a)

Theorem: setp-permutation (setp (b) ∧ permutation (a, b)) → setp (a)

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

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

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

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

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

Event: Let us define the theory sets-and-bags to consist of the following events: subbagp-bagint2, subbagp-bagint1, subbagp-cdr2, subbagp-cdr1, subbagp-delete, setp-delete, permutation-delete-delete, permutation-reflexivity, commutativityof-permutation, permutation-right-cons, permutation-right-cons1, not-permutation, member-bagint, member-bagdiff, member-delete, member-delete-implies-membership, member-cons, member-non-list, occurrences-bagint, occurrences-bagdiff, occurrencesdelete, occurrences-cons, occurrences-in-a-set, equal-occurrences-zero, deletedelete, delete-non-member, listp-delete.

Theorem: open-plus ((1 + a) + b) = (1 + (a + b))

Theorem: plus-stopper (a ≃ 0) → ((a + b) = fix (b))

Theorem: plus-right-id2 (y ≃ 0) → ((x + y) = fix (x))

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

else 1 + x endif

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

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

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

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

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

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

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

else fix (c) endif

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

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

else fix (a) endif

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

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

else t endif then if if c < d then f

else t endif then (a + c) − (b + d) else a − b endif

elseif if c < d then f

else t endif then c − d else 0 endif

Theorem: plus-difference-difference ((b < a) ∧ (d < c)) → (((a − b) + (c − d)) = ((a + c) − (b + d)))

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

Theorem: difference-leq-arg1 if b < a then f else t endif → ((a − b) = 0)

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

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

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

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

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

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

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

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

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

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

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

Theorem: difference-sub1-arg2 (a − (b − 1)) = if if 1 < b then f

else t endif 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 if b < c then f

else t endif then (a + c) − b else fix (a) endif Theorem: difference-difference-difference (if a < b then f else t endif ∧ if c < d then f

else t endif) → (((a − b) − (c − d)) = ((a + d) − (b + c)))

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

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

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

else list (x) 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cons ('equal,

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

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)

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

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

else fix (a) endif

Theorem: diff-diff-arg2 (c < b) → ((a − (b − c)) = ((a + c) − b))

Theorem: diff-diff-diff-casesplit ((a − b) − (c − d)) = if b < a

then if d < c then (a + d) − (b + c)

else a − b endif else 0 endif

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

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

else 0 endif

Theorem: diff-add1-arg2 (b < a) → ((a − (1 + b)) = ((a − b) − 1))

Theorem: diff-sub1-arg2-casesplit (a − (b − 1)) = if if 1 < b then f

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

Theorem: diff-sub1-arg2 (if b < 1 then f else t endif ∧ if a < b then f

else t endif) → ((a − (b − 1)) = (1 + (a − b)))

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

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

else t endif then a < b else c < b endif

Theorem: lessp-difference ((x ≄ 0) ∧ (y ≄ 0)) → (((x − y) < x) = t)

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)

Event: Enable cancel-lessp-plus; name this event ‘cancel-lessp-plus-off’.

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

Event: Enable cancel-difference-plus; name this event ‘cancel-difference-plus-off’. Event: Enable cancel-equal-plus; name this event ‘cancel-equal-plus-off’. Event: Enable listp-eval$; name this event ‘listp-eval$-off’. Event: Enable eval$-quote; name this event ‘eval$-quote-off’. Event: Enable cadr-eval$-list; name this event ‘cadr-eval$-list-off’. Event: Enable member-implies-numberp; name this event ‘member-implies-numberp-off’. Event: Enable plus-tree-plus-fringe; name this event ‘plus-tree-plus-fringe-off’. Event: Enable eval$-plus-tree-append; name this event ‘eval$-plus-tree-append-off’. Event: Enable bridge-to-subbagp-implies-plus-tree-greatereqp; name this event ‘bridge-to-subbagp-implies-plus-tree-greatereqp-off’. Event: Enable numberp-eval$-bridge; name this event ‘numberp-eval$-bridge-off’. Event: Enable plus-tree-bagdiff; name this event ‘plus-tree-bagdiff-off’. Event: Enable subbagp-implies-plus-tree-greatereqp; name this event ‘subbagpimplies-plus-tree-greatereqp-off’. Event: Enable plus-tree-delete; name this event ‘plus-tree-delete-off’. Event: Enable member-implies-plus-tree-greatereqp; name this event ‘memberimplies-plus-tree-greatereqp-off’. Event: Enable numberp-eval$-plus-tree; name this event ‘numberp-eval$-plus-tree-off’.

Event: Enable numberp-eval$-plus; name this event ‘numberp-eval$-plus-off’. Event: Enable difference-plus-cancellation3; name this event ‘difference-plus-cancellation3-off’. Event: Enable difference-difference-difference; name this event ‘difference-difference-difference-off’. Event: Enable difference-difference-arg2; name this event ‘difference-difference-arg2-off’. Event: Enable difference-difference-arg1; name this event ‘difference-difference-arg1-off’. Event: Enable difference-sub1-arg2; name this event ‘difference-sub1-arg2-off’. Event: Enable difference-add1-plus-cancellation; name this event ‘differenceadd1-plus-cancellation-off’. Event: Enable difference-2; name this event ‘difference-2-off’. Event: Enable difference-1; name this event ‘difference-1-off’. Event: Enable difference-cancellation-1; name this event ‘difference-cancellation-1-off’. Event: Enable difference-cancellation-0; name this event ‘difference-cancellation-0-off’. Event: Enable difference-plus-cancellation2; name this event ‘difference-plus-cancellation2-off’. Event: Enable difference-plus-cancellation1; name this event ‘difference-plus-cancellation1-off’. Event: Enable difference-plus; name this event ‘difference-plus-off’.

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

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

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

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

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

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

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: times-sub1 (b ≄ 0) → ((a ∗ (b − 1)) = ((a ∗ b) − a))

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

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: equal-times-0 ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

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

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 (if b < a then f else t endif ∧ (c ≄ 0)) → (((b ∗ c) < a) = f)

Theorem: lessp-times2 (if b < a then f else t endif ∧ (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)))

Theorem: lessp-times-cancellation2 (((b ∗ a ∗ c) < (a ∗ d)) = ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ ((((a ∗ c) ∗ b) < (a ∗ d))

= ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ (((b ∗ a ∗ c) < (d ∗ a)) = ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ ((((a ∗ c) ∗ b) < (d ∗ a))

= ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ (((b ∗ c ∗ a) < (a ∗ d)) = ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ ((((c ∗ a) ∗ b) < (a ∗ d))

= ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ (((b ∗ c ∗ a) < (d ∗ a)) = ((a ≄ 0) ∧ ((b ∗ c) < d))) ∧ ((((c ∗ a) ∗ b) < (d ∗ a))

= ((a ≄ 0) ∧ ((b ∗ c) < d)))

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

Theorem: equal-sub1-times-0 (((a ∗ b) − 1) = 0) = ((a ≃ 0) ∨ (b ≃ 0) ∨ ((a = 1) ∧ (b = 1)))

Event: Let us define the theory multiplication to consist of the following events: equal-sub1-times-0, lessp-1-times, lessp-plus-times2, lessp-plus-times1, lessp-times-cancellation2, lessp-times-cancellation1, lessp-times3, lessp-times2, lessp-times1, times-1-arg1, equal-times-1, equal-times-0, times-quotient, timesdistributes-over-difference, associativity-of-times, commutativity2-of-times, timesdistributes-over-plus, commutativity-of-times, times-sub1, times-add1, timeszero.

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)

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

Theorem: remainder-sub1 ((a ≄ 0) ∧ (b ≄ 0)) → (((a − 1) mod b)

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

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

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

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)

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

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

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

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

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)

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 if j < i then f else t endif → ((exp (a, j ) mod exp (a, i)) = 0)

Event: Enable lessp-plus-fact; name this event ‘lessp-plus-fact-off’.

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

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

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

Event: Enable equal-remainder-plus-remainder; name this event ‘equal-remainder-plus-remainder-off’.

Event: Enable plus-remainder-times-quotient; name this event ‘plus-remainder-times-quotient-off’.

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

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

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)

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)

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

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

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: quotient-exp (k ≄ 0) → ((exp (n, k) ÷ n)

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

Theorem: leq-quotient (a < b) → if (b ÷ c) < (a ÷ c) then f

else t endif

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

Event: Enable quotient-times-instance-temp; name this event ‘quotient-times-instance-temp-off’.

Event: Enable remainder-equals-its-first-argument; name this event ‘remainderequals-its-first-argument-off’.

Event: Let us define the theory quotients to consist of the following events: lessp-quotient, quotient-x-x, quotient-1-arg1, quotient-1-arg1-casesplit, quotient-1-arg2, leq-quotient, quotient-exp, quotient-quotient, quotient-plus-times-times-instance, quotient-plus-times-times, quotient-plus-times-times, quotient-lessp-arg1, quotient-remainder-instance, quotient-remainder, quotient-remainder-times, quotient-difference3, quotient-difference2, quotient-difference1, quotient-times-times, quotient-times-instance, quotient-times, quotient-plus, quotient-sub1, equalquotient-0, quotient-add1, quotient-zero, quotient-of-non-number, quotient-noop.

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 (if b < c then f else t endif ∧ (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.

Definition: log (base, n) = if base < 2 then 0

elseif n ≃ 0 then 0

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

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 if m < n then f else t endif → if log (c, m) < log (c, n) then f

else t endif

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.

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: 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)) → if gcd (x, y) < z then f

else t endif

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

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 arithmetic to consist of the following events: addition, multiplication, remainders, quotients, exponentiation, logs, gcds.

Definition: integerp (x) = ((x ∈ N) ∨ (negativep (x) ∧ (negative-guts (x) ≄ 0)))

Definition: fix-int (x) = if integerp (x) then x

else 0 endif

Definition: izerop (i) = if integerp (i) then i = 0

else t endif

Definition: ilessp (i, j ) = if negativep (i)

then if negativep (j ) then negative-guts (j ) < negative-guts (i)

else t endif elseif negativep (j ) then f else i < j endif

Definition: ileq (i, j ) = (ilessp (i, j ) ∨ (i = j ))

Definition: iplus (x, y) = if negativep (x)

then if negativep (y)

then if (negative-guts (x) ≃ 0) ∧ (negative-guts (y) ≃ 0) then 0 else − (negative-guts (x) + negative-guts (y)) endif elseif y < negative-guts (x) then − (negative-guts (x) − y) else y − negative-guts (x) endif

elseif negativep (y)

then if x < negative-guts (y) then − (negative-guts (y) − x)

else x − negative-guts (y) endif else x + y endif

Definition: ineg (x) = if negativep (x) then negative-guts (x)

elseif x ≃ 0 then 0

else − x endif

Definition: idifference (x, y) = iplus (x, ineg (y))

Definition: iabs (i) = if negativep (i) then negative-guts (i)

else fix (i) endif Definition: itimes (i, j ) = if negativep (i)

then if negativep (j ) then negative-guts (i) ∗ negative-guts (j )

else fix-int (− (negative-guts (i) ∗ j )) endif elseif negativep (j ) then fix-int (− (i ∗ negative-guts (j ))) else i ∗ j endif

Theorem: integerp-fix-int integerp (fix-int (x))

Theorem: integerp-iplus integerp (iplus (x, y))

Theorem: integerp-idifference integerp (idifference (x, y))

Theorem: integerp-ineg integerp (ineg (x))

Theorem: integerp-iabs integerp (iabs (x))

Theorem: integerp-itimes integerp (itimes (x, y))

Theorem: fix-int-fix-int fix-int (fix-int (x)) = fix-int (x)

Theorem: fix-int-iplus fix-int (iplus (a, b)) = iplus (a, b)

Theorem: fix-int-idifference fix-int (idifference (a, b)) = idifference (a, b)

Theorem: fix-int-ineg fix-int (ineg (x)) = ineg (x)

Theorem: fix-int-iabs fix-int (iabs (x)) = iabs (x)

Theorem: fix-int-itimes fix-int (itimes (x, y)) = itimes (x, y)

Theorem: ineg-id (¬ integerp (x)) → (ineg (x) = 0)

Theorem: ineg-iplus ineg (iplus (a, b)) = iplus (ineg (a), ineg (b))

Theorem: ineg-ineg ineg (ineg (x)) = fix-int (x)

Theorem: ineg-idifference ineg (idifference (a, b)) = iplus (ineg (a), b)

Theorem: ineg-fix-int ineg (fix-int (x)) = ineg (x)

Theorem: iplus-left-id (¬ integerp (x)) → (iplus (x, y) = fix-int (y))

Theorem: iplus-right-id (¬ integerp (y)) → (iplus (x, y) = fix-int (x))

Theorem: iplus-0 iplus (0, x) = fix-int (x)

Theorem: commutativity2-of-iplus iplus (x, iplus (y, z)) = iplus (y, iplus (x, z))

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

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

Theorem: iplus-cancellation (iplus (a, b) = iplus (a, c)) = (fix-int (b) = fix-int (c))

Theorem: iplus-ineg1 iplus (a, ineg (a)) = 0

Theorem: iplus-ineg2 iplus (ineg (a), a) = 0

Theorem: iplus-fix-int1 iplus (fix-int (a), b) = iplus (a, b)

Theorem: iplus-fix-int2 iplus (a, fix-int (b)) = iplus (a, b)

Theorem: iplus-idifference-arg1 iplus (idifference (a, b), c) = idifference (iplus (a, c), b)

Theorem: iplus-idifference-arg2 iplus (a, idifference (b, c)) = idifference (iplus (a, b), c)

Theorem: idifference-x-x idifference (x, x) = 0

Theorem: idifference-iplus-canonicalizer1 idifference (iplus (a, b), c) = iplus (a, idifference (b, c))

Theorem: idifference-iplus (idifference (iplus (x, y), x) = fix-int (y)) ∧ (idifference (iplus (y, x), x) = fix-int (y))

Theorem: idifference-right-id (¬ integerp (b)) → (idifference (a, b) = fix-int (a))

Theorem: idifference-idifference idifference (idifference (x, y), z) = idifference (x, iplus (y, z))

Theorem: idifference-fix-int idifference (a, fix-int (b)) = idifference (a, b)

Theorem: idifference-0 idifference (x, 0) = fix-int (x)

Theorem: idifference-cancellation-1 (idifference (x, y) = idifference (z, y)) = (fix-int (x) = fix-int (z))

Theorem: equal-idifference-0 (0 = idifference (x, y)) = (fix-int (x) = fix-int (y))

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

then append (iplus-fringe (cadr (x)), iplus-fringe (caddr (x))) else list (x) endif

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

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

elseif cddr (l) ≃ nil then list ('iplus, car (l), cadr (l))

else list ('iplus, car (l), iplus-tree (cdr (l))) endif Definition: cancel-iplus (x) = if listp (x) ∧ (car (x) = 'equal)

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

then list ('equal,

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

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

iplus-fringe (caddr (x))))),

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

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

iplus-fringe (caddr (x))))))

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

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

cons ('equal,

cons (iplus-tree (delete (caddr (x),

iplus-fringe (cadr (x)))),

         '('0))),

list ('quote, f))

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

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

list ('equal,
    ''0,

iplus-tree (delete (cadr (x), iplus-fringe (caddr (x))))), list ('quote, f))

else x endif else x endif

Theorem: integerp-eval$-iplus (listp (x) ∧ (car (x) = 'iplus)) → integerp (eval$ (t, x, a))

Theorem: integerp-eval$-iplus-tree integerp (eval$ (t, iplus-tree (l), a))

Theorem: integerp-eval$-bridge (eval$ (t, z, a) = eval$ (t, iplus-tree (x), a)) → integerp (eval$ (t, z, a))

Definition: eval$-iplus-tree-append-induction (a, b, c) = if listp (a) then eval$-iplus-tree-append-induction (cdr (a), b, c)

else nil endif

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

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

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

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

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

= idifference (eval$ (t, iplus-tree (y), a), eval$ (t, iplus-tree (x), a)))

Theorem: not-integerp-implies-not-equal-iplus (¬ integerp (a)) → ((a = iplus (b, c)) = f)

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

Theorem: iplus-idifference-idifference iplus (idifference (a, b), idifference (c, d)) = idifference (iplus (a, c), iplus (b, d))

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

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

         then list ('idifference,

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

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

iplus-fringe (caddr (x))))),

iplus-tree (bagdiff (iplus-fringe (caddr (x)), bagint (iplus-fringe (cadr (x)),

iplus-fringe (caddr (x))))))

elseif listp (cadr (x))

∧ (caadr (x) = 'iplus)

∧ (caddr (x) ∈ iplus-fringe (cadr (x))) then iplus-tree (delete (caddr (x), iplus-fringe (cadr (x)))) elseif listp (caddr (x))

∧ (caaddr (x) = 'iplus)

∧ (cadr (x) ∈ iplus-fringe (caddr (x))) then list ('ineg,

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

else x endif else x endif

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

Theorem: itimes-zero1 izerop (x) → (itimes (x, y) = 0)

Theorem: itimes-zero2 izerop (y) → (itimes (x, y) = 0)

Theorem: itimes-fix-int1 itimes (fix-int (a), b) = itimes (a, b)

Theorem: itimes-fix-int2 itimes (a, fix-int (b)) = itimes (a, b)

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

Theorem: itimes-distributes-over-iplus-proof itimes (x, iplus (y, z)) = iplus (itimes (x, y), itimes (x, z))

Theorem: itimes-distributes-over-iplus (itimes (x, iplus (y, z)) = iplus (itimes (x, y), itimes (x, z))) ∧ (itimes (iplus (x, y), z) = iplus (itimes (x, z), itimes (y, z)))

Theorem: commutativity2-of-itimes itimes (x, itimes (y, z)) = itimes (y, itimes (x, z))

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

Theorem: itimes-distributes-over-idifference-proof itimes (idifference (a, b), c) = idifference (itimes (a, c), itimes (b, c))

Theorem: itimes-distributes-over-idifference (itimes (idifference (a, b), c) = idifference (itimes (a, c), itimes (b, c))) ∧ (itimes (a, idifference (b, c)) = idifference (itimes (a, b), itimes (a, c)))

Theorem: equal-itimes-0 (itimes (x, y) = 0) = (izerop (x) ∨ izerop (y))

Theorem: equal-itimes-1 (itimes (a, b) = 1) = (((a = 1) ∧ (b = 1)) ∨ ((a = -1) ∧ (b = -1)))

Theorem: equal-itimes-minus-1 (itimes (a, b) = -1) = (((a = -1) ∧ (b = 1)) ∨ ((a = 1) ∧ (b = -1)))

Theorem: itimes-1-arg1 itimes (1, x) = fix-int (x)

Theorem: quotient-remainder-uniqueness ((a = (r + (b ∗ q))) ∧ (r < b)) → ((fix (r) = (a mod b)) ∧ (fix (q) = (a ÷ b)))

Definition: iquotient (i, j ) = if izerop (j ) then 0

elseif negativep (i) then if negativep (j )

then if (negative-guts (i) mod negative-guts (j )) = 0 then negative-guts (i) ÷ negative-guts (j ) else 1 + (negative-guts (i) ÷ negative-guts (j )) endif

elseif (negative-guts (i) mod j ) = 0 then fix-int (− (negative-guts (i) ÷ j )) else fix-int (− (1 + (negative-guts (i) ÷ j ))) endif elseif negativep (j ) then fix-int (− (i ÷ negative-guts (j ))) else i ÷ j endif

Definition: iremainder (i, j ) = idifference (fix-int (i), itimes (j , iquotient (i, j )))

Theorem: division-theorem-part1 integerp (i) → (iplus (iremainder (i, j ), itimes (j , iquotient (i, j ))) = i)

Theorem: division-theorem-part2 (integerp (j ) ∧ (j ≠ 0)) → ileq (0, iremainder (i, j ))

Theorem: division-theorem-part3 (integerp (j ) ∧ (j ≠ 0)) → ilessp (iremainder (i, j ), iabs (j ))

Theorem: division-theorem (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (iremainder (i, j ), itimes (j , iquotient (i, j ))) = i)

∧ ileq (0, iremainder (i, j ))

∧ ilessp (iremainder (i, j ), iabs (j )))

Theorem: quotient-difference-lessp-arg2 (((a mod c) = 0) ∧ (b < c)) → (((a − b) ÷ c)

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

Theorem: iquotient-iremainder-uniqueness (integerp (i) ∧ integerp (j ) ∧ integerp (r) ∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q))) ∧ ileq (0, r) ∧ ilessp (r, iabs (j ))) → ((r = iremainder (i, j )) ∧ (q = iquotient (i, j )))

Definition: idiv (i, j ) = if izerop (j ) then 0

elseif negativep (i)

then if negativep (j ) then negative-guts (i) ÷ negative-guts (j ) elseif (negative-guts (i) mod j ) = 0 then fix-int (− (negative-guts (i) ÷ j )) else fix-int (− (1 + (negative-guts (i) ÷ j ))) endif

elseif negativep (j )

then if (i mod negative-guts (j )) = 0 then fix-int (− (i ÷ negative-guts (j ))) else fix-int (− (1 + (i ÷ negative-guts (j )))) endif

else i ÷ j endif

Definition: imod (i, j ) = idifference (fix-int (i), itimes (j , idiv (i, j )))

Theorem: division-theorem-for-truncate-to-neginf-part1 integerp (i) → (iplus (imod (i, j ), itimes (j , idiv (i, j ))) = i)

Theorem: division-theorem-for-truncate-to-neginf-part2 ilessp (0, j ) → (ileq (0, imod (i, j )) ∧ ilessp (imod (i, j ), j ))

Theorem: division-theorem-for-truncate-to-neginf-part3 (integerp (j ) ∧ ilessp (j , 0)) → (ileq (imod (i, j ), 0) ∧ ilessp (j , imod (i, j )))

Theorem: division-theorem-for-truncate-to-neginf (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (imod (i, j ), itimes (j , idiv (i, j ))) = i)

∧ if ilessp (0, j ) then ileq (0, imod (i, j )) ∧ ilessp (imod (i, j ), j ) else ileq (imod (i, j ), 0) ∧ ilessp (j , imod (i, j )) endif)

Theorem: idiv-imod-uniqueness (integerp (i) ∧ integerp (j ) ∧ integerp (r) ∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q))) ∧ if ilessp (0, j ) then ileq (0, r) ∧ ilessp (r, j )

else ileq (r, 0) ∧ ilessp (j , r) endif) → ((r = imod (i, j )) ∧ (q = idiv (i, j )))

Definition: iquo (i, j ) = if izerop (j ) then 0

elseif negativep (i)

then if negativep (j ) then negative-guts (i) ÷ negative-guts (j )

else fix-int (− (negative-guts (i) ÷ j )) endif elseif negativep (j ) then fix-int (− (i ÷ negative-guts (j ))) else i ÷ j endif

Definition: irem (i, j ) = idifference (fix-int (i), itimes (j , iquo (i, j )))

Theorem: division-theorem-for-truncate-to-zero-part1 integerp (i) → (iplus (irem (i, j ), itimes (j , iquo (i, j ))) = i)

Theorem: division-theorem-for-truncate-to-zero-part2 (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0) ∧ ileq (0, i)) → (ileq (0, irem (i, j )) ∧ ilessp (irem (i, j ), iabs (j )))

Theorem: division-theorem-for-truncate-to-zero-part3 (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0) ∧ ilessp (i, 0)) → (ileq (irem (i, j ), 0) ∧ ilessp (ineg (iabs (j )), irem (i, j )))

Theorem: division-theorem-for-truncate-to-zero (integerp (i) ∧ integerp (j ) ∧ (j ≠ 0)) → ((iplus (irem (i, j ), itimes (j , iquo (i, j ))) = i)

∧ if ileq (0, i) then ileq (0, irem (i, j )) ∧ ilessp (irem (i, j ), iabs (j )) else ileq (irem (i, j ), 0)

∧ ilessp (ineg (iabs (j )), irem (i, j )) endif)

Theorem: iquo-irem-uniqueness (integerp (i) ∧ integerp (j ) ∧ integerp (r) ∧ integerp (q) ∧ (j ≠ 0) ∧ (i = iplus (r, itimes (j , q))) ∧ if ileq (0, i) then ileq (0, r) ∧ ilessp (r, iabs (j ))

else ileq (r, 0) ∧ ilessp (ineg (iabs (j )), r) endif) → ((r = irem (i, j )) ∧ (q = iquo (i, j )))

Theorem: integerp-iquotient integerp (iquotient (i, j ))

Theorem: integerp-iremainder integerp (iremainder (i, j ))

Theorem: integerp-idiv integerp (idiv (i, j ))

Theorem: integerp-imod integerp (imod (i, j ))

Theorem: integerp-iquo integerp (iquo (i, j ))

Theorem: integerp-irem integerp (irem (i, j ))

Theorem: iquotient-fix-int1 iquotient (fix-int (i), j ) = iquotient (i, j )

Theorem: iquotient-fix-int2 iquotient (i, fix-int (j )) = iquotient (i, j )

Theorem: iremainder-fix-int1 iremainder (fix-int (i), j ) = iremainder (i, j )

Theorem: iremainder-fix-int2 iremainder (i, fix-int (j )) = iremainder (i, j )

Theorem: idiv-fix-int1 idiv (fix-int (i), j ) = idiv (i, j )

Theorem: idiv-fix-int2 idiv (i, fix-int (j )) = idiv (i, j )

Theorem: imod-fix-int1 imod (fix-int (i), j ) = imod (i, j )

Theorem: imod-fix-int2 imod (i, fix-int (j )) = imod (i, j )

Theorem: iquo-fix-int1 iquo (fix-int (i), j ) = iquo (i, j )

Theorem: iquo-fix-int2 iquo (i, fix-int (j )) = iquo (i, j )

Theorem: irem-fix-int1 irem (fix-int (i), j ) = irem (i, j )

Theorem: irem-fix-int2 irem (i, fix-int (j )) = irem (i, j )

Theorem: fix-int-iquotient fix-int (iquotient (i, j )) = iquotient (i, j )

Theorem: fix-int-iremainder fix-int (iremainder (i, j )) = iremainder (i, j )

Theorem: fix-int-idiv fix-int (idiv (i, j )) = idiv (i, j )

Theorem: fix-int-imod fix-int (imod (i, j )) = imod (i, j )

Theorem: fix-int-iquo fix-int (iquo (i, j )) = iquo (i, j )

Theorem: fix-int-irem fix-int (irem (i, j )) = irem (i, j )

Event: Enable irem; name this event ‘irem-off’. Event: Enable iquo; name this event ‘iquo-off’. Event: Enable imod; name this event ‘imod-off’. Event: Enable idiv; name this event ‘idiv-off’. Event: Enable quotient-difference-lessp-arg2; name this event ‘quotient-difference-lessp-arg2-off’. Event: Enable iremainder; name this event ‘iremainder-off’. Event: Enable iquotient; name this event ‘iquotient-off’. Event: Enable cancel-idifference; name this event ‘cancel-idifference-off’. Event: Enable not-integerp-implies-not-equal-iplus; name this event ‘not-integerp-implies-not-equal-iplus-off’. Event: Enable iplus-tree-bagdiff; name this event ‘iplus-tree-bagdiff-off’. Event: Enable iplus-tree-delete; name this event ‘iplus-tree-delete-off’. Event: Enable iplus-tree-iplus-fringe; name this event ‘iplus-tree-iplus-fringe-off’. Event: Enable eval$-iplus-tree-append; name this event ‘eval$-iplus-tree-append-off’. Event: Enable integerp-eval$-bridge; name this event ‘integerp-eval$-bridge-off’. Event: Enable integerp-eval$-iplus-tree; name this event ‘integerp-eval$-iplus-tree-off’.

Event: Enable integerp-eval$-iplus; name this event ‘integerp-eval$-iplus-off’. Event: Enable cancel-iplus; name this event ‘cancel-iplus-off’. Event: Enable itimes; name this event ‘itimes-off’. Event: Enable iabs; name this event ‘iabs-off’. Event: Enable idifference; name this event ‘idifference-off’. Event: Enable ineg; name this event ‘ineg-off’. Event: Enable iplus; name this event ‘iplus-off’. Event: Enable ileq; name this event ‘ileq-off’. Event: Enable ilessp; name this event ‘ilessp-off’. Event: Enable izerop; name this event ‘izerop-off’. Event: Enable fix-int; name this event ‘fix-int-off’. Event: Enable integerp; name this event ‘integerp-off’. Event: Let us define the theory integers to consist of the following events: fixint-irem, fix-int-iquo, fix-int-imod, fix-int-idiv, fix-int-iremainder, fix-int-iquotient, irem-fix-int2, irem-fix-int1, iquo-fix-int2, iquo-fix-int1, imod-fix-int2, imod-fix-int1, idiv-fix-int2, idiv-fix-int1, iremainder-fix-int2, iremainder-fix-int1, iquotientfix-int2, iquotient-fix-int1, integerp-irem, integerp-iquo, integerp-imod, integerpidiv, integerp-iremainder, integerp-iquotient, itimes-1-arg1, equal-itimes-minus-1, equal-itimes-1, equal-itimes-0, itimes-distributes-over-idifference, itimes-distributes-over-idifference-proof, associativity-of-itimes, commutativity2-of-itimes, itimesdistributes-over-iplus, commutativity-of-itimes, itimes-distributes-over-iplus-proof, itimes-fix-int2, itimes-fix-int1, itimes-zero2, itimes-zero1, correctness-of-cancel-idifference, iplus-idifference-idifference, correctness-of-cancel-iplus, equal-idifference-0, idifference-cancellation-1, idifference-0, idifference-fix-int, idifference-idifference, idifference-right-id, idifference-iplus, idifference-iplus-canonicalizer1, idifferencex-x, iplus-idifference-arg2, iplus-idifference-arg1, iplus-fix-int2, iplus-fix-int1, iplusineg2, iplus-ineg1, iplus-cancellation, associativity-of-iplus, commutativity-of-iplus, commutativity2-of-iplus, iplus-0, iplus-right-id, iplus-left-id, ineg-fix-int, ineg-idifference, ineg-ineg, ineg-iplus, ineg-id, fix-int-itimes, fix-int-iabs, fix-int-ineg, fix-int-idifference, fix-int-iplus, fix-int-fix-int, integerp-itimes, integerp-iabs, integerp-ineg, integerp-idifference, integerp-iplus, integerp-fix-int.

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 list (x) 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)

Theorem: eval$-times eval$ (t, list ('times, x, y), a) = (eval$ (t, x, a) ∗ eval$ (t, y, a))

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

Theorem: eval$-or eval$ (t, list ('or, x, y), a) = (eval$ (t, x, a) ∨ eval$ (t, y, a))

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

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

Theorem: eval$-lessp eval$ (t, list ('lessp, x, y), a) = (eval$ (t, x, a) < eval$ (t, y, a))

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

Theorem: eval$-quotient eval$ (t, list ('quotient, x, y), a) = (eval$ (t, x, a) ÷ eval$ (t, y, a))

Theorem: eval$-quotient2

(car (x) = 'quotient)

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

Theorem: eval$-if eval$ (t, list ('if, x, y, z), a) = if eval$ (t, x, a) then eval$ (t, y, a)

else eval$ (t, z, a) endif

Theorem: eval$-if2 (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)

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

Theorem: bagdiff-delete bagdiff (delete (e, x), y) = delete (e, bagdiff (x, y))

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

Theorem: stupid-hack ((a ∈ N) ∧ (b ∈ N)) → (((a ≮ b) ∧ (b ≮ a)) = (a = b))

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

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

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

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

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

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

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

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

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

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

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)

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

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 cons ('if,

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

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

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

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

Theorem: correctness-of-cancel-quotient-times eval$ (t, x, a) = eval$ (t, cancel-quotient-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)

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

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

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

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

Event: Enable numberp-eval$-times; name this event ‘numberp-eval$-times-off’.

Event: Enable eval$-times; name this event ‘eval$-times-off’.

Event: Enable eval$-times2; name this event ‘eval$-times2-off’.

Event: Enable eval$-or; name this event ‘eval$-or-off’.

Event: Enable eval$-or2; name this event ‘eval$-or2-off’.

Event: Enable eval$-equal; name this event ‘eval$-equal-off’.

Event: Enable eval$-lessp; name this event ‘eval$-lessp-off’.

Event: Enable eval$-lessp2; name this event ‘eval$-lessp2-off’.

Event: Enable eval$-if; name this event ‘eval$-if-off’. Event: Enable eval$-if2; name this event ‘eval$-if2-off’. Event: Enable eval$-quotient; name this event ‘eval$-quotient-off’. Event: Enable eval$-quotient2; name this event ‘eval$-quotient2-off’. Event: Enable numberp-eval$-times-tree; name this event ‘numberp-eval$- times-tree-off’. Event: Enable bagdiff-delete; name this event ‘bagdiff-delete-off’. Event: Enable lessp-times-arg1; name this event ‘lessp-times-arg1-off’. Event: Enable stupid-hack; name this event ‘stupid-hack-off’. Event: Enable equal-times-arg1; name this event ‘equal-times-arg1-off’. Event: Enable equal-times-bridge; name this event ‘equal-times-bridge-off’. Event: Enable eval$-times-member; name this event ‘eval$-times-member-off’. Event: Enable zerop-makes-times-tree-zero; name this event ‘zerop-makes-times-tree-zero-off’. Event: Enable or-zerop-tree-is-not-zerop-tree; name this event ‘or-zerop-tree-is-not-zerop-tree-off’. Event: Enable zerop-makes-times-tree-zero2; name this event ‘zerop-makes-times-tree-zero2-off’. Event: Enable times-tree-append; name this event ‘times-tree-append-off’. Event: Enable times-tree-of-times-fringe; name this event ‘times-tree-of-times-fringe-off’.

Event: Enable eval$-lessp-times-tree-bagdiff; name this event ‘eval$-lessp-times-tree-bagdiff-off’.

Event: Enable zerop-makes-lessp-false-bridge; name this event ‘zerop-makes-lessp-false-bridge-off’.

Event: Enable zerop-makes-quotient-zero-bridge; name this event ‘zerop-makes-quotient-zero-bridge-off’.

Event: Enable eval$-quotient-times-tree-bagdiff; name this event ‘eval$-quotient-times-tree-bagdiff-off’.

Event: Enable zerop-makes-equal-true-bridge; name this event ‘zerop-makes-equal-true-bridge-off’.

Event: Enable eval$-equal-times-tree-bagdiff; name this event ‘eval$-equal-times-tree-bagdiff-off’.

Event: Enable cancel-equal-times-preserves-inequality; name this event ‘cancelequal-times-preserves-inequality-off’.

Event: Enable cancel-equal-times-preserves-inequality-bridge; name this event ‘cancel-equal-times-preserves-inequality-bridge-off’.

Event: Add the shell rational, with recognizer function symbol rational-formp and 2 accessors: numerator, with type restriction (one-of numberp negativep) and default value zero; denominator, with type restriction (one-of numberp) and default value zero.

Event: Let us define the theory rational-defns to consist of the following events: count-rational, numerator-denominator-elim, rational-numerator-denominator, rational-equal, denominator-lesseqp, denominator-lessp, denominator-type-restriction, denominator-nrational-formp, denominator-rational, numerator-lesseqp, numeratorlessp, numerator-type-restriction, numerator-nrational-formp, numerator-rational, denominator, numerator, *1*rational-formp, rational-formp.

Definition: rationalp (x) = (rational-formp (x)

∧ integerp (numerator (x)) ∧ (denominator (x) ≄ 0))

Definition: fix-rational (x) = if rationalp (x) then x

else rational (0, 1) endif

Definition: reduce (r) = if rationalp (r)

then if negativep (numerator (r))

then rational (− (negative-guts (numerator (r))

÷ gcd (negative-guts (numerator (r)), denominator (r))),

denominator (r)

÷ gcd (negative-guts (numerator (r)), denominator (r)))

else rational (numerator (r)

÷ gcd (numerator (r), denominator (r)), denominator (r) ÷ gcd (numerator (r), denominator (r))) endif

else rational (0, 1) endif

Definition: simple-rplus (x, y) = rational (iplus (itimes (numerator (fix-rational (x)),

denominator (fix-rational (y))), itimes (numerator (fix-rational (y)),

denominator (fix-rational (x)))),

itimes (denominator (fix-rational (x)), denominator (fix-rational (y))))

Definition: rplus (x, y) = reduce (simple-rplus (x, y))

Definition: simple-rneg (x) = rational (ineg (numerator (fix-rational (x))),

denominator (fix-rational (x)))

Definition: rneg (x) = reduce (simple-rneg (x))

Definition: rdifference (a, b) = rplus (a, rneg (b))

Definition: simple-rtimes (x, y) = rational (itimes (numerator (fix-rational (x)), numerator (fix-rational (y))),

denominator (fix-rational (x))

∗ denominator (fix-rational (y)))

Definition: rtimes (x, y) = reduce (simple-rtimes (x, y))

Definition: rzerop (x) = ((¬ rationalp (x)) ∨ (numerator (x) = 0))

Definition: simple-rinverse (r) = if rzerop (r) then rational (0, 1)

elseif negativep (numerator (r))

then rational (ineg (denominator (r)), ineg (numerator (r)))

else rational (denominator (r), numerator (r)) endif

Definition: rinverse (r) = reduce (simple-rinverse (r))

Definition: rquotient (x, y) = rtimes (x, rinverse (y))

Definition: simple-rmagnitude (x) = if negativep (numerator (fix-rational (x))) then rneg (fix-rational (x))

else fix-rational (x) endif

Definition: rmagnitude (x) = reduce (simple-rmagnitude (x))

Definition: rlessp (x, y) = ilessp (itimes (numerator (fix-rational (x)), denominator (fix-rational (y))),

itimes (numerator (fix-rational (y)), denominator (fix-rational (x))))

Definition: requal (x, y) = (itimes (numerator (fix-rational (x)), denominator (fix-rational (y)))

= itimes (numerator (fix-rational (y)), denominator (fix-rational (x))))

Theorem: integerp-minus integerp (− x) = (0 < x)

Theorem: fix-int-on-integers integerp (x) → (fix-int (x) = x)

Theorem: itimes-ineg-arg1 itimes (ineg (x), y) = ineg (itimes (x, y))

Theorem: itimes-ineg-arg2 itimes (x, ineg (y)) = ineg (itimes (x, y))

Theorem: integerp-if-negativep-non-zero (negativep (x) ∧ (x ≠ (− 0))) → integerp (x)

Theorem: integerp-if-numberp (x ∈ N) → integerp (x)

Theorem: itimes-negativep-arg1 negativep (x) → (itimes (x, y) = ineg (itimes (negative-guts (x), y)))

Theorem: itimes-negativep-arg2 negativep (y) → (itimes (x, y) = ineg (itimes (x, negative-guts (y))))

Theorem: equal-ineg-ineg (integerp (x) ∧ integerp (y)) → ((ineg (x) = ineg (y)) = (x = y))

Theorem: itimes-is-times ((x ∈ N) ∧ (y ∈ N)) → (itimes (x, y) = (x ∗ y))

Theorem: iplus-is-plus ((x ∈ N) ∧ (y ∈ N)) → (iplus (x, y) = (x + y))

Theorem: rationalp-reduce rationalp (reduce (x))

Theorem: rationalp-rplus rationalp (rplus (x, y))

Theorem: rationalp-fix-rational rationalp (fix-rational (x))

Theorem: rationalp-rtimes rationalp (rtimes (x, y))

Theorem: rationalp-rneg rationalp (rneg (x))

Theorem: rationalp-rdifference rationalp (rdifference (x, y))

Theorem: rationalp-rquotient rationalp (rquotient (x, y))

Theorem: rationalp-rmagnitude rationalp (rmagnitude (x))

Theorem: fix-rational-reduce fix-rational (reduce (x)) = reduce (x)

Theorem: fix-rational-rplus fix-rational (rplus (x, y)) = rplus (x, y)

Theorem: fix-rational-fix-rational fix-rational (fix-rational (x)) = fix-rational (x)

Theorem: fix-rational-rtimes fix-rational (rtimes (x, y)) = rtimes (x, y)

Theorem: fix-rational-rneg fix-rational (rneg (x)) = rneg (x)

Theorem: fix-rational-rdifference fix-rational (rdifference (x, y)) = rdifference (x, y)

Theorem: fix-rational-rquotient fix-rational (rquotient (x, y)) = rquotient (x, y)

Theorem: fix-rational-rmagnitude fix-rational (rmagnitude (x)) = rmagnitude (x)

Theorem: rational-generalization (rationalp (x) → integerp (numerator (x))) ∧ (rationalp (x) → (denominator (x) ∈ N)) ∧ (rationalp (x) → (denominator (x) ≄ 0))

Theorem: gcd-remainder-fact1 ((1 < b) ∧ (gcd (a, b) = 1)) → ((a mod b) ≠ 0)

Theorem: gcd-remainder-fact2 ((1 < b) ∧ (gcd (b, a) = 1)) → ((a mod b) ≠ 0)

Definition: gcd-times1-induct (x, y) = if y ≃ 0 then t

else gcd-times1-induct (x, y − 1) endif

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

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

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

Theorem: divides-each-equality (((a mod b) = 0) ∧ ((b mod a) = 0)) = (fix (a) = fix (b))

Event: Enable idifference-iplus-canonicalizer1; name this event ‘idifferenceiplus-canonicalizer1-off’.

Event: Disable ilessp; name this event ‘ilessp-on’.

Event: Disable idifference; name this event ‘idifference-on’.

Event: Disable iplus; name this event ‘iplus-on’.

Event: Disable itimes; name this event ‘itimes-on’.

Event: Disable ineg; name this event ‘ineg-on’.

Event: Disable integerp; name this event ‘integerp-on’.

Event: Disable fix-int; name this event ‘fix-int-on’.

Event: Disable izerop; name this event ‘izerop-on’.

Definition: gcd-factors (x, y) = if x ≃ 0 then '(0 . 1)

elseif y ≃ 0 then '(1 . 0)

elseif x < y

then cons (idifference (car (gcd-factors (x, y − x)),

cdr (gcd-factors (x, y − x))),

cdr (gcd-factors (x, y − x)))

else cons (car (gcd-factors (x − y, y)),

idifference (cdr (gcd-factors (x − y, y)), car (gcd-factors (x − y, y)))) endif

Theorem: gcd-factors-gives-linear-combination ((x ∈ N) ∧ (y ∈ N)) → (iplus (itimes (car (gcd-factors (x, y)), x),

itimes (cdr (gcd-factors (x, y)), y)) = gcd (x, y))

Event: Disable iremainder; name this event ‘iremainder-on’.

Event: Disable iquotient; name this event ‘iquotient-on’.

Theorem: gcd-factors-gives-linear-combination-rewrite ((x ∈ N) ∧ (y ∈ N)) → (gcd (x, y)

= iplus (itimes (car (gcd-factors (x, y)), x), itimes (cdr (gcd-factors (x, y)), y)))

Theorem: dpr-hack1 itimes (x, iplus (itimes (c, a), itimes (b, q))) = iplus (itimes (c, itimes (a, x)), itimes (b, itimes (q, x)))

Theorem: dpr-hack2 ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (iremainder (itimes (c, y), x) = 0)) → (itimes (iquotient (itimes (c, y), x), x) = itimes (c, y))

Theorem: dpr-hack3 iplus (itimes (c, itimes (a, x)), itimes (b, itimes (c, y))) = iplus (itimes (c, itimes (a, x)), itimes (c, itimes (b, y)))

Theorem: dpr-hack4 iplus (itimes (c, itimes (a, x)), itimes (c, itimes (b, y))) = itimes (c, iplus (itimes (a, x), itimes (b, y)))

Theorem: dpr-hack5 ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (iremainder (itimes (c, y), x) = 0)) → (itimes (x, iplus (itimes (c, a), itimes (b, iquotient (itimes (c, y), x))))

= itimes (c, iplus (itimes (a, x), itimes (b, y))))

Theorem: remainder-0-sufficiency ((x ∈ N) ∧ (c ∈ N) ∧ (itimes (x, p) = c)) → (((c mod x) = 0) = t)

Theorem: divides-product-reduction ((x ∈ N) ∧ (y ∈ N) ∧ (c ∈ N) ∧ (gcd (x, y) = 1) ∧ (((c ∗ y) mod x) = 0)) → ((c mod x) = 0)

Event: Enable remainder-0-sufficiency; name this event ‘remainder-0-sufficiency-off’. Event: Enable dpr-hack1; name this event ‘dpr-hack1-off’. Event: Enable dpr-hack2; name this event ‘dpr-hack2-off’. Event: Enable dpr-hack3; name this event ‘dpr-hack3-off’. Event: Enable dpr-hack4; name this event ‘dpr-hack4-off’. Event: Enable dpr-hack5; name this event ‘dpr-hack5-off’. Event: Enable gcd-factors-gives-linear-combination-rewrite; name this event ‘gcd-factors-gives-linear-combination-rewrite-off’. Event: Enable gcd-factors-gives-linear-combination; name this event ‘gcd-factors-gives-linear-combination-off’. Event: Enable gcd-factors; name this event ‘gcd-factors-off’. Event: Disable idifference-iplus-canonicalizer1; name this event ‘idifferenceiplus-canonicalizer1-on’. Event: Enable ilessp; name this event ‘ilessp-off1’. Event: Enable idifference; name this event ‘idifference-off1’. Event: Enable iplus; name this event ‘iplus-off1’. Event: Enable itimes; name this event ‘itimes-off1’. Event: Enable ineg; name this event ‘ineg-off1’. Event: Enable fix-int; name this event ‘fix-int-off1’.

Event: Enable izerop; name this event ‘izerop-off1’.

Event: Enable iremainder; name this event ‘iremainder-off1’.

Event: Enable iquotient; name this event ‘iquotient-off1’.

Theorem: gcd-remainder-times-fact1-proof (gcd (a, b) = 1) → ((((b ∗ c) mod a) = 0) = ((c mod a) = 0))

Theorem: times-gcd-fact ((gcd (a, c) = 1) ∧ (gcd (b, d) = 1)) → (((a ∗ b) = (c ∗ d))

= ((fix (a) = fix (d)) ∧ (fix (b) = fix (c))))

Theorem: equal-times-times-quotient-arg2 (((b mod e) = 0) ∧ ((d mod e) = 0)) → ((((a ∗ (b ÷ e)) = (c ∗ (d ÷ e)))

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

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

Theorem: quotient-gcd-times-fact (((v ∗ z) = (w ∗ x)) ∧ (0 < w) ∧ (0 < z)) → ((v ÷ gcd (v, w)) = (x ÷ gcd (x, z)))

Theorem: quotient-gcd-times-fact1 (((v ∗ z) = (w ∗ x)) ∧ (0 < w) ∧ (0 < z)) → (((v ÷ gcd (v, w)) = (x ÷ gcd (x, z))) = t)

Theorem: quotient-gcd-times-fact2 (((v ∗ z) = (w ∗ x)) ∧ (0 < w) ∧ (0 < z)) → (((v ÷ gcd (w, v)) = (x ÷ gcd (x, z))) = t)

Theorem: quotient-gcd-times-fact3 (((v ∗ z) = (w ∗ x)) ∧ (0 < w) ∧ (0 < z)) → (((v ÷ gcd (v, w)) = (x ÷ gcd (z, x))) = t)

Theorem: quotient-gcd-times-fact4 (((v ∗ z) = (w ∗ x)) ∧ (0 < w) ∧ (0 < z)) → (((v ÷ gcd (w, v)) = (x ÷ gcd (z, x))) = t)

Theorem: quotient-gcd-times-fact5 (((v ∗ z) = (w ∗ x)) ∧ (0 < v) ∧ (0 < x)) → (((v ÷ gcd (v, w)) = (x ÷ gcd (x, z))) = t)

Theorem: equal-times-gcd-bridge1 (((b ÷ gcd (c, b)) = (d ÷ gcd (a, d))) ∧ ((c ÷ gcd (c, b)) = (a ÷ gcd (a, d)))) → (((a ∗ b) = (c ∗ d)) = t)

Theorem: numberp-if-integerp-and-not-negativep (integerp (x) ∧ (¬ negativep (x))) → (x ∈ N)

Theorem: negativep-if-integerp-and-not-numberp (integerp (x) ∧ (x ∉ N)) → negativep (x)

Event: Enable numberp-if-integerp-and-not-negativep; name this event ‘numberpif-integerp-and-not-negativep-off’.

Event: Enable negativep-if-integerp-and-not-numberp; name this event ‘negativepif-integerp-and-not-numberp-off’.

Theorem: requal-reduce-reduce-equal requal (a, b) = (reduce (a) = reduce (b))

Event: Enable requal-reduce-reduce-equal; name this event ‘requal-reduce-reduce-equal-off’.

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

Theorem: requal-reduce1 requal (reduce (x), y) = requal (x, y)

Theorem: requal-reduce2 requal (x, reduce (y)) = requal (x, y)

Theorem: reduce-reduce reduce (reduce (x)) = reduce (x)

Theorem: rplus-open-up rplus (a, b) = if rationalp (a)

then if rationalp (b) then reduce (rational (iplus (itimes (numerator (a), denominator (b)),

itimes (numerator (b), denominator (a))), itimes (denominator (a), denominator (b))))

else reduce (fix-rational (a)) endif else reduce (fix-rational (b)) endif

Event: Enable rplus-open-up; name this event ‘rplus-open-up-off’.

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

Theorem: rplus-requal-arg1 requal (a, b) → requal (rplus (a, x), rplus (b, x))

Event: Enable rplus-requal-arg1; name this event ‘rplus-requal-arg1-off’.

Theorem: requal-x-x requal (x, x)

Theorem: rplus-reduce-arg1 requal (rplus (reduce (x), y), rplus (x, y))

Theorem: rplus-reduce-arg2 requal (rplus (x, reduce (y)), rplus (x, y))

Theorem: requal-simple-rplus-reduce-arg1 requal (simple-rplus (reduce (x), y), simple-rplus (x, y))

Theorem: requal-simple-rplus-reduce-arg2 requal (simple-rplus (x, reduce (y)), simple-rplus (x, y))

Theorem: reduce-nrationalp (¬ rationalp (x)) → (reduce (x) = rational (0, 1))

Theorem: numberp-numerator-reduce (numerator (reduce (x)) ∈ N) = (numerator (fix-rational (x)) ∈ N)

Theorem: negativep-ineg negativep (ineg (x)) = (0 < x)

Theorem: numberp-ineg (ineg (x) ∈ N) = (0 ≮ x)

Theorem: rational-ineg-numerator-reduce-bridge rational (ineg (numerator (reduce (x))), denominator (reduce (x))) = reduce (rational (ineg (numerator (x)), denominator (x)))

Theorem: reduce-0 reduce (rational (0, x)) = rational (0, 1)

Theorem: simple-rneg-reduce simple-rneg (reduce (x)) = reduce (simple-rneg (x))

Theorem: rneg-reduce rneg (reduce (x)) = rneg (x)

Theorem: simple-rneg-simple-rneg requal (simple-rneg (simple-rneg (x)), x)

Theorem: requal-rneg-rneg requal (rneg (rneg (x)), x)

Theorem: rneg-rneg rneg (rneg (x)) = reduce (x)

Theorem: rationalp-means rationalp (x) → (rational-formp (x)

∧ integerp (numerator (x)) ∧ (0 < denominator (x)))

Theorem: means-rationalp (integerp (n) ∧ (0 < d)) → rationalp (rational (n, d))

Theorem: nrational-rplus-arg1 (¬ rationalp (x)) → (rplus (x, y) = reduce (y))

Theorem: nrational-rplus-arg2 (¬ rationalp (x)) → (rplus (y, x) = reduce (y))

Theorem: nrational-simple-rplus-arg1 (¬ rationalp (x)) → (simple-rplus (x, y) = fix-rational (y))

Theorem: nrational-simple-rplus-arg2 (¬ rationalp (x)) → (simple-rplus (y, x) = fix-rational (y))

Theorem: simple-rplus-fix-rational-arg1 simple-rplus (fix-rational (x), y) = simple-rplus (x, y)

Theorem: simple-rplus-fix-rational-arg2 simple-rplus (x, fix-rational (y)) = simple-rplus (x, y)

Theorem: fix-rational-of-rationalp rationalp (x) → (fix-rational (x) = x)

Theorem: negative-guts-ineg negative-guts (ineg (x)) = if 0 < x then x

else 0 endif

Theorem: rationalp-simple-rplus rationalp (simple-rplus (x, y))

Theorem: fix-rational-simple-rplus fix-rational (simple-rplus (x, y)) = simple-rplus (x, y)

Theorem: requal-associativity-of-simple-rplus requal (simple-rplus (simple-rplus (x, y), z), simple-rplus (x, simple-rplus (y, z)))

Theorem: equal-times-bridge1 (((a ∗ b) = (c ∗ d)) ∧ ((a ∗ x) = (c ∗ y)) ∧ (a ≄ 0)) → (((b ∗ y) = (d ∗ x)) = t)

Theorem: equal-times-bridge2 (((a ∗ b) = (c ∗ d)) ∧ ((a ∗ x) = (c ∗ y)) ∧ (a ≄ 0)) → (((y ∗ b) = (d ∗ x)) = t)

Theorem: equal-times-bridge3 (((a ∗ b) = (c ∗ d)) ∧ ((a ∗ x) = (c ∗ y)) ∧ (a ≄ 0)) → (((b ∗ y) = (x ∗ d)) = t)

Theorem: equal-times-bridge4 (((a ∗ b) = (c ∗ d)) ∧ ((a ∗ x) = (c ∗ y)) ∧ (a ≄ 0)) → (((y ∗ b) = (x ∗ d)) = t)

Theorem: transitivity-of-requal-bridge (requal (a, b) ∧ requal (b, c)) → requal (a, c)

Event: Enable transitivity-of-requal-bridge; name this event ‘transitivity-of-requal-bridge-off’.

Theorem: transitivity-of-requal ((requal (a, b) ∧ requal (b, c)) → requal (a, c)) ∧ ((requal (a, b) ∧ requal (c, b)) → requal (a, c)) ∧ ((requal (b, a) ∧ requal (b, c)) → requal (a, c)) ∧ ((requal (b, a) ∧ requal (c, b)) → requal (a, c))

Theorem: equal-requal-rewrite (requal (b, c) → (requal (a, b) = requal (a, c))) ∧ (requal (b, c) → (requal (a, b) = requal (c, a))) ∧ (requal (b, c) → (requal (b, a) = requal (c, a)))

Event: Enable equal-requal-rewrite; name this event ‘equal-requal-rewrite-off’.

Theorem: requal-simple-rplus-bridge (requal (simple-rplus (reduce (x), y), z) = requal (simple-rplus (x, y), z)) ∧ (requal (simple-rplus (x, reduce (y)), z) = requal (simple-rplus (x, y), z)) ∧ (requal (z, simple-rplus (reduce (x), y)) = requal (z, simple-rplus (x, y))) ∧ (requal (z, simple-rplus (x, reduce (y))) = requal (z, simple-rplus (x, y)))

Theorem: requal-associativity-of-rplus requal (rplus (rplus (x, y), z), rplus (x, rplus (y, z)))

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

Theorem: commutativity2-of-rplus rplus (x, rplus (y, z)) = rplus (y, rplus (x, z))

Theorem: rplus-rdifference-arg1 rplus (rdifference (x, y), z) = rdifference (rplus (x, z), y)

Theorem: rplus-rdifference-arg2 rplus (x, rdifference (y, z)) = rdifference (rplus (x, y), z)

Theorem: reduce-rplus reduce (rplus (x, y)) = rplus (x, y)

Theorem: reduce-rtimes reduce (rtimes (x, y)) = rtimes (x, y)

Theorem: reduce-difference reduce (rdifference (x, y)) = rdifference (x, y)

Theorem: reduce-rquotient reduce (rquotient (x, y)) = rquotient (x, y)

Theorem: reduce-rmagnitude reduce (rmagnitude (x)) = rmagnitude (x)

Theorem: reduce-rneg reduce (rneg (x)) = rneg (x)

Theorem: rplus-reduce-arg1-rewrite rplus (reduce (x), y) = rplus (x, y)

Theorem: rplus-reduce-arg2-rewrite rplus (x, reduce (y)) = rplus (x, y)

Theorem: requal-rneg-simple-rplus requal (simple-rplus (simple-rneg (x), simple-rneg (y)),

simple-rneg (simple-rplus (x, y)))

Theorem: requal-rplus-rneg requal (rneg (rplus (x, y)), rplus (rneg (x), rneg (y)))

Theorem: rneg-rplus rneg (rplus (x, y)) = rplus (rneg (x), rneg (y))

Theorem: rdifference-rdifference-arg1 rdifference (rdifference (x, y), z) = rdifference (x, rplus (y, z))

Theorem: rdifference-rdifference-arg2 rdifference (x, rdifference (y, z)) = rdifference (rplus (x, z), y)

Theorem: rplus-rneg-arg1 rplus (rneg (x), y) = rdifference (y, x)

Theorem: rplus-rneg-arg2 rplus (x, rneg (y)) = rdifference (x, y)

Theorem: commutativity-of-simple-rtimes simple-rtimes (x, y) = simple-rtimes (y, x)

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

Theorem: simple-rtimes-rzerop rzerop (x) → ((numerator (simple-rtimes (x, y)) = 0)

∧ (numerator (simple-rtimes (y, x)) = 0))

Theorem: associativity-of-simple-rtimes-when-not-rzerop ((¬ rzerop (x)) ∧ (¬ rzerop (y)) ∧ (¬ rzerop (z))) → requal (simple-rtimes (simple-rtimes (x, y), z),

simple-rtimes (x, simple-rtimes (y, z)))

Theorem: numerator-zero-rzerop-bridge (numerator (x) = 0) → rzerop (x)

Theorem: associativity-of-simple-rtimes requal (simple-rtimes (simple-rtimes (x, y), z),

simple-rtimes (x, simple-rtimes (y, z)))

Theorem: requal-simple-rtimes-requal-arg1 requal (x, y) → requal (simple-rtimes (x, z), simple-rtimes (y, z))

Theorem: requal-simple-rtimes-requal-arg2 requal (x, y) → requal (simple-rtimes (z, x), simple-rtimes (z, y))

Theorem: requal-simple-rtimes-reduce-arg1 requal (simple-rtimes (reduce (x), y), simple-rtimes (x, y))

Theorem: requal-simple-rtimes-reduce-arg2 requal (simple-rtimes (x, reduce (y)), simple-rtimes (x, y))

Theorem: requal-simple-rtimes-bridge (requal (simple-rtimes (reduce (x), y), z) = requal (simple-rtimes (x, y), z)) ∧ (requal (simple-rtimes (x, reduce (y)), z)

= requal (simple-rtimes (x, y), z)) ∧ (requal (z, simple-rtimes (reduce (x), y))

= requal (z, simple-rtimes (x, y))) ∧ (requal (z, simple-rtimes (x, reduce (y)))

= requal (z, simple-rtimes (x, y)))

Theorem: requal-associativity-of-rtimes requal (rtimes (rtimes (x, y), z), rtimes (x, rtimes (y, z)))

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

Theorem: simple-rplus-rzerop rzerop (x) → (requal (simple-rplus (x, y), y) ∧ requal (simple-rplus (y, x), y))

Theorem: numerator-type (numerator (x) ∈ N) ∨ negativep (numerator (x))

Theorem: rationalp-simple-rtimes rationalp (simple-rtimes (x, y))

Theorem: fix-rational-simple-rtimes fix-rational (simple-rtimes (x, y)) = simple-rtimes (x, y)

Theorem: requal-simple-rtimes-simple-rplus-when-not-rzerop ((¬ rzerop (x)) ∧ (¬ rzerop (y)) ∧ (¬ rzerop (z))) → requal (simple-rtimes (simple-rplus (x, y), z),

simple-rplus (simple-rtimes (x, z), simple-rtimes (y, z)))

Theorem: requal-rzerop-simple-rplus rzerop (x) → (requal (simple-rplus (x, y), fix-rational (y))

∧ requal (simple-rplus (y, x), fix-rational (y)))

Theorem: commutativity-of-simple-rplus simple-rplus (x, y) = simple-rplus (y, x)

Theorem: simple-rplus-bridge (rzerop (x) ∨ rzerop (y) ∨ rzerop (z)) → requal (simple-rtimes (simple-rplus (x, y), z),

simple-rplus (simple-rtimes (x, z), simple-rtimes (y, z)))

Theorem: requal-simple-rtimes-simple-rplus-arg1 requal (simple-rtimes (simple-rplus (x, y), z),

simple-rplus (simple-rtimes (x, z), simple-rtimes (y, z)))

Theorem: requal-rtimes-rplus-bridge requal (rtimes (rplus (x, y), z), rplus (rtimes (x, z), rtimes (y, z)))

Theorem: rtimes-rplus-arg1 rtimes (rplus (x, y), z) = rplus (rtimes (x, z), rtimes (y, z))

Theorem: rtimes-rplus-arg2 rtimes (x, rplus (y, z)) = rplus (rtimes (x, y), rtimes (x, z))

Theorem: requal-simple-rtimes-simple-rneg requal (simple-rtimes (simple-rneg (x), y), simple-rneg (simple-rtimes (x, y)))

Theorem: requal-rtimes-rneg requal (rtimes (rneg (x), y), rneg (rtimes (x, y)))

Theorem: rtimes-rneg-arg1 rtimes (rneg (x), y) = rneg (rtimes (x, y))

Theorem: rtimes-rneg-arg2 rtimes (x, rneg (y)) = rneg (rtimes (x, y))

Theorem: rtimes-rdifference-arg1 rtimes (rdifference (x, y), z) = rdifference (rtimes (x, z), rtimes (y, z))

Theorem: rtimes-rdifference-arg2 rtimes (x, rdifference (y, z)) = rdifference (rtimes (x, y), rtimes (x, z))

Theorem: rneg-rdifference rneg (rdifference (x, y)) = rdifference (y, x)

Theorem: rdifference-rneg-arg2 rdifference (x, rneg (y)) = rplus (x, y)

Event: Enable rdifference-rneg-arg2; name this event ‘rdifference-rneg-arg2-off’. Event: Enable rneg-rdifference; name this event ‘rneg-rdifference-off’. Event: Enable rtimes-rdifference-arg2; name this event ‘rtimes-rdifference-arg2-off’. Event: Enable rtimes-rdifference-arg1; name this event ‘rtimes-rdifference-arg1-off’. Event: Enable rtimes-rneg-arg2; name this event ‘rtimes-rneg-arg2-off’. Event: Enable rtimes-rneg-arg1; name this event ‘rtimes-rneg-arg1-off’. Event: Enable requal-rtimes-rneg; name this event ‘requal-rtimes-rneg-off’. Event: Enable requal-simple-rtimes-simple-rneg; name this event ‘requal-simple-rtimes-simple-rneg-off’. Event: Enable rtimes-rplus-arg2; name this event ‘rtimes-rplus-arg2-off’. Event: Enable rtimes-rplus-arg1; name this event ‘rtimes-rplus-arg1-off’. Event: Enable requal-rtimes-rplus-bridge; name this event ‘requal-rtimes-rplus-bridge-off’. Event: Enable requal-simple-rtimes-simple-rplus-arg1; name this event ‘requalsimple-rtimes-simple-rplus-arg1-off’. Event: Enable simple-rplus-bridge; name this event ‘simple-rplus-bridge-off’. Event: Enable commutativity-of-simple-rplus; name this event ‘commutativityof-simple-rplus-off’. Event: Enable requal-rzerop-simple-rplus; name this event ‘requal-rzerop-simple-rplus-off’.

Event: Enable requal-simple-rtimes-simple-rplus-when-not-rzerop; name this event ‘requal-simple-rtimes-simple-rplus-when-not-rzerop-off’. Event: Enable fix-rational-simple-rtimes; name this event ‘fix-rational-simple-rtimes-off’. Event: Enable rationalp-simple-rtimes; name this event ‘rationalp-simple-rtimes-off’. Event: Enable numerator-type; name this event ‘numerator-type-off’. Event: Enable simple-rplus-rzerop; name this event ‘simple-rplus-rzerop-off’. Event: Enable associativity-of-rtimes; name this event ‘associativity-of-rtimes-off’. Event: Enable requal-associativity-of-rtimes; name this event ‘requal-associativity-of-rtimes-off’. Event: Enable requal-simple-rtimes-bridge; name this event ‘requal-simple-rtimes-bridge-off’. Event: Enable requal-simple-rtimes-reduce-arg2; name this event ‘requal-simple-rtimes-reduce-arg2-off’. Event: Enable requal-simple-rtimes-reduce-arg1; name this event ‘requal-simple-rtimes-reduce-arg1-off’. Event: Enable requal-simple-rtimes-requal-arg2; name this event ‘requal-simple-rtimes-requal-arg2-off’. Event: Enable requal-simple-rtimes-requal-arg1; name this event ‘requal-simple-rtimes-requal-arg1-off’. Event: Enable associativity-of-simple-rtimes; name this event ‘associativityof-simple-rtimes-off’.

Event: Enable numerator-zero-rzerop-bridge; name this event ‘numeratorzero-rzerop-bridge-off’. Event: Enable associativity-of-simple-rtimes-when-not-rzerop; name this event ‘associativity-of-simple-rtimes-when-not-rzerop-off’. Event: Enable simple-rtimes-rzerop; name this event ‘simple-rtimes-rzerop-off’. Event: Enable rzerop; name this event ‘rzerop-off’. Event: Enable commutativity-of-rtimes; name this event ‘commutativity-of-rtimes-off’. Event: Enable commutativity-of-simple-rtimes; name this event ‘commutativityof-simple-rtimes-off’. Event: Enable rplus-rneg-arg2; name this event ‘rplus-rneg-arg2-off’. Event: Enable rplus-rneg-arg1; name this event ‘rplus-rneg-arg1-off’. Event: Enable rdifference-rdifference-arg2; name this event ‘rdifference-rdifference-arg2-off’. Event: Enable rdifference-rdifference-arg1; name this event ‘rdifference-rdifference-arg1-off’. Event: Enable rneg-rplus; name this event ‘rneg-rplus-off’. Event: Enable requal-rplus-rneg; name this event ‘requal-rplus-rneg-off’. Event: Enable requal-rneg-simple-rplus; name this event ‘requal-rneg-simple-rplus-off’. Event: Enable rplus-reduce-arg2-rewrite; name this event ‘rplus-reduce-arg2-rewrite-off’.

Event: Enable rplus-reduce-arg1-rewrite; name this event ‘rplus-reduce-arg1-rewrite-off’. Event: Enable reduce-rneg; name this event ‘reduce-rneg-off’. Event: Enable reduce-rmagnitude; name this event ‘reduce-rmagnitude-off’. Event: Enable reduce-rquotient; name this event ‘reduce-rquotient-off’. Event: Enable reduce-difference; name this event ‘reduce-difference-off’. Event: Enable reduce-rtimes; name this event ‘reduce-rtimes-off’. Event: Enable reduce-rplus; name this event ‘reduce-rplus-off’. Event: Enable rplus-rdifference-arg2; name this event ‘rplus-rdifference-arg2-off’. Event: Enable rplus-rdifference-arg1; name this event ‘rplus-rdifference-arg1-off’. Event: Enable commutativity2-of-rplus; name this event ‘commutativity2-of-rplus-off’. Event: Enable associativity-of-rplus; name this event ‘associativity-of-rplus-off’. Event: Enable requal-associativity-of-rplus; name this event ‘requal-associativity-of-rplus-off’. Event: Enable requal-simple-rplus-bridge; name this event ‘requal-simple-rplus-bridge-off’. Event: Enable equal-requal-rewrite; name this event ‘equal-requal-rewrite-off1’. Event: Enable transitivity-of-requal; name this event ‘transitivity-of-requal-off’. Event: Enable transitivity-of-requal-bridge; name this event ‘transitivity-of-requal-bridge-off1’. Event: Enable equal-times-bridge4; name this event ‘equal-times-bridge4-off’. Event: Enable equal-times-bridge3; name this event ‘equal-times-bridge3-off’. Event: Enable equal-times-bridge2; name this event ‘equal-times-bridge2-off’. Event: Enable equal-times-bridge1; name this event ‘equal-times-bridge1-off’. Event: Enable requal-associativity-of-simple-rplus; name this event ‘requalassociativity-of-simple-rplus-off’. Event: Enable fix-rational-simple-rplus; name this event ‘fix-rational-simple-rplus-off’. Event: Enable rationalp-simple-rplus; name this event ‘rationalp-simple-rplus-off’. Event: Enable negative-guts-ineg; name this event ‘negative-guts-ineg-off’. Event: Enable fix-rational-of-rationalp; name this event ‘fix-rational-of-rationalp-off’. Event: Enable simple-rplus-fix-rational-arg2; name this event ‘simple-rplus-fix-rational-arg2-off’. Event: Enable simple-rplus-fix-rational-arg1; name this event ‘simple-rplus-fix-rational-arg1-off’. Event: Enable nrational-simple-rplus-arg2; name this event ‘nrational-simple-rplus-arg2-off’. Event: Enable nrational-simple-rplus-arg1; name this event ‘nrational-simple-rplus-arg1-off’. Event: Enable nrational-rplus-arg2; name this event ‘nrational-rplus-arg2-off’. Event: Enable nrational-rplus-arg1; name this event ‘nrational-rplus-arg1-off’. Event: Enable means-rationalp; name this event ‘means-rationalp-off’. Event: Enable rationalp-means; name this event ‘rationalp-means-off’. Event: Enable rneg-rneg; name this event ‘rneg-rneg-off’. Event: Enable requal-rneg-rneg; name this event ‘requal-rneg-rneg-off’. Event: Enable simple-rneg-simple-rneg; name this event ‘simple-rneg-simple-rneg-off’. Event: Enable rneg-reduce; name this event ‘rneg-reduce-off’. Event: Enable simple-rneg-reduce; name this event ‘simple-rneg-reduce-off’. Event: Enable reduce-0; name this event ‘reduce-0-off’. Event: Enable rational-ineg-numerator-reduce-bridge; name this event ‘rationalineg-numerator-reduce-bridge-off’. Event: Enable numberp-ineg; name this event ‘numberp-ineg-off’. Event: Enable negativep-ineg; name this event ‘negativep-ineg-off’. Event: Enable numberp-numerator-reduce; name this event ‘numberp-numerator-reduce-off’. Event: Enable reduce-nrationalp; name this event ‘reduce-nrationalp-off’. Event: Enable requal-simple-rplus-reduce-arg2; name this event ‘requal-simple-rplus-reduce-arg2-off’. Event: Enable requal-simple-rplus-reduce-arg1; name this event ‘requal-simple-rplus-reduce-arg1-off’. Event: Enable rplus-reduce-arg2; name this event ‘rplus-reduce-arg2-off’. Event: Enable rplus-reduce-arg1; name this event ‘rplus-reduce-arg1-off’. Event: Enable requal-x-x; name this event ‘requal-x-x-off’. Event: Enable rplus-requal-arg1; name this event ‘rplus-requal-arg1-off1’. Event: Enable commutativity-of-rplus; name this event ‘commutativity-of-rplus-off’. Event: Enable rplus-open-up; name this event ‘rplus-open-up-off1’. Event: Enable reduce-reduce; name this event ‘reduce-reduce-off’. Event: Enable requal-reduce2; name this event ‘requal-reduce2-off’. Event: Enable requal-reduce1; name this event ‘requal-reduce1-off’. Event: Enable commutativity-of-requal; name this event ‘commutativity-of-requal-off’. Event: Enable requal-reduce-reduce-equal; name this event ‘requal-reduce-reduce-equal-off1’. Event: Enable negativep-if-integerp-and-not-numberp; name this event ‘negativepif-integerp-and-not-numberp-off1’. Event: Enable numberp-if-integerp-and-not-negativep; name this event ‘numberpif-integerp-and-not-negativep-off1’.

Event: Enable equal-times-gcd-bridge1; name this event ‘equal-times-gcd-bridge1-off’. Event: Enable quotient-gcd-times-fact5; name this event ‘quotient-gcd-times-fact5-off’. Event: Enable quotient-gcd-times-fact4; name this event ‘quotient-gcd-times-fact4-off’. Event: Enable quotient-gcd-times-fact3; name this event ‘quotient-gcd-times-fact3-off’. Event: Enable quotient-gcd-times-fact2; name this event ‘quotient-gcd-times-fact2-off’. Event: Enable quotient-gcd-times-fact1; name this event ‘quotient-gcd-times-fact1-off’. Event: Enable quotient-gcd-times-fact; name this event ‘quotient-gcd-times-fact-off’. Event: Enable equal-times-times-quotient-arg2; name this event ‘equal-times-times-quotient-arg2-off’. Event: Enable times-gcd-fact; name this event ‘times-gcd-fact-off’. Event: Enable gcd-remainder-times-fact1-proof; name this event ‘gcd-remainder-times-fact1-proof-off’. Event: Enable divides-product-reduction; name this event ‘divides-product-reduction-off’. Event: Enable remainder-0-sufficiency; name this event ‘remainder-0-sufficiency-off1’. Event: Enable dpr-hack5; name this event ‘dpr-hack5-off1’.

Event: Enable dpr-hack4; name this event ‘dpr-hack4-off1’. Event: Enable dpr-hack3; name this event ‘dpr-hack3-off1’. Event: Enable dpr-hack2; name this event ‘dpr-hack2-off1’. Event: Enable dpr-hack1; name this event ‘dpr-hack1-off1’. Event: Enable gcd-factors-gives-linear-combination-rewrite; name this event ‘gcd-factors-gives-linear-combination-rewrite-off1’. Event: Enable gcd-factors-gives-linear-combination; name this event ‘gcd-factors-gives-linear-combination-off1’. Event: Enable gcd-factors; name this event ‘gcd-factors-off1’. Event: Enable divides-each-equality; name this event ‘divides-each-equality-off’. Event: Enable gcd-quotient-quotient; name this event ‘gcd-quotient-quotient-off’. Event: Enable gcd-times2; name this event ‘gcd-times2-off’. Event: Enable gcd-times1; name this event ‘gcd-times1-off’. Event: Enable gcd-times1-induct; name this event ‘gcd-times1-induct-off’. Event: Enable gcd-remainder-fact2; name this event ‘gcd-remainder-fact2-off’. Event: Enable gcd-remainder-fact1; name this event ‘gcd-remainder-fact1-off’. Event: Enable rational-generalization; name this event ‘rational-generalization-off’. Event: Enable fix-rational-rmagnitude; name this event ‘fix-rational-rmagnitude-off’. Event: Enable fix-rational-rquotient; name this event ‘fix-rational-rquotient-off’. Event: Enable fix-rational-rdifference; name this event ‘fix-rational-rdifference-off’. Event: Enable fix-rational-rneg; name this event ‘fix-rational-rneg-off’. Event: Enable fix-rational-rtimes; name this event ‘fix-rational-rtimes-off’. Event: Enable fix-rational-fix-rational; name this event ‘fix-rational-fix-rational-off’. Event: Enable fix-rational-rplus; name this event ‘fix-rational-rplus-off’. Event: Enable fix-rational-reduce; name this event ‘fix-rational-reduce-off’. Event: Enable rationalp-rmagnitude; name this event ‘rationalp-rmagnitude-off’. Event: Enable rationalp-rquotient; name this event ‘rationalp-rquotient-off’. Event: Enable rationalp-rdifference; name this event ‘rationalp-rdifference-off’. Event: Enable rationalp-rneg; name this event ‘rationalp-rneg-off’. Event: Enable rationalp-rtimes; name this event ‘rationalp-rtimes-off’. Event: Enable rationalp-fix-rational; name this event ‘rationalp-fix-rational-off’. Event: Enable rationalp-rplus; name this event ‘rationalp-rplus-off’. Event: Enable rationalp-reduce; name this event ‘rationalp-reduce-off’.

Event: Enable iplus-is-plus; name this event ‘iplus-is-plus-off’. Event: Enable itimes-is-times; name this event ‘itimes-is-times-off’. Event: Enable equal-ineg-ineg; name this event ‘equal-ineg-ineg-off’. Event: Enable itimes-negativep-arg2; name this event ‘itimes-negativep-arg2-off’. Event: Enable itimes-negativep-arg1; name this event ‘itimes-negativep-arg1-off’. Event: Enable integerp-if-numberp; name this event ‘integerp-if-numberp-off’. Event: Enable integerp-if-negativep-non-zero; name this event ‘integerp-if-negativep-non-zero-off’. Event: Enable itimes-ineg-arg2; name this event ‘itimes-ineg-arg2-off’. Event: Enable itimes-ineg-arg1; name this event ‘itimes-ineg-arg1-off’. Event: Enable fix-int-on-integers; name this event ‘fix-int-on-integers-off’. Event: Enable integerp-minus; name this event ‘integerp-minus-off’. Event: Enable requal; name this event ‘requal-off’. Event: Enable rlessp; name this event ‘rlessp-off’. Event: Enable rmagnitude; name this event ‘rmagnitude-off’. Event: Enable simple-rmagnitude; name this event ‘simple-rmagnitude-off’. Event: Enable rquotient; name this event ‘rquotient-off’. Event: Enable rtimes; name this event ‘rtimes-off’.

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

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

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

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

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

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

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

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

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

Event: Let us define the theory r1 to consist of the following events: rdifferencerneg-arg2, rneg-rdifference, rtimes-rdifference-arg2, rtimes-rdifference-arg1, rtimesrneg-arg2, rtimes-rneg-arg1, rtimes-rplus-arg2, rtimes-rplus-arg1, associativityof-rtimes, rzerop, commutativity-of-rtimes, rplus-rneg-arg2, rplus-rneg-arg1, rdifferencerdifference-arg2, rdifference-rdifference-arg1, rneg-rplus, rplus-reduce-arg2-rewrite, rplus-reduce-arg1-rewrite, reduce-rneg, reduce-rmagnitude, reduce-rquotient, reducedifference, reduce-rtimes, reduce-rplus, rplus-rdifference-arg2, rplus-rdifference-arg1, commutativity2-of-rplus, associativity-of-rplus, equal-requal-rewrite, transitivityof-requal, fix-rational-of-rationalp, nrational-rplus-arg2, nrational-rplus-arg1, rationalpmeans, means-rationalp, rneg-rneg, rneg-reduce, reduce-0, numberp-numerator-reduce, reduce-nrationalp, rplus-reduce-arg2, rplus-reduce-arg1, requal-x-x, rplusrequal-arg1, commutativity-of-rplus, reduce-reduce, requal-reduce2, requal-reduce1, commutativity-of-requal, rational-generalization, fix-rational-rmagnitude, fixrational-rquotient, fix-rational-rdifference, fix-rational-rneg, fix-rational-rtimes, fix-rational-fix-rational, fix-rational-rplus, fix-rational-reduce, rationalp-rmagnitude, rationalp-rquotient, rationalp-rdifference, rationalp-rneg, rationalp-rtimes, rationalpfix-rational, rationalp-rplus, rationalp-reduce.

Definition: rplus-tree (x)

= if x ≃ nil then '(rational '0 '1)

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

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

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

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

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

else list (x) endif

Definition: split-by-parity (x) = if listp (x)

then if (caar (x) = 'rneg)

∧ (caadar (x) ≠ 'rneg) ∧ (cddar (x) = nil)

then cons (car (split-by-parity (cdr (x))),

cons (cadar (x), cdr (split-by-parity (cdr (x)))))

else cons (cons (car (x), car (split-by-parity (cdr (x)))), cdr (split-by-parity (cdr (x)))) endif

else '(nil) endif

Definition: make-negs (x) = if listp (x) then cons (list ('rneg, car (x)), make-negs (cdr (x)))

else nil endif

Theorem: rplus-rzerop-bridge ((v ≄ 0) ∧ (z ∈ N)) → (reduce (rational (v ∗ z, v ∗ w)) = reduce (rational (z, w)))

Theorem: rplus-rzerop-bridge2 (v ≄ 0) → (reduce (rational (− (d ∗ v), v ∗ w))

= reduce (rational (− d, w)))

Theorem: rplus-rzerop rzerop (x) → ((rplus (x, y) = reduce (y)) ∧ (rplus (y, x) = reduce (y)))

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

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

Theorem: reduce-eval$-rplus-tree reduce (eval$ (t, rplus-tree (y), a)) = eval$ (t, rplus-tree (y), a)

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

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

Theorem: delete-append delete (x, append (a, b)) = if x ∈ a then append (delete (x, a), b)

else append (a, delete (x, b)) endif

Theorem: member-subbagp ((a ∈ x) ∧ subbagp (x, y)) → (a ∈ y)

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

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

else car (x) endif else 0 endif

Theorem: member-occur (a ∈ x) = (0 < occurrences (a, x))

Theorem: occurrences-delete2 occurrences (a, delete (b, x)) = if a = b then occurrences (a, x) − 1

else occurrences (a, x) endif

Theorem: subbagp-wit-lemma subbagp (x, y) = (occurrences (badguy (x, y), y) ≮ occurrences (badguy (x, y), x))

Theorem: occurrences-append occurrences (a, append (x, y)) = (occurrences (a, x) + occurrences (a, y))

Theorem: subbagp-append subbagp (append (x, y), append (y, x))

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

Event: Enable subbagp-wit-lemma; name this event ‘subbagp-wit-lemma-off’.

Theorem: subbagp-delete-same subbagp (x, y) → subbagp (delete (a, x), delete (a, y))

Theorem: subbagp-delete-same-means ((a ∈ y) ∧ subbagp (delete (a, x), delete (a, y))) → subbagp (x, y)

Theorem: subbagp-delete-car subbagp (x, y) → subbagp (delete (car (y), x), cdr (y))

Theorem: subbagp-delete-car2 subbagp (x, y) → subbagp (cdr (x), delete (car (x), y))

Theorem: subbagp-permutation (subbagp (x, y) ∧ subbagp (y, x)) → permutation (x, y)

Theorem: permutation-a-b permutation (append (a, b), append (b, a))

Theorem: not-subbagp-not-permutation (¬ subbagp (x, y)) → ((¬ permutation (x, y)) ∧ (¬ permutation (y, x)))

Theorem: permutation-as-subbagp-helper permutation (x, y) ↔ (subbagp (x, y) ∧ subbagp (y, x))

Theorem: permutation-as-subbagp permutation (x, y) = (subbagp (x, y) ∧ subbagp (y, x))

Event: Enable permutation-as-subbagp-helper; name this event ‘permutationas-subbagp-helper-off’.

Event: Enable permutation-as-subbagp; name this event ‘permutation-as-subbagp-off’.

Theorem: subbagp-necc subbagp (x, y) → (occurrences (a, y) ≮ occurrences (a, x))

Theorem: subbagp-transitive (subbagp (x, y) ∧ subbagp (y, z)) → subbagp (x, z)

Theorem: not-member-make-negs-fact (x ∉ y) → (delete (list ('rneg, x), make-negs (y)) = make-negs (y))

Theorem: make-negs-delete make-negs (delete (a, x)) = delete (list ('rneg, a), make-negs (x))

Theorem: make-negs-bagdiff make-negs (bagdiff (x, y)) = bagdiff (make-negs (x), make-negs (y))

Theorem: append-bagdiff-arg1 subbagp (a, b) → (append (bagdiff (b, a), c) = bagdiff (append (b, c), a))

Theorem: append-bagdiff-arg2 (bagint (a, c) = nil) → (append (c, bagdiff (b, a)) = bagdiff (append (c, b), a))

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

Theorem: member-rneg-make-negs (list ('rneg, x) ∈ make-negs (y)) = (x ∈ y)

Theorem: subbagp-make-negs subbagp (make-negs (x), make-negs (y)) = subbagp (x, y)

Theorem: rdifference-reduce (rdifference (reduce (x), y) = rdifference (x, y)) ∧ (rdifference (x, reduce (y)) = rdifference (x, y))

Theorem: requal-simple-rplus-x-simple-rneg-x requal (simple-rplus (x, simple-rneg (x)), rational (0, 1))

Theorem: requal-rplus-x-simple-rneg-x requal (rplus (x, simple-rneg (x)), rational (0, 1))

Theorem: rplus-x-rneg-x rplus (x, rneg (x)) = rational (0, 1)

Theorem: rdifference-x-x rdifference (x, x) = rational (0, 1)

Theorem: rdifference-rplus-hack rdifference (rplus (a, b), a) = reduce (b)

Theorem: rdifference-rplus-hack2 rdifference (rplus (b, a), a) = reduce (b)

Theorem: rplus-rdifference-hack (rplus (a, rdifference (b, a)) = reduce (b)) ∧ (rplus (rdifference (b, a), a) = reduce (b))

Theorem: equal-difference-hack1 (a = rdifference (b, c)) → (rplus (c, a) = reduce (b))

Theorem: equal-difference-hack2 (reduce (a) = rdifference (b, c)) → (rplus (c, a) = reduce (b))

Theorem: equal-difference-rewrite (fix (b) = fix (d)) → (((a − b) = (c − d))

= (((b ≮ a) ∧ (b ≮ c)) ∨ (a = c)))

Theorem: equal-difference-rewrite2 (fix (a) = fix (c)) → (((a − b) = (c − d))

= (((b ≮ a) ∧ (d ≮ c)) ∨ (fix (b) = fix (d))))

Theorem: equal-times-bridge5 (((b ∗ a) = (c ∗ d)) ∧ ((x ∗ a) = (c ∗ y)) ∧ (a ≄ 0)) → (((b ∗ y) = (x ∗ d)) = t)

Theorem: equal-plus-difference-rewrite (fix (a) = fix (c)) → ((((a + b) = (c − d)) = ((b ≃ 0) ∧ ((a ≃ 0) ∨ (d ≃ 0))))

∧ (((b + a) = (c − d))

= ((b ≃ 0) ∧ ((a ≃ 0) ∨ (d ≃ 0))))
∧ (((c − d) = (a + b))
= ((b ≃ 0) ∧ ((a ≃ 0) ∨ (d ≃ 0))))
∧ (((c − d) = (b + a))
= ((b ≃ 0) ∧ ((a ≃ 0) ∨ (d ≃ 0)))))

Theorem: lessp-times-bridge1 (((c ∗ v) < (x1 ∗ z1 )) ∧ ((w ∗ x1 ) = (c ∗ d)) ∧ (c ≄ 0) ∧ (d ≄ 0)) → ((v ∗ w) < (d ∗ z1 ))

Theorem: equal-difference ((a = (a − b)) = ((a ∈ N) ∧ ((a ≃ 0) ∨ (b ≃ 0)))) ∧ (((a − b) = a) = ((a ∈ N) ∧ ((a ≃ 0) ∨ (b ≃ 0))))

Theorem: requal-simple-rplus-x-x-rewrite requal (simple-rplus (x, y), simple-rplus (x, z)) = requal (y, z)

Theorem: equal-rplus-x-x-rewrite (rplus (x, y) = rplus (x, z)) = (reduce (y) = reduce (z))

Theorem: equal-rplus-rdifference-hack (rplus (x, y) = rdifference (rplus (x, z), v)) = (reduce (y) = rdifference (z, v))

Theorem: eval$-rplus-tree-delete eval$ (t, rplus-tree (delete (m, x)), a) = if m ∈ x then rdifference (eval$ (t, rplus-tree (x), a), eval$ (t, m, a))

else eval$ (t, rplus-tree (x), a) endif

Theorem: permutation-does-not-effect-rplus permutation (x, y) → (eval$ (t, rplus-tree (x), a) = eval$ (t, rplus-tree (y), a))

Theorem: eval$-rplus-tree-zero eval$ (t, rplus-tree (append (make-negs (x), x)), a) = rational (0, 1)

Theorem: cancel-zero-fact (eval$ (t, rplus-tree (z), a) = rational (0, 1)) → (eval$ (t, rplus-tree (append (x, z)), a) = eval$ (t, rplus-tree (x), a))

Theorem: member-car-x-x (car (x) ∈ x) = listp (x)

Theorem: member-bagdiff-append (e ∈ bagdiff (append (x, z), z)) = (e ∈ x)

Theorem: permutation-transitive (permutation (x, y) ∧ permutation (y, z)) → permutation (x, z)

Definition: last-cdr (x) = if listp (x) then last-cdr (cdr (x))

else x endif

Theorem: bagdiff-x-x bagdiff (x, x) = last-cdr (x)

Theorem: bagdiff-append-arg1 bagdiff (append (z, x), z) = x

Theorem: bagdiff-cons-z-z bagdiff (cons (x, z), z) = cons (x, last-cdr (z))

Theorem: bagdiff-not-listp (¬ listp (x)) → (bagdiff (x, z) = x)

Theorem: bagdiff-car-in (listp (x) ∧ (car (x) ∈ z)) → (bagdiff (x, z) = bagdiff (cdr (x), delete (car (x), z)))

Theorem: last-cdr-delete last-cdr (delete (e, x)) = last-cdr (x)

Theorem: member-subbagp2 (subbagp (x, y) ∧ (e ∈ x)) → (e ∈ y)

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

Theorem: subbagp-bagdiff subbagp (x, y) → subbagp (bagdiff (x, z), bagdiff (y, z))

Theorem: permutation-bagdiff permutation (x, y) → permutation (bagdiff (x, z), bagdiff (y, z))

Theorem: permutation-append-arg1-arg2-bridge permutation (bagdiff (append (x, z), z), bagdiff (append (z, x), z))

Theorem: subbagp-transitive-bridge-helper (subbagp (y, z) ∧ subbagp (z, y)) → (((subbagp (y, x) ↔ subbagp (z, x)) = t)

∧ ((subbagp (x, y) ↔ subbagp (x, z)) = t))

Theorem: subbagp-transitive-bridge (subbagp (y, z) ∧ subbagp (z, y)) → (((subbagp (y, x) = subbagp (z, x)) = t)

∧ ((subbagp (x, y) = subbagp (x, z)) = t))

Theorem: equal-permutation (permutation (y, z) → ((permutation (x, y) = permutation (x, z)) = t)) ∧ (permutation (y, z) → ((permutation (y, x) = permutation (z, x)) = t))

Theorem: permutation-bagdiff-append-helper (permutation (bagdiff (append (z, x), x), y) = permutation (bagdiff (append (x, z), x), y)) ∧ (permutation (y, bagdiff (append (z, x), x))

= permutation (y, bagdiff (append (x, z), x)))

Theorem: permutation-bagdiff-append permutation (x, bagdiff (append (x, z), z))

Theorem: cancel-zero-fact-bridge (subbagp (z, x) ∧ (eval$ (t, rplus-tree (z), a) = rational (0, 1))) → (eval$ (t, rplus-tree (bagdiff (x, z)), a) = eval$ (t, rplus-tree (x), a))

Theorem: rnegs-cancel-list eval$ (t, rplus-tree (append (x, make-negs (x))), a) = rational (0, 1)

Theorem: subbagp-append-simplify1 subbagp (a, x) → subbagp (a, append (x, y))

Theorem: subbagp-permutation-equiv (permutation (x, y) ∧ subbagp (a, x)) → subbagp (a, y)

Theorem: subbagp-append-simplify2 subbagp (a, x) → subbagp (a, append (y, x))

Theorem: subbagp-append-bridge (subbagp (x, b) ∧ subbagp (y, a)) → subbagp (append (x, y), append (b, a))

Theorem: subbagp-append-bridge2 (subbagp (x, b) ∧ subbagp (y, a)) → subbagp (append (x, y), append (a, b))

Theorem: cancelling-from-rplus (subbagp (z, x) ∧ subbagp (z, y) ∧ (bagint (make-negs (z), x) = nil)) → (eval$ (t, rplus-tree (append (bagdiff (x, z), make-negs (bagdiff (y, z)))), a)

= eval$ (t, rplus-tree (append (x, make-negs (y))), a))

Theorem: eval$-rplus-tree-rplus-fringe (car (x) = 'rplus) → (eval$ (t, rplus-tree (rplus-fringe (x)), a) = eval$ (t, x, a))

Theorem: subbagp-x-x subbagp (x, x)

Theorem: rnegs-not-car-split-by-parity ((car (x) = 'rneg) ∧ (caadr (x) ≠ 'rneg) ∧ (cddr (x) = nil)) → (x ∉ car (split-by-parity (y)))

Theorem: permutation-append-split-by-parity-bridge permutation (append (car (split-by-parity (x)),

make-negs (cdr (split-by-parity (x)))), x)

Theorem: member-cdr-split-by-parity (e ∈ cdr (split-by-parity (x))) → (car (e) ≠ 'rneg)

Definition: all-rnegs (x) = if listp (x)

then (caar (x) = 'rneg) ∧ (caadar (x) ≠ 'rneg) ∧ (cddar (x) = nil) ∧ all-rnegs (cdr (x))

else t endif Theorem: all-rnegs-make-negs-bagint-fact (all-rnegs (make-negs (bagint (z, w))) ∧ (v ∈ w)) → all-rnegs (make-negs (bagint (z, delete (v, w))))

Theorem: all-rnegs-make-negs-bagint all-rnegs (make-negs (bagint (car (split-by-parity (x)), cdr (split-by-parity (y)))))

Theorem: bagint-all-rnegs-car-split-by-parity all-rnegs (x) → (bagint (x, car (split-by-parity (y))) = nil)

Theorem: bagint-make-negs-split-by-parity bagint (make-negs (bagint (car (split-by-parity (y)), cdr (split-by-parity (y)))),

car (split-by-parity (y))) = nil

Theorem: commutativity2-of-rtimes rtimes (x, rtimes (y, z)) = rtimes (y, rtimes (x, z))

Event: Enable eval$-rplus-tree-rplus-fringe; name this event ‘eval$-rplus-tree-rplus-fringe-off’.

Event: Enable cancelling-from-rplus; name this event ‘cancelling-from-rplus-off’.

Event: Enable rnegs-cancel-list; name this event ‘rnegs-cancel-list-off’.

Event: Enable cancel-zero-fact-bridge; name this event ‘cancel-zero-fact-bridge-off’.

Event: Enable cancel-zero-fact; name this event ‘cancel-zero-fact-off’.

Event: Enable eval$-rplus-tree-zero; name this event ‘eval$-rplus-tree-zero-off’.

Event: Enable permutation-does-not-effect-rplus; name this event ‘permutationdoes-not-effect-rplus-off’.

Event: Enable eval$-rplus-tree-delete; name this event ‘eval$-rplus-tree-delete-off’.

Event: Enable rplus-eval$-rplus-tree; name this event ‘rplus-eval$-rplus-tree-off’.

Event: Enable reduce-eval$-rplus-tree; name this event ‘reduce-eval$-rplus-tree-off’.

Event: Enable bagint-make-negs-split-by-parity; name this event ‘bagint-make-negs-split-by-parity-off’.

Event: Enable bagint-all-rnegs-car-split-by-parity; name this event ‘bagint-all-rnegs-car-split-by-parity-off’.

Event: Enable all-rnegs-make-negs-bagint; name this event ‘all-rnegs-make-negs-bagint-off’.

Event: Enable all-rnegs-make-negs-bagint-fact; name this event ‘all-rnegs-make-negs-bagint-fact-off’.

Event: Enable member-cdr-split-by-parity; name this event ‘member-cdr-split-by-parity-off’.

Event: Enable permutation-append-split-by-parity-bridge; name this event ‘permutation-append-split-by-parity-bridge-off’.

Event: Enable rnegs-not-car-split-by-parity; name this event ‘rnegs-not-car-split-by-parity-off’.

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

Event: Enable subbagp-append-bridge2; name this event ‘subbagp-append-bridge2-off’.

Event: Enable subbagp-append-bridge; name this event ‘subbagp-append-bridge-off’.

Event: Enable subbagp-append-simplify2; name this event ‘subbagp-append-simplify2-off’.

Event: Enable subbagp-permutation-equiv; name this event ‘subbagp-permutation-equiv-off’.

Event: Enable subbagp-append-simplify1; name this event ‘subbagp-append-simplify1-off’. Event: Enable permutation-bagdiff-append; name this event ‘permutationbagdiff-append-off’. Event: Enable permutation-bagdiff-append-helper; name this event ‘permutationbagdiff-append-helper-off’. Event: Enable equal-permutation; name this event ‘equal-permutation-off’. Event: Enable subbagp-transitive-bridge; name this event ‘subbagp-transitive-bridge-off’. Event: Enable subbagp-transitive-bridge-helper; name this event ‘subbagptransitive-bridge-helper-off’. Event: Enable permutation-append-arg1-arg2-bridge; name this event ‘permutationappend-arg1-arg2-bridge-off’. Event: Enable permutation-bagdiff; name this event ‘permutation-bagdiff-off’. Event: Enable subbagp-bagdiff; name this event ‘subbagp-bagdiff-off’. Event: Enable member-subbagp-delete; name this event ‘member-subbagp-delete-off’. Event: Enable member-subbagp2; name this event ‘member-subbagp2-off’. Event: Enable last-cdr-delete; name this event ‘last-cdr-delete-off’. Event: Enable bagdiff-car-in; name this event ‘bagdiff-car-in-off’. Event: Enable bagdiff-not-listp; name this event ‘bagdiff-not-listp-off’. Event: Enable bagdiff-cons-z-z; name this event ‘bagdiff-cons-z-z-off’.

Event: Enable bagdiff-append-arg1; name this event ‘bagdiff-append-arg1-off’. Event: Enable bagdiff-x-x; name this event ‘bagdiff-x-x-off’. Event: Enable permutation-transitive; name this event ‘permutation-transitive-off’. Event: Enable member-bagdiff-append; name this event ‘member-bagdiff-append-off’. Event: Enable member-car-x-x; name this event ‘member-car-x-x-off’. Event: Enable equal-rplus-rdifference-hack; name this event ‘equal-rplus-rdifference-hack-off’. Event: Enable equal-rplus-x-x-rewrite; name this event ‘equal-rplus-x-x-rewrite-off’. Event: Enable requal-simple-rplus-x-x-rewrite; name this event ‘requal-simple-rplus-x-x-rewrite-off’. Event: Enable equal-difference; name this event ‘equal-difference-off’. Event: Enable lessp-times-bridge1; name this event ‘lessp-times-bridge1-off’. Event: Enable equal-plus-difference-rewrite; name this event ‘equal-plus-difference-rewrite-off’. Event: Enable equal-times-bridge5; name this event ‘equal-times-bridge5-off’. Event: Enable equal-difference-rewrite2; name this event ‘equal-difference-rewrite2-off’. Event: Enable equal-difference-rewrite; name this event ‘equal-difference-rewrite-off’. Event: Enable equal-difference-hack2; name this event ‘equal-difference-hack2-off’. Event: Enable equal-difference-hack1; name this event ‘equal-difference-hack1-off’. Event: Enable rplus-rdifference-hack; name this event ‘rplus-rdifference-hack-off’. Event: Enable rdifference-rplus-hack2; name this event ‘rdifference-rplus-hack2-off’. Event: Enable rdifference-rplus-hack; name this event ‘rdifference-rplus-hack-off’. Event: Enable rdifference-x-x; name this event ‘rdifference-x-x-off’. Event: Enable rplus-x-rneg-x; name this event ‘rplus-x-rneg-x-off’. Event: Enable requal-rplus-x-simple-rneg-x; name this event ‘requal-rplus-x-simple-rneg-x-off’. Event: Enable requal-simple-rplus-x-simple-rneg-x; name this event ‘requalsimple-rplus-x-simple-rneg-x-off’. Event: Enable rdifference-reduce; name this event ‘rdifference-reduce-off’. Event: Enable subbagp-make-negs; name this event ‘subbagp-make-negs-off’. Event: Enable member-rneg-make-negs; name this event ‘member-rneg-make-negs-off’. Event: Enable bagdiff-bagdiff; name this event ‘bagdiff-bagdiff-off’. Event: Enable append-bagdiff-arg2; name this event ‘append-bagdiff-arg2-off’. Event: Enable append-bagdiff-arg1; name this event ‘append-bagdiff-arg1-off’.

Event: Enable make-negs-bagdiff; name this event ‘make-negs-bagdiff-off’. Event: Enable make-negs-delete; name this event ‘make-negs-delete-off’. Event: Enable not-member-make-negs-fact; name this event ‘not-member-make-negs-fact-off’. Event: Enable subbagp-transitive; name this event ‘subbagp-transitive-off’. Event: Enable subbagp-necc; name this event ‘subbagp-necc-off’. Event: Enable not-subbagp-not-permutation; name this event ‘not-subbagp-not-permutation-off’. Event: Enable permutation-a-b; name this event ‘permutation-a-b-off’. Event: Enable subbagp-permutation; name this event ‘subbagp-permutation-off’. Event: Enable subbagp-delete-car2; name this event ‘subbagp-delete-car2-off’. Event: Enable subbagp-delete-car; name this event ‘subbagp-delete-car-off’. Event: Enable subbagp-delete-same-means; name this event ‘subbagp-delete-same-means-off’. Event: Enable subbagp-delete-same; name this event ‘subbagp-delete-same-off’. Event: Enable subbagp-append; name this event ‘subbagp-append-off’. Event: Enable occurrences-append; name this event ‘occurrences-append-off’. Event: Enable occurrences-delete2; name this event ‘occurrences-delete2-off’. Event: Enable member-subbagp; name this event ‘member-subbagp-off’.

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

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

Event: Enable eval$-reduce; name this event ‘eval$-reduce-off’.

Event: Enable eval$-rplus; name this event ‘eval$-rplus-off’.

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

Event: Enable rplus-rzerop-bridge2; name this event ‘rplus-rzerop-bridge2-off’.

Event: Enable rplus-rzerop-bridge; name this event ‘rplus-rzerop-bridge-off’.

Definition: cancel-rplus (x) = if car (x) = 'rplus

then if listp (bagint (car (split-by-parity (rplus-fringe (x))),

cdr (split-by-parity (rplus-fringe (x))))) then rplus-tree (append (bagdiff (car (split-by-parity (rplus-fringe (x))),

bagint (car (split-by-parity (rplus-fringe (x))),

cdr (split-by-parity (rplus-fringe (x))))),

make-negs (bagdiff (cdr (split-by-parity (rplus-fringe (x))),

bagint (car (split-by-parity (rplus-fringe (x))),

cdr (split-by-parity (rplus-fringe (x))))))))

else x endif else x endif

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

Event: Enable correctness-of-cancel-rplus; name this event ‘correctness-of-cancel-rplus-off’.

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

Event: Let us define the theory r2 to consist of the following events: rtimesrneg-arg2, rtimes-rneg-arg1, rtimes-rplus-arg2, rtimes-rplus-arg1, associativityof-rtimes, rzerop, commutativity-of-rtimes, rdifference-rdifference-arg2, rdifferencerdifference-arg1, rneg-rplus, rplus-reduce-arg2-rewrite, rplus-reduce-arg1-rewrite, reduce-rneg, reduce-rmagnitude, reduce-rquotient, reduce-difference, reduce-rtimes, reduce-rplus, commutativity2-of-rplus, associativity-of-rplus, equal-requal-rewrite, transitivity-of-requal, fix-rational-of-rationalp, nrational-rplus-arg2, nrationalrplus-arg1, rationalp-means, means-rationalp, rneg-rneg, rneg-reduce, reduce-0, numberp-numerator-reduce, reduce-nrationalp, rplus-reduce-arg2, rplus-reduce-arg1, requal-x-x, rplus-requal-arg1, commutativity-of-rplus, reduce-reduce, requalreduce2, requal-reduce1, commutativity-of-requal, rational-generalization, fixrational-rmagnitude, fix-rational-rquotient, fix-rational-rdifference, fix-rational-rneg, fix-rational-rtimes, fix-rational-fix-rational, fix-rational-rplus, fix-rational-reduce, rationalp-rmagnitude, rationalp-rquotient, rationalp-rdifference, rationalprneg, rationalp-rtimes, rationalp-fix-rational, rationalp-rplus, rationalp-reduce, commutativity2-of-rtimes, rdifference, correctness-of-cancel-rplus.

Event: Make the library "r2".

Index

addition, 15 all-rnegs, 88, 89 all-rnegs-make-negs-bagint, 89 all-rnegs-make-negs-bagint-fact, 89

-off, 90 all-rnegs-make-negs-bagint-off, 90 and-not-zerop-tree, 45, 47–49 append-bagdiff-arg1, 84 append-bagdiff-arg1-off, 93 append-bagdiff-arg2, 84 append-bagdiff-arg2-off, 93 arithmetic, 30 associativity-of-gcd, 30 associativity-of-gcd-zero-case, 30 associativity-of-iplus, 33 associativity-of-itimes, 37 associativity-of-plus, 5 associativity-of-rplus, 65 associativity-of-rplus-off, 72 associativity-of-rtimes, 67 associativity-of-rtimes-off, 70 associativity-of-simple-rtimes, 66 associativity-of-simple-rtimes-

off, 70

when-not-rzerop, 66 when-not-rzerop-off, 71

associativity-of-times, 16

badguy, 82 bagdiff, 1–3, 8–10, 12, 35–37, 46–50,

84, 86–88, 95 bagdiff-append-arg1, 86 bagdiff-append-arg1-off, 92 bagdiff-bagdiff, 84 bagdiff-bagdiff-off, 93 bagdiff-car-in, 86 bagdiff-car-in-off, 91 bagdiff-cons-z-z, 86 bagdiff-cons-z-z-off, 91 bagdiff-delete, 46 bagdiff-delete-off, 51 bagdiff-not-listp, 86 bagdiff-not-listp-off, 91 bagdiff-x-x, 86 bagdiff-x-x-off, 92 bagint, 1–3, 5, 9, 10, 12, 35–37, 47– 50, 84, 88, 89, 95

bagint-all-rnegs-car-split-by-p arity, 89 arity-off, 90

bagint-make-negs-split-by-parit y, 89 y-off, 90

bridge-to-subbagp-implies-plus-t ree-greatereqp, 9 ree-greatereqp-off, 13

cadr-eval$-list, 9 cadr-eval$-list-off, 13 cancel-difference-plus, 10, 11 cancel-difference-plus-off, 13 cancel-equal-plus, 9, 10 cancel-equal-plus-off, 13 cancel-equal-times, 49, 50 cancel-equal-times-preserves-ineq

uality, 50

uality-bridge, 50 uality-bridge-off, 52 uality-off, 52 cancel-idifference, 36, 37 cancel-idifference-off, 43 cancel-iplus, 35, 36 cancel-iplus-off, 44 cancel-lessp-plus, 12 cancel-lessp-plus-off, 12 cancel-lessp-times, 47, 48 cancel-quotient-times, 48, 49 cancel-rplus, 95 cancel-rplus-off, 95 cancel-zero-fact, 86 cancel-zero-fact-bridge, 87 cancel-zero-fact-bridge-off, 89 cancel-zero-fact-off, 89 cancelling-from-rplus, 88 cancelling-from-rplus-off, 89 common-divisor-divides-gcd, 30 commutativity-of-gcd, 29 commutativity-of-iplus, 33 commutativity-of-itimes, 37 commutativity-of-permutation, 3 commutativity-of-plus, 5 commutativity-of-requal, 61 commutativity-of-requal-off, 75 commutativity-of-rplus, 62 commutativity-of-rplus-off, 75 commutativity-of-rtimes, 66 commutativity-of-rtimes-off, 71 commutativity-of-simple-rplus, 68 commutativity-of-simple-rplus-o

ff, 69 commutativity-of-simple-rtimes, 66 commutativity-of-simple-rtimes-

off, 71 commutativity-of-times, 15 commutativity2-of-gcd, 30 commutativity2-of-gcd-zero-case, 30 commutativity2-of-iplus, 33 commutativity2-of-itimes, 37 commutativity2-of-plus, 5 commutativity2-of-rplus, 65 commutativity2-of-rplus-off, 72 commutativity2-of-rtimes, 89 commutativity2-of-times, 15 correctness-of-cancel-difference

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

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

s, 50 correctness-of-cancel-idifferen

ce, 37 correctness-of-cancel-iplus, 36 correctness-of-cancel-lessp-plu

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

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

mes, 49 correctness-of-cancel-rplus, 95 correctness-of-cancel-rplus-off, 95

delete, 1–4, 8, 10, 12, 35–37, 46, 47,

82, 83, 86, 87, 89 delete-append, 82 delete-append-off, 95 delete-delete, 2 delete-non-member, 2 denominator, 53, 54, 56, 61–63 diff-add1-arg2, 11 diff-add1-arg2-casesplit, 11 diff-diff-arg1, 11 diff-diff-arg2, 11 diff-diff-arg2-casesplit, 11 diff-diff-diff, 11 diff-diff-diff-casesplit, 11 diff-sub1-arg2, 11 diff-sub1-arg2-casesplit, 11 diff-x-x, 12 difference-1, 7 difference-1-off, 14 difference-2, 7 difference-2-off, 14 difference-add1-plus-cancellati

on, 7 on-off, 14

difference-cancellation-0, 7 difference-cancellation-0-off, 14 difference-cancellation-1, 7 difference-cancellation-1-off, 14 difference-difference-arg1, 7 difference-difference-arg1-off, 14 difference-difference-arg2, 7 difference-difference-arg2-off, 14 difference-difference-difference, 8

-off, 14 difference-elim, 6 difference-leq-arg1, 6 difference-plus, 7 difference-plus-cancellation1, 7 difference-plus-cancellation1-o

ff, 14 difference-plus-cancellation2, 7 difference-plus-cancellation2-o

ff, 14 difference-plus-cancellation3, 8 difference-plus-cancellation3-o

ff, 14 difference-plus-off, 14 difference-sub1-arg2, 7 difference-sub1-arg2-off, 14 difference-x-x, 7 difference-x-x-off, 15 distributivity-of-times-over-gc

d, 30 d-proof, 30

divides-each-equality, 57 divides-each-equality-off, 77 divides-product-reduction, 58 divides-product-reduction-off, 76 division-theorem, 39 division-theorem-for-truncate-t

o-neginf, 40 o-neginf-part1, 39 o-neginf-part2, 39 o-neginf-part3, 40 o-zero, 41 o-zero-part1, 40 o-zero-part2, 40 o-zero-part3, 40

division-theorem-part1, 38 division-theorem-part2, 38 division-theorem-part3, 38 double-log-induction, 27 double-number-induction, 22 double-remainder-induction, 20 dpr-hack1, 58 dpr-hack1-off, 59 dpr-hack1-off1, 77 dpr-hack2, 58 dpr-hack2-off, 59 dpr-hack2-off1, 77 dpr-hack3, 58 dpr-hack3-off, 59 dpr-hack3-off1, 77 dpr-hack4, 58 dpr-hack4-off, 59 dpr-hack4-off1, 77 dpr-hack5, 58 dpr-hack5-off, 59 dpr-hack5-off1, 76

equal-difference, 85 equal-difference-0, 7 equal-difference-hack1, 84 equal-difference-hack1-off, 93 equal-difference-hack2, 85 equal-difference-hack2-off, 93 equal-difference-off, 92 equal-difference-rewrite, 85 equal-difference-rewrite-off, 92 equal-difference-rewrite2, 85 equal-difference-rewrite2-off, 92 equal-exp-0, 27 equal-exp-1, 27 equal-gcd-0, 29 equal-idifference-0, 34 equal-ineg-ineg, 55 equal-ineg-ineg-off, 79 equal-itimes-0, 38 equal-itimes-1, 38 equal-itimes-minus-1, 38 equal-log-0, 27 equal-occurrences-zero, 2 equal-permutation, 87 equal-permutation-off, 91 equal-plus-0, 5 equal-plus-1, 6 equal-plus-difference-rewrite, 85 equal-plus-difference-rewrite-o

ff, 92 equal-quotient-0, 23 equal-remainder-difference-0, 20 equal-remainder-difference-0-of

f, 22 equal-remainder-plus-0, 19 equal-remainder-plus-0-proof, 19 equal-remainder-plus-remainder, 19 equal-remainder-plus-remainder-

off, 22 equal-remainder-plus-remainder-p

roof, 19 equal-requal-rewrite, 64 equal-requal-rewrite-off, 65 equal-requal-rewrite-off1, 72 equal-rplus-rdifference-hack, 85 equal-rplus-rdifference-hack-of

f, 92 equal-rplus-x-x-rewrite, 85 equal-rplus-x-x-rewrite-off, 92 equal-sub1-times-0, 18 equal-times-0, 16 equal-times-1, 16 equal-times-arg1, 47 equal-times-arg1-off, 51 equal-times-bridge, 47 equal-times-bridge-off, 51 equal-times-bridge1, 64 equal-times-bridge1-off, 73 equal-times-bridge2, 64 equal-times-bridge2-off, 73 equal-times-bridge3, 64 equal-times-bridge3-off, 73 equal-times-bridge4, 64 equal-times-bridge4-off, 73 equal-times-bridge5, 85 equal-times-bridge5-off, 92 equal-times-gcd-bridge1, 61 equal-times-gcd-bridge1-off, 76 equal-times-times-quotient-arg2, 60

-off, 76 eval$-equal, 46 eval$-equal-off, 50 eval$-equal-times-tree-bagdiff, 49

-off, 52 eval$-if, 46 eval$-if-off, 51 eval$-if2, 46 eval$-if2-off, 51 eval$-iplus-tree-append, 36 eval$-iplus-tree-append-inducti

on, 36 eval$-iplus-tree-append-off, 43 eval$-lessp, 46 eval$-lessp-off, 50 eval$-lessp-times-tree-bagdiff, 48

-off, 52 eval$-lessp2, 46 eval$-lessp2-off, 50 eval$-or, 46 eval$-or-off, 50 eval$-or2, 46 eval$-or2-off, 50 eval$-plus-tree-append, 9 eval$-plus-tree-append-off, 13 eval$-quote, 9 eval$-quote-off, 13 eval$-quotient, 46 eval$-quotient-off, 51 eval$-quotient-times-tree-bagdi

ff, 49 ff-off, 52

eval$-quotient2, 46 eval$-quotient2-off, 51 eval$-reduce, 81 eval$-reduce-off, 95 eval$-rplus, 81 eval$-rplus-off, 95 eval$-rplus-tree-delete, 86 eval$-rplus-tree-delete-off, 89 eval$-rplus-tree-rplus-fringe, 88 eval$-rplus-tree-rplus-fringe-

off, 89 eval$-rplus-tree-zero, 86 eval$-rplus-tree-zero-off, 89 eval$-times, 45 eval$-times-member, 47 eval$-times-member-off, 51 eval$-times-off, 50 eval$-times2, 45 eval$-times2-off, 50 exp, 15, 21, 22, 25–28 exp-0-arg1, 26 exp-0-arg2, 27 exp-1-arg1, 26 exp-add1, 26 exp-difference, 27 exp-exp, 27 exp-plus, 26 exp-times, 27 exp-zero, 26 exponentiation, 27

fix-int, 31–34, 36–42, 54 fix-int-fix-int, 32 fix-int-iabs, 32 fix-int-idifference, 32 fix-int-idiv, 42 fix-int-imod, 42 fix-int-ineg, 32 fix-int-iplus, 32 fix-int-iquo, 42 fix-int-iquotient, 42 fix-int-irem, 42 fix-int-iremainder, 42 fix-int-itimes, 32 fix-int-off, 44 fix-int-off1, 59 fix-int-on, 57 fix-int-on-integers, 54 fix-int-on-integers-off, 79 fix-rational, 53–56, 62–64, 67 fix-rational-fix-rational, 56 fix-rational-fix-rational-off, 78 fix-rational-of-rationalp, 63 fix-rational-of-rationalp-off, 73 fix-rational-off, 80 fix-rational-rdifference, 56 fix-rational-rdifference-off, 78 fix-rational-reduce, 56 fix-rational-reduce-off, 78 fix-rational-rmagnitude, 56 fix-rational-rmagnitude-off, 78 fix-rational-rneg, 56 fix-rational-rneg-off, 78 fix-rational-rplus, 56 fix-rational-rplus-off, 78 fix-rational-rquotient, 56 fix-rational-rquotient-off, 78 fix-rational-rtimes, 56 fix-rational-rtimes-off, 78 fix-rational-simple-rplus, 64 fix-rational-simple-rplus-off, 73 fix-rational-simple-rtimes, 67 fix-rational-simple-rtimes-off, 70

gcd, 28–30, 53, 56–58, 60, 61

gcd-0, 29 gcd-1, 29 gcd-factors, 57, 58 gcd-factors-gives-linear-combin

ation, 57 ation-off, 59 ation-off1, 77 ation-rewrite, 58 ation-rewrite-off, 59 ation-rewrite-off1, 77

gcd-factors-off, 59 gcd-factors-off1, 77 gcd-idempotence, 30 gcd-is-the-greatest, 30 gcd-plus, 29 gcd-plus-instance, 29 gcd-plus-instance-temp, 29 gcd-plus-instance-temp-proof, 29 gcd-plus-proof, 29 gcd-quotient-quotient, 57 gcd-quotient-quotient-off, 77 gcd-remainder-fact1, 56 gcd-remainder-fact1-off, 77 gcd-remainder-fact2, 56 gcd-remainder-fact2-off, 77 gcd-remainder-times-fact1-proof, 60

-off, 76 gcd-times1, 56 gcd-times1-induct, 56 gcd-times1-induct-off, 77 gcd-times1-off, 77 gcd-times2, 56 gcd-times2-off, 77 gcd-x-x, 30 gcds, 30

iabs, 31, 32, 38–41

iabs-off, 44 idifference, 31–34, 36–40, 57 idifference-0, 34 idifference-cancellation-1, 34 idifference-fix-int, 34 idifference-idifference, 34 idifference-iplus, 34 idifference-iplus-canonicalizer

1-off, 57 1-on, 59 1, 34

idifference-off, 44 idifference-off1, 59 idifference-on, 57 idifference-right-id, 34 idifference-x-x, 34 idiv, 39–42 idiv-fix-int1, 42 idiv-fix-int2, 42 idiv-imod-uniqueness, 40 idiv-off, 43 ileq, 31, 38–41 ileq-off, 44 ilessp, 31, 38–41, 54 ilessp-off, 44 ilessp-off1, 59 ilessp-on, 57 imod, 39–42 imod-fix-int1, 42 imod-fix-int2, 42 imod-off, 43 ineg, 31–33, 40, 41, 53–55, 62, 64 ineg-fix-int, 33 ineg-id, 32 ineg-idifference, 33 ineg-ineg, 33 ineg-iplus, 33 ineg-off, 44 ineg-off1, 59 ineg-on, 57 integerp, 30–36, 38–41, 53–56, 61,

63 integerp-eval$-bridge, 35 integerp-eval$-bridge-off, 43 integerp-eval$-iplus, 35 integerp-eval$-iplus-off, 44 integerp-eval$-iplus-tree, 35 integerp-eval$-iplus-tree-off, 43 integerp-fix-int, 32 integerp-iabs, 32 integerp-idifference, 32 integerp-idiv, 41 integerp-if-negativep-non-zero, 55 integerp-if-negativep-non-zero-

off, 79 integerp-if-numberp, 55 integerp-if-numberp-off, 79 integerp-imod, 41 integerp-ineg, 32 integerp-iplus, 32 integerp-iquo, 41 integerp-iquotient, 41 integerp-irem, 41 integerp-iremainder, 41 integerp-itimes, 32 integerp-minus, 54 integerp-minus-off, 79 integerp-off, 44 integerp-on, 57 integers, 45 iplus, 31–34, 36–41, 53, 55, 58, 62 iplus-0, 33 iplus-cancellation, 33 iplus-fix-int1, 33 iplus-fix-int2, 33 iplus-fringe, 34–37 iplus-idifference-arg1, 33 iplus-idifference-arg2, 34 iplus-idifference-idifference, 36 iplus-ineg1, 33 iplus-ineg2, 33 iplus-is-plus, 55 iplus-is-plus-off, 79 iplus-left-id, 33 iplus-off, 44 iplus-off1, 59 iplus-on, 57 iplus-right-id, 33 iplus-tree, 34–37 iplus-tree-bagdiff, 36 iplus-tree-bagdiff-off, 43 iplus-tree-delete, 36 iplus-tree-delete-off, 43 iplus-tree-iplus-fringe, 36 iplus-tree-iplus-fringe-off, 43 iquo, 40–42 iquo-fix-int1, 42 iquo-fix-int2, 42 iquo-irem-uniqueness, 41 iquo-off, 43 iquotient, 38, 39, 41, 42, 58 iquotient-fix-int1, 41 iquotient-fix-int2, 41 iquotient-iremainder-uniqueness, 39 iquotient-off, 43 iquotient-off1, 60 iquotient-on, 58 irem, 40–42 irem-fix-int1, 42 irem-fix-int2, 42 irem-off, 43 iremainder, 38, 39, 41, 42, 58 iremainder-fix-int1, 41 iremainder-fix-int2, 42 iremainder-off, 43 iremainder-off1, 60 iremainder-on, 58 itimes, 32, 37–41, 53–55, 57, 58, 61,

62 itimes-1-arg1, 38 itimes-distributes-over-idiffere

nce, 38 nce-proof, 37

itimes-distributes-over-iplus, 37 itimes-distributes-over-iplus-p

roof, 37 itimes-fix-int1, 37 itimes-fix-int2, 37 itimes-ineg-arg1, 54 itimes-ineg-arg1-off, 79 itimes-ineg-arg2, 55 itimes-ineg-arg2-off, 79 itimes-is-times, 55 itimes-is-times-off, 79 itimes-negativep-arg1, 55 itimes-negativep-arg1-off, 79 itimes-negativep-arg2, 55 itimes-negativep-arg2-off, 79 itimes-off, 44 itimes-off1, 59 itimes-on, 57 itimes-zero1, 37 itimes-zero2, 37 izerop, 31, 37–40 izerop-off, 44 izerop-off1, 60 izerop-on, 57

last-cdr, 86, 87 last-cdr-delete, 87 last-cdr-delete-off, 91 leq-log-log, 28 leq-quotient, 25 lessp-1-times, 18 lessp-difference, 12 lessp-difference-cancellation, 12 lessp-difference-cancellation-o

ff, 12 lessp-gcd, 29 lessp-plus-fact, 21 lessp-plus-fact-off, 22 lessp-plus-times-proof, 17 lessp-plus-times1, 17 lessp-plus-times2, 17 lessp-quotient, 26 lessp-remainder, 18 lessp-times-arg1, 46 lessp-times-arg1-off, 51 lessp-times-bridge1, 85 lessp-times-bridge1-off, 92 lessp-times-cancellation-proof, 17 lessp-times-cancellation1, 17 lessp-times-cancellation2, 17 lessp-times1, 16 lessp-times1-proof, 16 lessp-times2, 16 lessp-times2-proof, 16 lessp-times3, 17 lessp-times3-proof1, 16 lessp-times3-proof2, 17 listp-delete, 2 listp-eval$, 9 listp-eval$-off, 13 log, 27, 28 log-0, 27 log-1, 27 log-exp, 28 log-quotient, 28 log-quotient-exp, 28 log-quotient-times, 28 log-quotient-times-proof, 28 log-times, 28 log-times-exp, 28 log-times-exp-proof, 28 log-times-proof, 28 logs, 28

make-negs, 81, 83, 84, 86–89, 95 make-negs-bagdiff, 84 make-negs-bagdiff-off, 94 make-negs-delete, 83 make-negs-delete-off, 94 means-rationalp, 63 means-rationalp-off, 74 member-append, 82 member-append-off, 95 member-bagdiff, 3 member-bagdiff-append, 86 member-bagdiff-append-off, 92 member-bagint, 3 member-car-x-x, 86 member-car-x-x-off, 92 member-cdr-split-by-parity, 88 member-cdr-split-by-parity-off, 90 member-cons, 3 member-delete, 3 member-delete-implies-membership,

3 member-implies-numberp, 9 member-implies-numberp-off, 13 member-implies-plus-tree-greate reqp, 8 reqp-off, 13 member-non-list, 2 member-occur, 82 member-occur-off, 82 member-rneg-make-negs, 84 member-rneg-make-negs-off, 93 member-subbagp, 82 member-subbagp-delete, 87 member-subbagp-delete-off, 91 member-subbagp-off, 94 member-subbagp2, 87 member-subbagp2-off, 91 multiplication, 18

negative-guts-ineg, 64 negative-guts-ineg-off, 73 negativep-if-integerp-and-not-n

umberp, 61 umberp-off, 61 umberp-off1, 75

negativep-ineg, 62 negativep-ineg-off, 74 not-integerp-implies-not-equal-ip

lus, 36 lus-off, 43

not-member-make-negs-fact, 83 not-member-make-negs-fact-off, 94 not-permutation, 3 not-subbagp-not-permutation, 83 not-subbagp-not-permutation-off, 94 nrational-rplus-arg1, 63 nrational-rplus-arg1-off, 74 nrational-rplus-arg2, 63 nrational-rplus-arg2-off, 74 nrational-simple-rplus-arg1, 63 nrational-simple-rplus-arg1-off, 74 nrational-simple-rplus-arg2, 63 nrational-simple-rplus-arg2-off, 73 numberp-eval$-bridge, 8 numberp-eval$-bridge-off, 13 numberp-eval$-plus, 8 numberp-eval$-plus-off, 14 numberp-eval$-plus-tree, 8 numberp-eval$-plus-tree-off, 13 numberp-eval$-times, 45 numberp-eval$-times-off, 50 numberp-eval$-times-tree, 46 numberp-eval$-times-tree-off, 51 numberp-if-integerp-and-not-neg

ativep, 61 ativep-off, 61 ativep-off1, 75

numberp-ineg, 62 numberp-ineg-off, 74 numberp-numerator-reduce, 62 numberp-numerator-reduce-off, 74 numerator, 53, 54, 56, 61–63, 66, 67 numerator-type, 67 numerator-type-off, 70 numerator-zero-rzerop-bridge, 66 numerator-zero-rzerop-bridge-of

f, 71

occurrences, 1–3, 82, 83 occurrences-append, 82 occurrences-append-off, 94 occurrences-bagdiff, 2 occurrences-bagint, 2 occurrences-cons, 2 occurrences-delete, 2 occurrences-delete2, 82 occurrences-delete2-off, 94 occurrences-in-a-set, 2 open-plus, 5 open-plus-off, 15 or-zerop-tree, 45, 47, 49 or-zerop-tree-is-not-zerop-tree, 47

-off, 51

permutation, 1, 3, 4, 83, 86–88 permutation-a-b, 83 permutation-a-b-off, 94 permutation-append-arg1-arg2-bri

dge, 87 dge-off, 91

permutation-append-split-by-parit y-bridge, 88

y-bridge-off, 90 permutation-as-subbagp, 83 permutation-as-subbagp-helper, 83 permutation-as-subbagp-helper-o

ff, 83 permutation-as-subbagp-off, 83 permutation-bagdiff, 87 permutation-bagdiff-append, 87 permutation-bagdiff-append-helpe

r, 87 r-off, 91

permutation-bagdiff-append-off, 91 permutation-bagdiff-off, 91 permutation-delete-delete, 3 permutation-does-not-effect-rpl

us, 86 us-off, 89

permutation-implies-membership-eq

uivalence, 3 permutation-reflexivity, 3 permutation-right-cons, 3 permutation-right-cons1, 3 permutation-transitive, 86 permutation-transitive-off, 92 plus-add1, 5 plus-cancellation, 6 plus-cancellation-off, 15 plus-difference-arg1, 6 plus-difference-arg1-casesplit, 6 plus-difference-arg2, 6 plus-difference-arg2-casesplit, 6 plus-difference-difference, 6 plus-difference-difference-case

split, 6 plus-fringe, 8–10, 12 plus-remainder-times-quotient, 18 plus-remainder-times-quotient-o

ff, 22 plus-right-id2, 5 plus-stopper, 5 plus-tree, 8–10, 12 plus-tree-bagdiff, 8 plus-tree-bagdiff-off, 13 plus-tree-delete, 8 plus-tree-delete-off, 13 plus-tree-plus-fringe, 9 plus-tree-plus-fringe-off, 13

quotient-1-arg1, 26 quotient-1-arg1-casesplit, 26 quotient-1-arg2, 25 quotient-add1, 23 quotient-difference-lessp-arg2, 39 quotient-difference-lessp-arg2-

off, 43 quotient-difference1, 24 quotient-difference2, 24 quotient-difference3, 24 quotient-exp, 25 quotient-gcd-times-fact, 60 quotient-gcd-times-fact-off, 76 quotient-gcd-times-fact1, 60 quotient-gcd-times-fact1-off, 76 quotient-gcd-times-fact2, 60 quotient-gcd-times-fact2-off, 76 quotient-gcd-times-fact3, 60 quotient-gcd-times-fact3-off, 76 quotient-gcd-times-fact4, 60 quotient-gcd-times-fact4-off, 76 quotient-gcd-times-fact5, 61 quotient-gcd-times-fact5-off, 76 quotient-lessp-arg1, 24 quotient-noop, 22 quotient-of-non-number, 22 quotient-plus, 23 quotient-plus-fact, 25 quotient-plus-proof, 23 quotient-plus-times-times, 25 quotient-plus-times-times-insta

nce, 25 quotient-plus-times-times-proof, 25 quotient-quotient, 25 quotient-remainder, 25 quotient-remainder-instance, 25 quotient-remainder-times, 24 quotient-remainder-uniqueness, 38 quotient-sub1, 23 quotient-times, 23 quotient-times-instance, 24 quotient-times-instance-temp, 23 quotient-times-instance-temp-of

f, 26 quotient-times-instance-temp-pr

oof, 23 quotient-times-proof, 23 quotient-times-times, 24 quotient-times-times-proof, 24 quotient-x-x, 26 quotient-zero, 23 quotients, 26

r1, 80 r2, 96 rational, 52–54, 62, 63, 81, 84, 86,

87 rational-defns, 52 rational-formp, 52, 63 rational-generalization, 56 rational-generalization-off, 77 rational-ineg-numerator-reduce-

bridge, 62 bridge-off, 74 rationalp, 52–56, 61–64, 67 rationalp-fix-rational, 55 rationalp-fix-rational-off, 78 rationalp-means, 63 rationalp-means-off, 74 rationalp-off, 80 rationalp-rdifference, 55 rationalp-rdifference-off, 78 rationalp-reduce, 55 rationalp-reduce-off, 78 rationalp-rmagnitude, 55 rationalp-rmagnitude-off, 78 rationalp-rneg, 55 rationalp-rneg-off, 78 rationalp-rplus, 55 rationalp-rplus-off, 78 rationalp-rquotient, 55 rationalp-rquotient-off, 78 rationalp-rtimes, 55 rationalp-rtimes-off, 78 rationalp-simple-rplus, 64 rationalp-simple-rplus-off, 73 rationalp-simple-rtimes, 67 rationalp-simple-rtimes-off, 70 rdifference, 53, 55, 56, 65, 66, 68,

84–86 rdifference-off, 80 rdifference-rdifference-arg1, 66 rdifference-rdifference-arg1-of

f, 71 rdifference-rdifference-arg2, 66 rdifference-rdifference-arg2-of

f, 71 rdifference-reduce, 84 rdifference-reduce-off, 93 rdifference-rneg-arg2, 68 rdifference-rneg-arg2-off, 69 rdifference-rplus-hack, 84 rdifference-rplus-hack-off, 93 rdifference-rplus-hack2, 84 rdifference-rplus-hack2-off, 93 rdifference-x-x, 84 rdifference-x-x-off, 93 reduce, 53–56, 61–63, 65, 67, 81, 82,

84, 85 reduce-0, 63 reduce-0-off, 74 reduce-difference, 65 reduce-difference-off, 72 reduce-eval$-rplus-tree, 82 reduce-eval$-rplus-tree-off, 90 reduce-nrationalp, 62 reduce-nrationalp-off, 74 reduce-off, 80 reduce-reduce, 61 reduce-reduce-off, 75 reduce-rmagnitude, 65 reduce-rmagnitude-off, 72 reduce-rneg, 65 reduce-rneg-off, 72 reduce-rplus, 65 reduce-rplus-off, 72 reduce-rquotient, 65 reduce-rquotient-off, 72 reduce-rtimes, 65 reduce-rtimes-off, 72 remainder-0-sufficiency, 58 remainder-0-sufficiency-off, 59 remainder-0-sufficiency-off1, 76 remainder-1-arg1, 21 remainder-1-arg2, 21 remainder-add1, 19 remainder-difference1, 20 remainder-difference2, 20 remainder-difference3, 20 remainder-difference3-off, 22 remainder-equals-its-first-argu

ment, 24 ment-off, 26 remainder-exp, 21 remainder-exp-exp, 22 remainder-gcd, 29 remainder-noop, 18 remainder-of-non-number, 18 remainder-plus, 19 remainder-plus-fact, 21 remainder-plus-proof, 19 remainder-plus-times-times, 21 remainder-plus-times-times-inst

ance, 21 remainder-plus-times-times-proo

f, 21 remainder-quotient-elim, 18 remainder-remainder, 21 remainder-sub1, 18 remainder-times-times, 20 remainder-times-times-off, 22 remainder-times-times-proof, 19 remainder-times1, 19 remainder-times1-instance, 19 remainder-times1-instance-proof, 19 remainder-times1-proof, 19 remainder-times2, 20 remainder-times2-instance, 20 remainder-times2-proof, 20 remainder-x-x, 21 remainder-zero, 18 remainders, 22 requal, 54, 61–68, 84, 85 requal-associativity-of-rplus, 65 requal-associativity-of-rplus-o

ff, 72 requal-associativity-of-rtimes, 67 requal-associativity-of-rtimes-

off, 70 requal-associativity-of-simple-

rplus, 64 rplus-off, 73

requal-off, 79 requal-reduce-reduce-equal, 61 requal-reduce-reduce-equal-off, 61 requal-reduce-reduce-equal-off1, 75 requal-reduce1, 61 requal-reduce1-off, 75 requal-reduce2, 61 requal-reduce2-off, 75 requal-rneg-rneg, 63 requal-rneg-rneg-off, 74 requal-rneg-simple-rplus, 66 requal-rneg-simple-rplus-off, 71 requal-rplus-rneg, 66 requal-rplus-rneg-off, 71 requal-rplus-x-simple-rneg-x, 84 requal-rplus-x-simple-rneg-x-of

f, 93 requal-rtimes-rneg, 68 requal-rtimes-rneg-off, 69 requal-rtimes-rplus-bridge, 68 requal-rtimes-rplus-bridge-off, 69 requal-rzerop-simple-rplus, 67 requal-rzerop-simple-rplus-off, 69 requal-simple-rplus-bridge, 65 requal-simple-rplus-bridge-off, 72 requal-simple-rplus-reduce-arg1, 62

-off, 75 requal-simple-rplus-reduce-arg2, 62

-off, 75 requal-simple-rplus-x-simple-rne

g-x, 84 g-x-off, 93

requal-simple-rplus-x-x-rewrite, 85 -off, 92 requal-simple-rtimes-bridge, 67 requal-simple-rtimes-bridge-off, 70 requal-simple-rtimes-reduce-arg

1-off, 70 2-off, 70 1, 67 2, 67

requal-simple-rtimes-requal-arg 1-off, 70 2-off, 70 1, 66 2, 67

requal-simple-rtimes-simple-rne g, 68 g-off, 69

requal-simple-rtimes-simple-rpl us-arg1, 68 us-arg1-off, 69 us-when-not-rzerop, 67 us-when-not-rzerop-off, 70

requal-x-x, 62 requal-x-x-off, 75 rinverse, 54 rlessp, 54 rlessp-off, 79 rmagnitude, 54–56, 65 rmagnitude-off, 79 rneg, 53–56, 63, 65, 66, 68, 84 rneg-off, 80 rneg-rdifference, 68 rneg-rdifference-off, 69 rneg-reduce, 63 rneg-reduce-off, 74 rneg-rneg, 63 rneg-rneg-off, 74 rneg-rplus, 66 rneg-rplus-off, 71 rnegs-cancel-list, 87 rnegs-cancel-list-off, 89 rnegs-not-car-split-by-parity, 88 rnegs-not-car-split-by-parity-o

ff, 90 rplus, 53, 55, 56, 61–63, 65, 66, 68, 81, 82, 84, 85 rplus-eval$-rplus-tree, 82 rplus-eval$-rplus-tree-off, 89 rplus-fringe, 81, 88, 95 rplus-off, 80 rplus-open-up, 61 rplus-open-up-off, 62 rplus-open-up-off1, 75 rplus-rdifference-arg1, 65 rplus-rdifference-arg1-off, 72 rplus-rdifference-arg2, 65 rplus-rdifference-arg2-off, 72 rplus-rdifference-hack, 84 rplus-rdifference-hack-off, 93 rplus-reduce-arg1, 62 rplus-reduce-arg1-off, 75 rplus-reduce-arg1-rewrite, 65 rplus-reduce-arg1-rewrite-off, 72 rplus-reduce-arg2, 62 rplus-reduce-arg2-off, 75 rplus-reduce-arg2-rewrite, 65 rplus-reduce-arg2-rewrite-off, 71 rplus-requal-arg1, 62 rplus-requal-arg1-off, 62 rplus-requal-arg1-off1, 75 rplus-rneg-arg1, 66 rplus-rneg-arg1-off, 71 rplus-rneg-arg2, 66 rplus-rneg-arg2-off, 71 rplus-rzerop, 81 rplus-rzerop-bridge, 81 rplus-rzerop-bridge-off, 95 rplus-rzerop-bridge2, 81 rplus-rzerop-bridge2-off, 95 rplus-rzerop-off, 95 rplus-tree, 80–82, 86–88, 95 rplus-x-rneg-x, 84 rplus-x-rneg-x-off, 93 rquotient, 54–56, 65 rquotient-off, 79 rtimes, 54–56, 65–68, 89 rtimes-off, 79 rtimes-rdifference-arg1, 68 rtimes-rdifference-arg1-off, 69 rtimes-rdifference-arg2, 68 rtimes-rdifference-arg2-off, 69 rtimes-rneg-arg1, 68 rtimes-rneg-arg1-off, 69 rtimes-rneg-arg2, 68 rtimes-rneg-arg2-off, 69 rtimes-rplus-arg1, 68 rtimes-rplus-arg1-off, 69 rtimes-rplus-arg2, 68 rtimes-rplus-arg2-off, 69 rzerop, 54, 66–68, 81 rzerop-off, 71

setp, 1, 2, 4 setp-delete, 4 setp-permutation, 4 setp-permutation-base-case, 4 setp-permutation-induction, 4 setp-permutation-induction-step, 4 sets-and-bags, 5 simple-rinverse, 54 simple-rmagnitude, 54 simple-rmagnitude-off, 79 simple-rneg, 53, 63, 66, 68, 84 simple-rneg-off, 80 simple-rneg-reduce, 63 simple-rneg-reduce-off, 74 simple-rneg-simple-rneg, 63 simple-rneg-simple-rneg-off, 74 simple-rplus, 53, 62–68, 84, 85 simple-rplus-bridge, 68 simple-rplus-bridge-off, 69 simple-rplus-fix-rational-arg1, 63 simple-rplus-fix-rational-arg1-

off, 73 simple-rplus-fix-rational-arg2, 63 simple-rplus-fix-rational-arg2-

off, 73 simple-rplus-off, 80 simple-rplus-rzerop, 67 simple-rplus-rzerop-off, 70 simple-rtimes, 53, 54, 66–68 simple-rtimes-off, 80 simple-rtimes-rzerop, 66 simple-rtimes-rzerop-off, 71 single-number-induction, 29 split-by-parity, 81, 88, 89, 95 stupid-hack, 46 stupid-hack-off, 51 subbagp, 1, 2, 4, 5, 8, 9, 36, 47–50,

82–84, 87, 88 subbagp-append, 82 subbagp-append-bridge, 88 subbagp-append-bridge-off, 90 subbagp-append-bridge2, 88 subbagp-append-bridge2-off, 90 subbagp-append-off, 94 subbagp-append-simplify1, 88 subbagp-append-simplify1-off, 91 subbagp-append-simplify2, 88 subbagp-append-simplify2-off, 90 subbagp-bagdiff, 87 subbagp-bagdiff-off, 91 subbagp-bagint1, 5 subbagp-bagint2, 5 subbagp-cdr1, 5 subbagp-cdr2, 5 subbagp-delete, 4 subbagp-delete-car, 83 subbagp-delete-car-off, 94 subbagp-delete-car2, 83 subbagp-delete-car2-off, 94 subbagp-delete-same, 83 subbagp-delete-same-means, 83 subbagp-delete-same-means-off, 94 subbagp-delete-same-off, 94 subbagp-implies-plus-tree-greate

reqp, 8 reqp-off, 13

subbagp-make-negs, 84 subbagp-make-negs-off, 93 subbagp-necc, 83 subbagp-necc-off, 94 subbagp-permutation, 83 subbagp-permutation-equiv, 88 subbagp-permutation-equiv-off, 90 subbagp-permutation-off, 94 subbagp-transitive, 83 subbagp-transitive-bridge, 87 subbagp-transitive-bridge-helpe

r, 87 r-off, 91

subbagp-transitive-bridge-off, 91 subbagp-transitive-off, 94 subbagp-wit-lemma, 82 subbagp-wit-lemma-off, 82 subbagp-x-x, 88 subbagp-x-x-off, 90

times-1-arg1, 16 times-add1, 15 times-distributes-over-differen

ce, 16

ce-proof, 16 times-distributes-over-plus, 15 times-distributes-over-plus-pro

of, 15 times-fringe, 45, 47–50 times-gcd-fact, 60 times-gcd-fact-off, 76 times-quotient, 16 times-quotient-proof, 16 times-sub1, 15 times-tree, 45–50 times-tree-append, 47 times-tree-append-off, 51 times-tree-of-times-fringe, 47 times-tree-of-times-fringe-off, 51 times-zero, 15 transitivity-of-divides, 21 transitivity-of-permutation, 4 transitivity-of-permutation-base

-case, 4 transitivity-of-permutation-ind

uction, 4 uction-step, 4 transitivity-of-requal, 64 transitivity-of-requal-bridge, 64 transitivity-of-requal-bridge-o

ff, 64 ff1, 73

transitivity-of-requal-off, 73 zerop-makes-equal-true-bridge, 49 zerop-makes-equal-true-bridge-o

ff, 52 zerop-makes-lessp-false-bridge, 48 zerop-makes-lessp-false-bridge-

off, 52 zerop-makes-quotient-zero-bridge, 48

-off, 52 zerop-makes-times-tree-zero, 47 zerop-makes-times-tree-zero-off, 51 zerop-makes-times-tree-zero2, 47 zerop-makes-times-tree-zero2-of

f, 51