#|
 Copyright (C) 1994 by Ken Kunen.  All Rights Reserved.
 This script is hereby placed in the public domain, and therefore unlimited
 editing and redistribution is permitted.
 NO WARRANTY
 Ken Kunen PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT IS PROVIDED "AS
 IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING, BUT
 NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU ASSUME THE COST OF
 ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 IN NO EVENT WILL Ken Kunen BE LIABLE TO YOU FOR ANY DAMAGES, ANY LOST
 PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES
 ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT NOT
 LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED
 BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH
 DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#

Event: Start with the initial nqthm theory.

; load initial database
; This file was developed by Ken Kunen, kunen@cs.wisc.edu.  It checks
; the fundamental theorem of arithmetic.  Unlike the proof in the book
; A Compuational Logic and in the file basic.events, Kunen's proof does not
; need auxilliary functions, e.g., gcd.  Why should one be interested
; in this matter?
; In full first order logic, one can show that definitions are
; unnecessary, both in the ``use sense'' that they are ``eliminable''
; from theorems in which they occur and in the ``unnecessary'' sense
; that anything that can be proved with a definition (whose statement
; does not involve that definition) can be proved without the
; definition.
; However, NQTHM does not provide the full power of first order logic.
; It remains an open question, can any Nqthm theorem be proved without
; the definition of concepts not used in the theorem?  Kunen did the

; job for prime factorization.  Can someone else do the job for, say,
; Wilson's theorem?
; Foregoing comments by Robert S. Boyer
; file basic4 -- proof of prime-factorization uniqueness
; no definitions needed except those used to state the theorem,
; EXCEPT the identically 0 function kludge used to
; force the correct induction.
; events in caps were just copied from basic.events
; no attemt to be elegant here, but it works
; time on decstation3100:  [ 22.7 1448.2 29.1 ]

;;;;;;;;;;;  basic defns -- needed to state the uniqueness of prime fact.

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

Definition: prime1 (x, y) = if y ≃ 0 then f

elseif y = 1 then t

else (¬ divides (y, x)) ∧ prime1 (x, y − 1) endif

Definition: prime (x) = ((x ≄ 0) ∧ (x ≠ 1) ∧ prime1 (x, x − 1))

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

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

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

Definition: perm (a, b) = if a ≃ nil then b ≃ nil

elseif car (a) ∈ b then perm (cdr (a), delete (car (a), b))

else f endif

Definition: prime-list (l) = if l ≃ nil then t

else prime (car (l)) ∧ prime-list (cdr (l)) endif Definition: times-list (l) = if l ≃ nil then 1

else car (l) ∗ times-list (cdr (l)) endif

; end defns
; THE GOAL
;    (PROVE-LEMMA PRIME-FACTORIZATION-UNIQUENESS NIL
;                (IMPLIES (AND (PRIME-LIST L1)
;                              (PRIME-LIST L2)
;                              (EQUAL (TIMES-LIST L1)
;                                     (TIMES-LIST L2)))
;                         (PERM L1 L2)))
;

;;;;;;;;;;;;;;;;;;;;;;;;;
;;;   Basic facts about +, *, -
;;;;;;;;;;;;;;;;;;;;;;;;

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

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: lessp-times-1 (i ≄ 0) → ((i ∗ j ) ≮ j )

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

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

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

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

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

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

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

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

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: times-equal-1 ((a ∗ b) = 1) = ((a ≠ 0)

∧ (b ≠ 0)

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  List facts -- pure lists only
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

Theorem: member-delete (x ∈ delete (u, v)) → (x ∈ v)

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

Theorem: lessp-count-delete (n ∈ l) → (count (delete (n, l)) < count (l))

;;; ok to here -- save as basic4a

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;  Quotients, Remainders, Divisibility
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;   !!!!!!!  this one is really important

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-quotient1 ((i ÷ j ) < i) = ((i ≄ 0) ∧ ((j ≃ 0) ∨ (j ≠ 1)))

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

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

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: 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: remainder-0-crock (0 mod y) = 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)

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

