Event: Start with the initial nqthm theory.

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

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

else 1 + x endif

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

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

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

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

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

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

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

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

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

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

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

elseif z < y then y ≮ x else fix (x) = fix (z) endif Theorem: times-zero2 (y ∉ N) → ((x ∗ y) = 0)

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

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

else fix (x) endif

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

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

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

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

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

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

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

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

else f = z endif

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

elseif w = z then t

else greatereqpr (w − 1, z) endif

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

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

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

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

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

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

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

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

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

else fix (x) endif

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

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

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

∧ (b ≠ 0)

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

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

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

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

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

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

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

else 0 endif

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

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

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

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

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

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

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

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

else 1 endif

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

else 0 endif

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

Theorem: remainder-difference-times (((p ∗ x) − (p ∗ y)) mod p) = 0 Theorem: lessp-remainder-divisor (y ≄ 0) → ((x mod y) < y)

Event: Make the library "arith".

Index

associativity-of-plus, 1 associativity-of-times, 2

commutativity-of-plus, 1 commutativity-of-times, 2 commutativity2-of-plus, 1 commutativity2-of-times, 2

difference-0, 1 difference-1, 5 difference-2, 5 difference-add1-cancellation, 3 difference-cancellation-0, 1 difference-cancellation-1, 1 difference-elim, 2 difference-plus, 1 difference-plus-cancelation, 3 difference-plus1, 3 difference-plus2, 3 difference-plus3, 3 difference-x-x, 1 distributivity-of-divides, 5 distributivity-of-times-over-pl

us, 2 divides, 3–5 divides-implies-times, 5 divides-plus-rewrite, 4 divides-plus-rewrite-commuted, 4 divides-plus-rewrite1, 4 divides-plus-rewrite2, 4 divides-times, 3 divides-times1, 5

equal-difference-0, 1 equal-length-0, 6 equal-lessp, 2 equal-times-0, 2 euclid, 4 exp, 2, 6 exp-by-0, 6 exp-exp, 6 exp-of-0, 6 exp-of-1, 6 exp-plus, 2 exp-times, 6

greatereqpr, 4, 5 greatereqpr-lessp, 4 greatereqpr-remainder, 5

half-plus, 6

if-times-then-divides, 5

length, 6

lessp-plus-cancelation, 4 lessp-plus-cancellation3, 4 lessp-quotient1, 3 lessp-remainder-divisor, 7 lessp-remainder1, 3 lessp-remainder2, 3 lessp-times-1, 3 lessp-times-2, 3 lessp-times-cancellation, 4

plus-add1, 1

plus-cancellation, 1 plus-equal-0, 1 plus-right-id2, 1

quotient-divides, 5 quotient-lessp, 4 quotient-times, 5 quotient-times1, 4

remainder-add1, 3

remainder-difference-times, 6 remainder-of-1, 6 remainder-plus-times-1, 6 remainder-plus-times-2, 6 remainder-quotient, 2 remainder-quotient-elim, 3 remainder-times, 5 remainder-times-1, 6 remainder-wrt-1, 2 remainder-wrt-12, 2 remainder-x-x, 3

times-1, 6 times-add1, 2 times-difference, 3 times-equal-1, 5 times-id-iff-1, 4 times-identity, 5 times-identity1, 5 times-zero2, 2