Theorem: quotient-divides ((y ∈ N) ∧ ((x ∗ (y ÷ x)) ≠ y)) → ((y mod x) ≠ 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))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Times-list and Prime-list facts -- only stuff that
;;;  doesn't depend on meaning of "prime"
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: times-list-append times-list (append (x, y)) = (times-list (x) ∗ times-list (y))

Theorem: prime-list-append prime-list (append (x, y)) = (prime-list (x) ∧ prime-list (y))

Theorem: prime-list-delete prime-list (l2 ) → prime-list (delete (x, l2 ))

;  ok to here -- save as "basic4b"

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  Primes and their properties
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; as far as possible, try to express theorems in terms of
; divisibility, rather than remainder=0 -- then, in later lemmas,
; we don't have to expand DIVIDES
; ????????? actually, that's not so clear -- divides is still
; expanded, even when it's disabled

Theorem: primes-are-big prime (p) → ((1 < p) = t)

Theorem: little-step-aux1 (prime1 (p, z) ∧ (1 < y) ∧ (y ≤ z)) → (¬ divides (y, p))

Theorem: little-step-aux2 (prime (p) ∧ (1 < y) ∧ (y < p)) → (¬ divides (y, p))

Theorem: little-step-aux3 ((1 < p) ∧ (1 < y) ∧ divides (y, p)) → (y ≤ p)

Theorem: little-step (prime (p) ∧ (1 < y) ∧ (y ≠ p)) → (¬ divides (y, p))

Theorem: exact-remainder-quotient ((x ∈ N) ∧ divides (p, x)) → ((p ∗ (x ÷ p)) = x)

Theorem: divides-product-aux1 divides (p, x) → ((x ∗ y) = (p ∗ ((x ÷ p) ∗ y)))

Theorem: divides-product-aux2 divides (p, p ∗ w) = t

Theorem: divides-product divides (p, x) → divides (p, x ∗ y)

; ok to here -- saved as basic4c

Theorem: divides-sum (divides (p, u + v) ∧ divides (p, v)) → divides (p, u)

; really just a restatement of DIVIDES-PLUS-REWRITE

Theorem: divides-reduction-aux1 (1 < p) → (((p mod b) + (b ∗ (p ÷ b))) = p)

; just a restatement of REMAINDER-QUOTIENT
; now, multiply on left by a:

Theorem: divides-reduction-aux2 (1 < p) → (((a ∗ (p mod b)) + (a ∗ (b ∗ (p ÷ b)))) = (a ∗ p))

; since p divides a*p:

Theorem: divides-reduction-aux3 (1 < p) → divides (p, (a ∗ (p mod b)) + (a ∗ (b ∗ (p ÷ b))))

; now, if p divides a*b, it divides the second term

Theorem: divides-reduction-aux4 divides (p, a ∗ b) → divides (p, a ∗ (b ∗ anything))

; hence:

Theorem: divides-reduction ((1 < p) ∧ divides (p, a ∗ b)) → divides (p, a ∗ (p mod b))

; point of this lemma -- it reduces b to a smaller b', so induction can be used
; basis for induction:

Theorem: prime-divides-small-product-aux1 divides (p, a ∗ 1) → divides (p, a)

; ok

Theorem: prime-divides-small-product-aux2 (prime (p) ∧ (1 < b) ∧ (b < p)) → (0 < (p mod b))

; just a restatement of little-step
; ok to here -- save as "basic4d"

; goal -- prime-divides-small-product is of form:
; (prime p) --> phi(b,p,a)
; we want to prove a lemma saying (prime p) & not(phi(b,p,a)) -->
; remainder(p,b) < b  and not(phi(remainder(p,b),p,a))
; phi is: not( b<p  and 0<b  and divides(p, a*b) and not(divides(p, a)))
; we can't seem to prove the induction lemma all in one step

Theorem: prime-divides-small-product-aux3 (0 < b) → ((1 < b) ∨ (1 = b))

; ok

Theorem: prime-divides-small-product-aux4 ((0 < b) ∧ divides (p, a ∗ b) ∧ (¬ divides (p, a))) → (1 < b)

; ok
; i.e., the the induction lemma is trivial unless 1<b

Theorem: prime-divides-small-product-aux5 (prime (p) ∧ (1 < b)) → ((p mod b) < b)

; ok

Theorem: prime-divides-small-product-aux6 (prime (p) ∧ (1 < b) ∧ (b < p)) → (0 < (p mod b))

; ok

Theorem: prime-divides-small-product-aux7 (prime (p) ∧ (1 < b) ∧ (b < p)) → ((p mod b) < p)

; ok

Theorem: prime-divides-small-product-aux8 (prime (p) ∧ (1 < b) ∧ (b < p) ∧ divides (p, a ∗ b) ∧ (¬ divides (p, a))) → (((p mod b) < b)

∧ (0 < (p mod b)) ∧ ((p mod b) < p) ∧ divides (p, a ∗ (p mod b)) ∧ (¬ divides (p, a)))

; trivially rewrites to T, after 166.6 seconds !!!!!!!!
; the induction lemma -- same as above, but with 1 replaced by 0

Theorem: prime-divides-small-product-aux9 (prime (p) ∧ (0 < b) ∧ (b < p) ∧ divides (p, a ∗ b)

∧ (¬ divides (p, a))) → (((p mod b) < b)

∧ (0 < (p mod b)) ∧ ((p mod b) < p) ∧ divides (p, a ∗ (p mod b)) ∧ (¬ divides (p, a)))

; rewrites trivially to T after 76.3 sec

; we still have to force nqthm to do the right induction

Definition: kludge (b, p) = if ¬ prime (p) then 0

elseif 0 ≮ b then 0

else kludge (p mod b, p) endif

; always returns 0, but now we can use it in an induct hint

Theorem: prime-divides-small-product (prime (p) ∧ divides (p, a ∗ b) ∧ (0 < b) ∧ (b < p)) → divides (p, a)

; ok after 199.1 sec -- probably phrasing some of the auxilliary
; lemmas as rewrite rules would have helped speed things up
;;; ok to here -- save as basic4e
; now, try to replace (b < p) by (not (divides p b))
; idea -- if p divdes a*b, then p divides a*(b mod p) -- if  b mod p
; isn't 0, then it's between 0 and p, so apply prime-divides-small-product
; first step -- prove a variant of divides-reduction, but replacing
; (remainder p b) by (remainder b p)
; i.e.  : divides p (a * b) --> divides p (a * remainder b p)
; say,
; plan
; remainder b p + p * b/p  = fix( b)    (REMAINDER-QUOTENT)
;  a * remainder b p + a * ( p * b/p) = a * b

Theorem: divides-reduction-var-aux1 (b ∈ N) → (((a ∗ (b mod p)) + (a ∗ (p ∗ (b ÷ p)))) = (a ∗ b))

Theorem: divides-reduction-var-aux2 divides (p, p ∗ anything)

Theorem: divides-reduction-var-aux3 (a ∗ (p ∗ anything)) = (p ∗ (a ∗ anything))

Theorem: divides-reduction-var-aux4 divides (p, a ∗ (p ∗ anything))

Theorem: divides-reduction-var ((b ∈ N) ∧ divides (p, a ∗ b)) → divides (p, a ∗ (b mod p))

; ok to here -- save as basic4f

Theorem: prime-divides-product-aux1 ((b mod p) ≠ 0) → ((0 < (b mod p)) = t)

Theorem: prime-divides-product-aux2 prime (p) → (((b mod p) < p) = t)

Theorem: prime-divides-product (prime (p) ∧ divides (p, a ∗ b) ∧ (¬ divides (p, b))) → divides (p, a)

;;;;;;;;  THIS is the key lemma -- the rest should be just list-hacking

Theorem: car-divides-times-list listp (l) → divides (car (l), times-list (l))

Theorem: divides-equal (prime (p) ∧ prime (q) ∧ divides (p, q)) → ((p = q) = t)

; following should be trivial by times-divides-product

Theorem: prime-divides-list-aux1 (prime-list (l) ∧ prime (p) ∧ listp (l) ∧ divides (p, times-list (l)) ∧ (¬ divides (p, times-list (cdr (l))))) → divides (p, car (l))

Event: Disable prime-divides-small-product-aux1.

Event: Disable prime-divides-small-product-aux2.

Event: Disable prime-divides-small-product.

; these auxilliaries are getting in the way

Theorem: prime-divides-list-aux2 (prime-list (l) ∧ prime (p) ∧ listp (l) ∧ divides (p, times-list (l)) ∧ (¬ divides (p, times-list (cdr (l))))) → (car (l) = p)

; ok

Event: Disable prime-divides-list-aux1.

; basis of induction

Theorem: prime-divides-list-aux3 (prime (p) ∧ (l ≃ nil)) → (¬ divides (p, times-list (l)))

; ok

; so it can see the trivial induction:

Theorem: prime-divides-list-aux4 (prime-list (l) ∧ prime (p) ∧ divides (p, times-list (l))) → (listp (l) ∧ ((car (l) = p) ∨ divides (p, times-list (cdr (l)))))

; ok

Event: Disable prime-divides-list-aux2.

Event: Disable prime-divides-list-aux3.

; now, by a simple induction on L:

Theorem: prime-divides-list (prime-list (l) ∧ prime (p) ∧ divides (p, times-list (l))) → (p ∈ l)

; ok

;;; two lemmas from basic.events now follow trivially

Theorem: prime-list-times-list (prime (c) ∧ prime-list (l2 ) ∧ (c ∉ l2 )) → ((times-list (l2 ) mod c) ≠ 0)

Theorem: prime-member (((c ∗ times-list (l1 )) = times-list (l2 )) ∧ prime (c) ∧ prime-list (l2 )) → (c ∈ l2 )

;;;;; some more lemmas about lists and producs
; this is the base case in PRIME-FACTORIZATION-UNIQUENESS

Theorem: void-case (prime-list (l) ∧ (1 = times-list (l))) → (l ≃ nil)

; ok

Theorem: product-delete (x ∈ l) → (times-list (l) = (x ∗ times-list (delete (x, l))))

; ok

Theorem: times-cancellation ((0 < p) ∧ ((p ∗ x) = (p ∗ y))) → (fix (x) = fix (y))

; ok

Theorem: number-times-cancellation ((x ∈ N) ∧ (y ∈ N) ∧ (0 < p) ∧ ((p ∗ x) = (p ∗ y))) → ((x = y) = t)

; ok

Theorem: products-are-numbers (times-list (l) ∈ N) = t

; ok
; changed

Theorem: divide-by-member-aux1 ((p ∈ l) ∧ ((p ∗ x) = times-list (l))) → ((p ∗ times-list (delete (p, l))) = (p ∗ x))

; ok
; next is just a kludge to force final rewrite
; with hypotheses stated in exact form required

Theorem: divide-by-member-aux2 (((p ∗ x) = times-list (l)) ∧ (x ∈ N) ∧ (p ≠ 0) ∧ (p ∈ N) ∧ (times-list (l) = (p ∗ times-list (delete (p, l))))) → (times-list (delete (p, l)) = x)

; trivially, we should have now:

Theorem: divide-by-member ((x ∈ N) ∧ (p ∈ l) ∧ (0 < p) ∧ ((p ∗ x) = times-list (l))) → (times-list (delete (p, l)) = x)

; ok

Theorem: divide-by-prime-member-aux1 (prime-list (l) ∧ (p ∈ l)) → prime (p)

; since primes are positive:

Theorem: divide-by-prime-member ((x ∈ N) ∧ prime-list (l) ∧ (p ∈ l) ∧ ((p ∗ x) = times-list (l))) → (times-list (delete (p, l)) = x)

; ok
; should handle induction case in prime factorization uniqueness

Theorem: reduct-product (prime-list (l1 ) ∧ prime-list (l2 ) ∧ (times-list (l1 ) = times-list (l2 )) ∧ listp (l1 ) ∧ (car (l1 ) ∈ l2 )) → (times-list (delete (car (l1 ), l2 )) = times-list (cdr (l1 )))

; ok

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; On to the goal:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Event: Disable divides-equal.

Event: Disable divide-by-prime-member-aux1.

Theorem: prime-factorization-uniqueness-aux1 (prime-list (l) ∧ listp (l)) → (1 < times-list (l))

; a trivial variant:

Theorem: prime-factorization-uniqueness-aux2 (prime-list (l) ∧ (1 = times-list (l))) → (¬ listp (l))

Event: Disable product-delete.

; seems to require some hints in our present setting

Theorem: prime-factorization-uniqueness (prime-list (l1 ) ∧ prime-list (l2 ) ∧ (times-list (l1 ) = times-list (l2 ))) → perm (l1 , l2 )

Index

associativity-of-plus, 3 associativity-of-times, 4

car-divides-times-list, 13 commutativity-of-delete, 6 commutativity-of-plus, 3 commutativity-of-times, 4 commutativity2-of-plus, 3 commutativity2-of-times, 4

delete, 2, 6, 8, 15–17 delete-non-member, 6 difference-0, 4 difference-add1-cancellation, 5 difference-cancellation-0, 4 difference-cancellation-1, 4 difference-elim, 5 difference-plus, 4 difference-plus-cancelation, 5 difference-plus1, 5 difference-plus2, 5 difference-plus3, 5 difference-x-x, 3 distributivity-of-divides, 8 distributivity-of-times-over-pl

us, 4 divide-by-member, 16 divide-by-member-aux1, 16 divide-by-member-aux2, 16 divide-by-prime-member, 16 divide-by-prime-member-aux1, 16 divides, 2, 7–15 divides-equal, 13 divides-plus-rewrite, 7 divides-plus-rewrite-commuted, 7 divides-plus-rewrite1, 7 divides-plus-rewrite2, 7 divides-product, 9 divides-product-aux1, 9 divides-product-aux2, 9 divides-reduction, 10 divides-reduction-aux1, 9 divides-reduction-aux2, 9 divides-reduction-aux3, 10 divides-reduction-aux4, 10 divides-reduction-var, 13 divides-reduction-var-aux1, 13 divides-reduction-var-aux2, 13 divides-reduction-var-aux3, 13 divides-reduction-var-aux4, 13 divides-sum, 9 divides-times, 7 divides-times1, 8

equal-difference-0, 4

equal-lessp, 4 equal-times-0, 4 euclid, 7 exact-remainder-quotient, 9

kludge, 12

lessp-count-delete, 6 lessp-plus-cancelation, 5 lessp-plus-cancellation3, 5 lessp-quotient1, 7 lessp-remainder1, 7 lessp-remainder2, 7 lessp-times-1, 5 lessp-times-2, 5 lessp-times-cancellation, 5 little-step, 9 little-step-aux1, 9 little-step-aux2, 9 little-step-aux3, 9

member-delete, 6

number-times-cancellation, 15

perm, 2, 17 plus-add1, 3 plus-cancellation, 4 plus-equal-0, 3 plus-right-id2, 3 prime, 2, 9–16 prime-divides-list, 15 prime-divides-list-aux1, 13 prime-divides-list-aux2, 14 prime-divides-list-aux3, 14 prime-divides-list-aux4, 14 prime-divides-product, 13 prime-divides-product-aux1, 13 prime-divides-product-aux2, 13 prime-divides-small-product, 12 prime-divides-small-product-aux

1, 10 2, 10 3, 10 4, 11 5, 11 6, 11 7, 11 8, 11 9, 11

prime-factorization-uniqueness, 17 prime-factorization-uniqueness-

aux1, 17 aux2, 17

prime-list, 2, 8, 13–17 prime-list-append, 8 prime-list-delete, 8 prime-list-times-list, 15 prime-member, 15 prime1, 2, 9 primes-are-big, 9 product-delete, 15 products-are-numbers, 16

quotient-divides, 8 quotient-lessp, 8 quotient-times, 8 quotient-times1, 7

reduct-product, 17 remainder-0-crock, 7 remainder-add1, 7 remainder-quotient, 6 remainder-quotient-elim, 7 remainder-wrt-1, 6 remainder-wrt-12, 6 remainder-x-x, 7

times-add1, 4

times-cancellation, 15 times-difference, 5 times-equal-1, 6 times-id-iff-1, 5 times-identity, 5 times-identity1, 5 times-list, 3, 8, 13–17 times-list-append, 8 times-zero2, 4

void-case, 15