Event: Start with the initial thm theory.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                    ;;
;;                       SUBSIDIARY FUNCTIONS                         ;;
;;                                                                    ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; I suspect that many of these lemmas are not necessary but I'm keeping
;; them for now.  I'll eliminate many of them later as I see that they
;; are not needed.
;; I'm adopting the convention that all alist components are cons
;; pairs.  That is, of the form (x . y) not of the form (x y).

Definition: name (exp) = car (exp)

Event: Disable name.

Theorem: name-expansion name (cons (x, y)) = x

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

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

else assoc (x, cdr (y)) endif else f endif

Theorem: assoc-value1 assoc (x, cons (cons (x, y), z)) = cons (x, y)

Definition: value (name, alist) = cdr (assoc (name, alist))

Theorem: value-expansion3 value (x, cons (cons (x, z), alist)) = z

Theorem: value-expansion2 (x ≠ y) → (value (x, cons (cons (y, z), alist)) = value (x, alist))

Event: Disable value.

Definition: max (x, y) = if x < y then y

else x endif

Definition: append (x, y) = if listp (x) then cons (car (x), append (cdr (x), y))

else y endif

Theorem: append-cons-rewrite append (cons (x, y), z) = cons (x, append (y, z))

Theorem: append-nil-lemma append (nil, x) = x

Theorem: assoc-not-affected-by-extra-element (y ≠ car (x)) → (assoc (y, append (lst1 , cons (x, lst2 ))) = assoc (y, append (lst1 , lst2 )))

Definition: plistp (x) = if x ≃ nil then x = nil

else plistp (cdr (x)) endif

Definition: length-plistp (lst, n) = (plistp (lst) ∧ (length (lst) = n))

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

Theorem: length-distributes length (append (lst1 , lst2 )) = (length (lst1 ) + length (lst2 ))

Theorem: not-zerop-length-listp (length (x) ≄ 0) → listp (x)

Event: Disable not-zerop-length-listp.

Theorem: length-cons length (cons (x, y)) = (1 + length (y))

Event: Disable length-cons.

Theorem: append-rewrite2 (append (x, y) = append (x, z)) = (y = z)

Theorem: append-cons-rewrite2 (cons (x, y) = cons (x, z)) = (y = z)

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

Definition: reverse (x) = if listp (x) then append (reverse (cdr (x)), list (car (x)))

else nil endif

Theorem: reverse-preserves-length length (reverse (lst)) = length (lst)

Theorem: reverse-plistp plistp (reverse (lst))

Theorem: reverse-reverse plistp (lst) → (reverse (reverse (lst)) = lst)

Theorem: listp-implies-non-zero-length listp (x) → (length (x) ≠ 0)

Definition: subset (x, y) = if x ≃ nil then t

else (car (x) ∈ y) ∧ subset (cdr (x), y) endif

Theorem: superset-preserves-membership (subset (x, y) ∧ (z ∈ x)) → (z ∈ y)

Event: Disable superset-preserves-membership.

Theorem: cons-preserves-subset subset (x, y) → subset (x, cons (z, y))

Event: Disable cons-preserves-subset.

Theorem: subset-reflexive subset (y, y)

Theorem: cons-preserves-subset2 subset (y, cons (x, y))

Theorem: subset-distributes subset (append (x, y), z) = (subset (x, z) ∧ subset (y, z))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                                      ;;
;;                         ALIST FUNCTIONS                              ;;
;;                                                                      ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: listcars (lst) = if lst ≃ nil then nil

else cons (car (car (lst)), listcars (cdr (lst))) endif

Theorem: listcars-plistp plistp (listcars (x))

Theorem: cons-distributes-over-listcars listcars (cons (x, y)) = cons (car (x), listcars (y))

Theorem: listcars-distributes listcars (append (x, y)) = append (listcars (x), listcars (y))

Theorem: listcars-preserves-length length (listcars (lst)) = length (lst)

Theorem: not-member-listcars-not-assoc (x ∉ listcars (lst)) → (assoc (x, lst) = f)

Theorem: member-listcars-assoc (x ∉ listcars (lst2 )) → (assoc (x, append (lst2 , lst3 )) = assoc (x, lst3 ))

Definition: no-duplicates (lst) = if lst ≃ nil then t

elseif car (lst) ∈ cdr (lst) then f else no-duplicates (cdr (lst)) endif

Theorem: no-duplicates-append no-duplicates (append (x, y)) → (no-duplicates (x) ∧ no-duplicates (y))

Theorem: no-duplicates-append-append no-duplicates (append (x, append (y, z))) → no-duplicates (append (x, z))

Event: Disable no-duplicates-append-append.

Theorem: no-duplicates-member2 (no-duplicates (append (lst1 , lst2 )) ∧ (x ∈ lst1 )) → ((x ∈ lst2 ) = f)

Event: Disable no-duplicates-member2.

Theorem: subset-preserves-no-duplicates (no-duplicates (append (x, y)) ∧ no-duplicates (z) ∧ subset (z, y)) → no-duplicates (append (x, z))

Event: Disable subset-preserves-no-duplicates.

Theorem: no-duplicates-cons-append2 no-duplicates (cons (x, append (y, z))) → no-duplicates (cons (x, z))

Event: Disable no-duplicates-cons-append2.

Theorem: no-duplicates-member-append2 no-duplicates (append (a, cons (x, b))) → no-duplicates (append (a, b))

Theorem: no-duplicates-duplication ((x ∈ lst1 ) ∧ (x ∈ lst2 )) → (no-duplicates (append (lst1 , lst2 )) = f)

Theorem: no-duplicates-cons-append ((x ∉ lst1 ) ∧ (x ∉ lst2 ) ∧ no-duplicates (append (lst1 , lst2 ))) → no-duplicates (append (lst1 , cons (x, lst2 )))

Event: Disable no-duplicates-cons-append.

Theorem: append-plistp-nil-lemma plistp (x) → (append (x, nil) = x)

Theorem: no-duplicates-commutes-append (plistp (x) ∧ plistp (y) ∧ no-duplicates (append (x, y))) → no-duplicates (append (y, x))

Event: Disable no-duplicates-commutes-append.

Theorem: member-cons (x ≠ y) → ((x ∈ cons (y, z)) = (x ∈ z))

Definition: all-cars-unique (lst) = no-duplicates (listcars (lst))

Theorem: cars-unique-cars-unique (all-cars-unique (cons (y, lst)) ∧ (x ∈ lst)) → (car (x) ≠ car (y))

Event: Disable cars-unique-cars-unique.

Theorem: assoc-unique-member ((x ∈ lst) ∧ all-cars-unique (lst)) → (assoc (car (x), lst) = x)

Theorem: no-duplicates-member-cons no-duplicates (append (x, cons (y, z))) → (y ∉ z)

Event: Disable no-duplicates-member-cons.

Theorem: all-cars-unique-commutes-append (plistp (x) ∧ plistp (y) ∧ all-cars-unique (append (x, y))) → all-cars-unique (append (y, x))

Event: Disable all-cars-unique-commutes-append.

Theorem: cars-unique-cons all-cars-unique (cons (x, cons (y, z))) → all-cars-unique (cons (x, z))

Event: Disable cars-unique-cons.

Theorem: cons-car-append-all-cars-unique (listp (x) ∧ all-cars-unique (append (x, y))) → all-cars-unique (cons (car (x), y))

Theorem: member-car-listcars (x ∈ y) → (car (x) ∈ listcars (y))

Theorem: cars-unique-names-unique (all-cars-unique (append (z, w)) ∧ (x ∈ z) ∧ (y ∈ w)) → (car (x) ≠ car (y))

Event: Disable cars-unique-names-unique.

Event: Disable all-cars-unique.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                   ARITHMETIC FUNCTIONS                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: exp (x, y) = if y ≃ 0 then 1

else x ∗ exp (x, y − 1) endif Definition: integerp (x) = ((negativep (x) ∧ (negative-guts (x) ≠ 0)) ∨ (x ∈ N))

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

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

else t endif elseif negativep (y) then f else x < y endif

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

then if negativep (j ) then − (negative-guts (i) + negative-guts (j )) elseif j < negative-guts (i) then − (negative-guts (i) − j ) else j − negative-guts (i) endif

elseif negativep (j )

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

else i − negative-guts (j ) endif else i + j endif

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

elseif i ≃ 0 then 0

else − i endif

Definition: idifference (i, j ) = iplus (i, inegate (j ))

Definition: ileq (x, y) = (¬ ilessp (y, x))

Theorem: zero-iplus-identity integerp (n) → (iplus (0, n) = n)

Theorem: iplus-integerp (integerp (n) ∧ integerp (m)) → integerp (iplus (n, m))

Event: Disable iplus-integerp.

Theorem: plus-commutes (x + y) = (y + x)

Event: Disable plus-commutes.

Theorem: plus-0-rewrite (x + 0) = fix (x)

Theorem: plus-add1 (x + 1) = (1 + x)

Event: Disable plus-add1.

Theorem: times-m-rewrite (m ∗ (1 + n)) = (m + (m ∗ n))

Event: Disable times-m-rewrite.

Theorem: plus-add1-commute (x + (1 + n)) = (1 + (x + n))

Event: Disable plus-add1-commute.

Theorem: add1-preserves-lessp (n < m) → ((n < (1 + m)) = t)

Event: Disable add1-preserves-lessp.

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

Theorem: plus-equality-lemma1 (m = k) → (((n + m) = (n + k)) = t)

Event: Disable plus-equality-lemma1.

Theorem: difference-rewrite (y < x) → ((x − y) = (1 + (x − (1 + y))))

Event: Disable difference-rewrite.

Theorem: sub1-preserves-lessp (x < y) → (((x − 1) < y) = t)

Theorem: add1-difference (j ≤ k) → (((1 + k) − j ) = (1 + (k − j )))

Theorem: add1-sub1-difference (((1 + x) − y) − 1) = (x − y)

Theorem: difference-add1 ((1 + n) − n) = 1

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

Theorem: plus-0-rewrite2 (n ≃ 0) → ((m + n) = fix (m))

Theorem: plus-add1-sub1 (m ≄ 0) → (((1 + n) + (m − 1)) = (n + m))

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

Theorem: difference-n-leq (n ≄ 0) → ((((n − m) − 1) < n) = t)

Event: Disable difference-n-leq.

Theorem: plus-preserves-lessp ((x + y) < z) → ((x < z) = t)

Theorem: plus-preserves-lessp2 (x < y) → ((x < (n + y)) = t)

Theorem: lessp-transitive ((x < y1 ) ∧ (y2 ≮ y1 )) → ((x < y2 ) = t)

Event: Disable lessp-transitive.

Theorem: difference-lessp (x < (y − z)) → ((z < y) = t)

Event: Disable difference-lessp.

Theorem: plus-preserves-lessp3 (n ≄ 0) → ((k < (n + k)) = t)

Event: Disable plus-preserves-lessp3.

Theorem: difference-difference-plus ((n ≮ l) ∧ (k ≮ n)) → ((k − (n − l)) = (l + (k − n)))

Event: Disable difference-difference-plus.

Theorem: zerop-difference-lessp (m < n) → (((n − m) = 0) = f)

Event: Disable zerop-difference-lessp.

Theorem: add1-difference2 (y < x) → ((x − (1 + y)) = ((x − y) − 1))

Event: Disable add1-difference2.

Theorem: sub1-plus5 (y ≄ 0) → ((x + (y − 1)) = ((x + y) − 1))

Event: Disable sub1-plus5.

Theorem: sub1-plus4 ((x ≄ 0) ∧ (y ≄ 0)) → (((x − 1) + y) = (x + (y − 1)))

Theorem: difference-lessp2 ((x + y + z) < (m − n)) → ((m < (x + y + z + n)) = f)

Theorem: plus-times-3 (k ≄ 0) → (((k ∗ 3) + n) = (1 + (1 + (1 + (((k − 1) ∗ 3) + n)))))

Theorem: zero-iplus-right-identity integerp (x) → (iplus (x, 0) = x)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                    MISCELLANEOUS STUFF                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: nth (x, n) = if n ≃ 0 then x

else nth (cdr (x), n − 1) endif

;; Index is used for converting the current condition to a numeric
;; value for the lower level state.

Definition: index (y, lst) = if lst ≃ nil then 0

elseif y = car (lst) then 1

else 1 + index (y, cdr (lst)) endif

Theorem: member-implies-nonzero-index (c ∈ cond-list) → (index (c, cond-list) ≠ 0)

Event: Disable member-implies-nonzero-index.

Theorem: member-index-lessp-length index (c, cond-list) < (1 + length (cond-list))

Event: Disable member-index-lessp-length.

Theorem: lessp-member-index-length (x ∈ lst) → ((index (x, lst) < (1 + length (lst))) = t)

Theorem: index-length (length (lst) < (n − 1)) → ((index (x, lst) < n) = t)

Event: Disable index-length.

Theorem: nth-index-elimination (x ∈ lst) → (car (nth (lst, index (x, lst) − 1)) = x)

Event: Disable nth-index-elimination.

Theorem: subset-append1 subset (x, y) → (subset (x, append (y, z)) ∧ subset (x, append (z, y)))

Theorem: reorder-subset subset (cons (x, append (y, z)), append (y, cons (x, z)))

Event: Disable reorder-subset.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       PLISTP LEMMAS                         ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: plistp-cons plistp (cons (x, y)) = plistp (y)

Theorem: plistp-append plistp (append (x, y)) = plistp (y)

Theorem: plistp-atom (x ≃ nil) → (plistp (x) = (x = nil))

Theorem: zero-length-plistp-nil (plistp (x) ∧ (length (x) = 0)) → ((x = nil) = t)

Event: Disable zero-length-plistp-nil.

Theorem: cddr-length-plistp-2 length-plistp (x, 2) → (cddr (x) = nil)

Theorem: reverse-append-reverse1 (plistp (x) ∧ plistp (y)) → (reverse (append (x, y)) = append (reverse (y), reverse (x)))

Theorem: reverse-append-reverse (plistp (lst1 ) ∧ plistp (lst2 )) → (reverse (append (reverse (lst1 ), reverse (lst2 ))) = append (lst2 , lst1 ))

Event: Disable reverse-append-reverse.

Theorem: append-doesnt-affect-value4 (x ∉ listcars (z)) → (assoc (x, append (y, z)) = assoc (x, y))

Event: Disable append-doesnt-affect-value4.

Event: Disable length-plistp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                     GET and PUT LEMMAS                      ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: get (n, lst) = if n ≃ 0 then car (lst)

else get (n − 1, cdr (lst)) endif Theorem: get-0 get (0, cons (x, y)) = x

Theorem: get-add1 get (1 + n, cons (x, y)) = get (n, y)

Theorem: get-length-cons (n ≄ 0) → (get (n, cons (x, lst)) = get (n − 1, lst))

Theorem: get-length-car1 get (length (lst), append (lst, lst2 )) = car (lst2 )

Event: Disable get-length-car1.

Theorem: get-length-car (n = length (lst)) → (get (n, append (lst, lst2 )) = car (lst2 ))

Theorem: get-length-plus (n = length (lst1 )) → (get (n + m, append (lst1 , lst2 )) = get (m, lst2 ))

Theorem: get-car (n ≃ 0) → (get (n, lst) = car (lst))

Theorem: get-sub1 (n ≄ 0) → (get (n, lst) = get (n − 1, cdr (lst)))

Theorem: get-append (k < length (lst1 )) → (get (k, append (lst1 , lst2 )) = get (k, lst1 ))

Theorem: get-add1-add1-append get (n + (1 + (1 + m)), cons (x, cons (y, lst))) = get (n + m, lst)

Theorem: get-add1-length-plus ((length (lst1 ) = (1 + n)) ∧ (m ≄ 0)) → (get (n + m, append (lst1 , lst2 )) = get (m − 1, lst2 ))

Theorem: get-add1-plus get ((1 + n) + m, cons (x, y)) = get (n + m, y)

Theorem: get-0-plus get (0 + n, y) = get (n, y)

Definition: put (val, n, lst) = if n ≃ 0

then if listp (lst) then cons (val, cdr (lst))

else list (val) endif else cons (car (lst), put (val, n − 1, cdr (lst))) endif Theorem: put-car-nlistp ((n ≃ 0) ∧ (lst ≃ nil)) → (put (val, n, lst) = list (val))

Theorem: put-car-listp ((n ≃ 0) ∧ listp (lst)) → (put (val, n, lst) = cons (val, cdr (lst)))

Theorem: put-preserves-plistp plistp (lst) → plistp (put (val, n, lst))

Theorem: get-inverts-put get (y, put (x, y, z)) = x

Definition: put-assoc (val, name, alist) = if alist ≃ nil then alist

elseif name = caar (alist) then cons (cons (name, val), cdr (alist)) else cons (car (alist), put-assoc (val, name, cdr (alist))) endif

Theorem: put-assoc-expansion put-assoc (x, y, cons (cons (y, z), w)) = cons (cons (y, x), w)

Definition: definedp (name, alist) = if alist ≃ nil then f

elseif name = caar (alist) then t else definedp (name, cdr (alist)) endif

Theorem: member-defined-name (x ∈ y) → definedp (car (x), y)

Theorem: definedp-car-assoc definedp (x, lst) → (car (assoc (x, lst)) = x)

Theorem: definedp-car-cons definedp (x, cons (cons (x, y), z))

Theorem: definedp-implies-member (x ∈ listcars (y)) = definedp (x, y)

Event: Disable definedp-implies-member.

Theorem: definedp-member-assoc definedp (x, lst) → (assoc (x, lst) ∈ lst)

Theorem: definedp-rewrites-to-member definedp (x, lst) = (x ∈ listcars (lst))

Event: Disable definedp-rewrites-to-member.

Theorem: definedp-distributes definedp (x, append (y, z)) = (definedp (x, y) ∨ definedp (x, z))

Theorem: definedp-append-preserves-assoc definedp (x, y) → (assoc (x, append (y, z)) = assoc (x, y))

Event: Disable definedp-append-preserves-assoc.

Theorem: definedp-once (all-cars-unique (append (y, z)) ∧ definedp (x, z)) → (¬ definedp (x, y))

Event: Disable definedp-once.

Theorem: not-definedp-assoc-append (¬ definedp (x, y)) → (assoc (x, append (y, z)) = assoc (x, z))

Theorem: put-preserves-length (y < length (z)) → (length (put (x, y, z)) = length (z))

Theorem: multiple-puts-cancel put (x, y, put (z, y, w)) = put (x, y, w)

Theorem: puts-commute ((y ∈ N) ∧ (v ∈ N) ∧ (y < length (z)) ∧ (v < length (z)) ∧ (v ≠ y)) → (put (x, y, put (u, v, z)) = put (u, v, put (x, y, z)))

Event: Disable puts-commute.

Theorem: put-never-shrinks (length (put (x, y, z)) < length (z)) = f

Theorem: put-value-length-rewrite (n = length (lst1 )) → (put (value, n, append (lst1 , cons (value2 , lst2 )))

= append (lst1 , cons (value, lst2 )))

Event: Disable put-value-length-rewrite.

Theorem: put-length (n = length (lst)) → (put (x, n, append (lst, cons (y, lst2 ))) = append (lst, cons (x, lst2 )))

Event: Disable put-length.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                         RESTRICT                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Given an alist, select the sub-alist with names in a given list.
;; This will allow me to select out, for example, the sub-alist relating to
;; the locals or formals.

Definition: restrict (alist, names) = if alist ≃ nil then nil

elseif caar (alist) ∈ names

then cons (car (alist), restrict (cdr (alist), names))

else restrict (cdr (alist), names) endif

Theorem: restriction-nil-names (names ≃ nil) → (restrict (alist, names) = nil)

Theorem: no-duplicates-restriction no-duplicates (cons (x, listcars (alist))) → (restrict (alist, cons (x, names)) = restrict (alist, names))

Event: Disable no-duplicates-restriction.

Theorem: restriction-names-cdr (no-duplicates (names) ∧ no-duplicates (listcars (alist)) ∧ (caar (alist) = car (names))) → (restrict (cdr (alist), names) = restrict (cdr (alist), cdr (names)))

Event: Disable restriction-names-cdr.

Theorem: restrict-alist-listcars (plistp (alist) ∧ no-duplicates (listcars (alist))) → (restrict (alist, listcars (alist)) = alist)

Event: Disable restrict-alist-listcars.

Theorem: restrict-listcars-member (x ∉ y) → (x ∉ listcars (restrict (lst, y)))

Definition: restriction-induction-hint (alist, names1 , names2 ) = if alist ≃ nil then t

elseif caar (alist) ∈ names1

then restriction-induction-hint (cdr (alist), cdr (names1 ), names2 ) else restriction-induction-hint (cdr (alist), names1 , cdr (names2 )) endif

Theorem: listcars-restriction-append ((listcars (alist) = append (names1 , names2 )) ∧ no-duplicates (listcars (alist)) ∧ plistp (alist)) → (append (restrict (alist, names1 ), restrict (alist, names2 )) = alist)

Event: Disable listcars-restriction-append.

Theorem: restriction-plistp plistp (restrict (x, y))

Theorem: assoc-restriction (x ∈ y) → (assoc (x, restrict (z, y)) = assoc (x, z))

Event: Disable assoc-restriction.

Theorem: no-duplicates-append-restrict no-duplicates (append (names, listcars (lst))) → (restrict (append (x, lst), names) = restrict (x, names))

Event: Disable no-duplicates-append-restrict.

Definition: double-cdr-induction (x, y) = if x ≃ nil then t

else double-cdr-induction (cdr (x), cdr (y)) endif

Theorem: restrict-matching-listcars (plistp (lst) ∧ (names = listcars (lst)) ∧ no-duplicates (listcars (lst))) → (restrict (lst, names) = lst)

Event: Disable restrict-matching-listcars.

Theorem: restrict-append2 no-duplicates (append (listcars (lst1 ), names)) → (restrict (append (lst1 , lst2 ), names) = restrict (lst2 , names))

Event: Disable restrict-append2.

Theorem: restrict-restricts-listcars (x ∉ listcars (y)) → (x ∉ listcars (restrict (y, z)))

Theorem: restriction-cdr (listp (y) ∧ (car (y) ∉ listcars (x))) → (restrict (x, y) = restrict (x, cdr (y)))

Event: Disable restriction-cdr.

Theorem: restrict-append (listp (y) ∧ (listcars (x) = append (y, z)) ∧ all-cars-unique (x)) → (restrict (x, y) = cons (car (x), restrict (cdr (x), cdr (y))))

Event: Disable restrict-append.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       SIGNATURES                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: signatures-match (alist1 , alist2 ) = if alist1 ≃ nil then alist2 = nil

else (caar (alist1 ) = caar (alist2 )) ∧ (cadr (car (alist1 )) = cadr (car (alist2 ))) ∧ signatures-match (cdr (alist1 ), cdr (alist2 )) endif

Theorem: signatures-match-reflexive plistp (lst) → signatures-match (lst, lst)

Theorem: signatures-match-reflexive1 signatures-match (lst, lst) = plistp (lst)

Theorem: signatures-match-symmetric (plistp (lst1 ) ∧ signatures-match (lst1 , lst2 )) → signatures-match (lst2 , lst1 )

Event: Disable signatures-match-symmetric.

Theorem: signatures-match-transitive (plistp (lst1 ) ∧ signatures-match (lst1 , lst2 ) ∧ signatures-match (lst2 , lst3 )) → signatures-match (lst1 , lst3 )

Event: Disable signatures-match-transitive.

Theorem: signatures-match-listp (signatures-match (x, y) ∧ listp (x)) → listp (y)

Event: Disable signatures-match-listp.

Theorem: signatures-match-listcars signatures-match (x, y) → (listcars (y) = listcars (x))

Event: Disable signatures-match-listcars.

Theorem: signatures-match-append1 (signatures-match (lst1 , lst3 ) ∧ signatures-match (lst2 , lst4 )) → signatures-match (append (lst1 , lst2 ), append (lst3 , lst4 ))

Event: Disable signatures-match-append1.

Theorem: signatures-match-reorder (plistp (alist1 ) ∧ signatures-match (alist1 , alist3 ) ∧ signatures-match (alist1 , alist2 )) → signatures-match (alist2 , alist3 )

Event: Disable signatures-match-reorder.

Definition: signature (mg-vars-list) = if mg-vars-list ≃ nil then nil

else cons (list (caar (mg-vars-list), cadar (mg-vars-list)), signature (cdr (mg-vars-list))) endif

Theorem: signatures-match-listcars-equal signatures-match (x, y) → (listcars (y) = listcars (x))

Event: Disable signatures-match-listcars-equal.

Theorem: signatures-match-preserves-uniqueness-of-cars (signatures-match (x, y) ∧ all-cars-unique (x)) → all-cars-unique (y)

Event: Disable signatures-match-preserves-uniqueness-of-cars.

Theorem: signature-restrict-commute signature (restrict (alist, names)) = restrict (signature (alist), names)

Event: Disable signature-restrict-commute.

Theorem: signatures-match-restrict signatures-match (x, y) → signatures-match (restrict (x, z), restrict (y, z))

Event: Disable signatures-match-restrict.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                         DISJOINT                            ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: one-way-disjoint (lst1 , lst2 ) = if lst1 ≃ nil then t

else (car (lst1 ) ∉ lst2 ) ∧ one-way-disjoint (cdr (lst1 ), lst2 ) endif

Definition: disjoint (lst1 , lst2 ) = (one-way-disjoint (lst1 , lst2 ) ∧ one-way-disjoint (lst2 , lst1 ))

Theorem: disjoint-nil disjoint (x, nil) ∧ disjoint (nil, x)

Theorem: cons-preserves-one-way-disjoint2 one-way-disjoint (lst2 , cons (x, lst)) → one-way-disjoint (lst2 , lst)

Theorem: cdr-preserves-disjoint disjoint (cons (x, lst), lst2 ) → disjoint (lst, lst2 )

Theorem: no-duplicates-append-implies-one-way-disjoint no-duplicates (append (x, y)) → one-way-disjoint (x, y)

Event: Disable no-duplicates-append-implies-one-way-disjoint.

Theorem: right-cdr-preserves-one-way-disjoint (one-way-disjoint (x, y) ∧ listp (y)) → one-way-disjoint (x, cdr (y))

Event: Disable right-cdr-preserves-one-way-disjoint.

Theorem: disjoint-preserves-no-duplicates (no-duplicates (lst1 ) ∧ no-duplicates (lst2 ) ∧ disjoint (lst1 , lst2 )) → no-duplicates (append (lst1 , lst2 ))

Event: Disable disjoint-preserves-no-duplicates.

Theorem: one-way-disjoint-right-cons (one-way-disjoint (lst1 , lst2 ) ∧ (x ∉ lst1 )) → one-way-disjoint (lst1 , cons (x, lst2 ))

Event: Disable one-way-disjoint-right-cons.

Theorem: disjoint-right-cons (disjoint (lst1 , lst2 ) ∧ (x ∉ lst1 )) → disjoint (lst1 , cons (x, lst2 ))

Event: Disable disjoint-right-cons.

Theorem: one-way-disjoint-right-cdr (listp (lst2 ) ∧ one-way-disjoint (lst1 , lst2 )) → one-way-disjoint (lst1 , cdr (lst2 ))

Event: Disable one-way-disjoint-right-cdr.

Theorem: disjoint-right-cdr (listp (lst2 ) ∧ disjoint (lst1 , lst2 )) → disjoint (lst1 , cdr (lst2 ))

Event: Disable disjoint-right-cdr.

Theorem: disjoint-right-append (disjoint (lst1 , lst2 ) ∧ disjoint (lst1 , lst3 )) → disjoint (lst1 , append (lst2 , lst3 ))

Event: Disable disjoint-right-append.

Event: Disable disjoint.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;                                                             ;;
;;                       COND-SUBSETP                          ;;
;;                                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Definition: cond-subsetp (lst1 , lst2 ) = if lst1 ≃ nil then t

else (car (lst1 ) ∈ cons ('leave, cons ('routineerror, lst2 ))) ∧ cond-subsetp (cdr (lst1 ), lst2 ) endif

Theorem: cond-subsetp-append (cond-subsetp (y, z) ∧ cond-subsetp (x, y)) → cond-subsetp (append (x, y), z)

Event: Disable cond-subsetp-append.

Theorem: subsetp-implies-cond-subsetp subset (x, y) → cond-subsetp (x, y)

Event: Disable subsetp-implies-cond-subsetp.

Event: Make the library "c1".

Index

add1-difference, 8 add1-difference2, 10 add1-preserves-lessp, 8 add1-sub1-difference, 8 all-cars-unique, 5, 6, 15, 18, 20 all-cars-unique-commutes-append, 6 append, 2 append-cons-rewrite, 2 append-cons-rewrite2, 3 append-doesnt-affect-value4, 12 append-nil-lemma, 2 append-plistp-nil-lemma, 5 append-rewrite2, 2 assoc, 1 assoc-not-affected-by-extra-ele

ment, 2 assoc-restriction, 17 assoc-unique-member, 6 assoc-value1, 1 associativity-of-append, 2 associativity-of-plus, 9

cars-unique-cars-unique, 5 cars-unique-cons, 6 cars-unique-names-unique, 6 cddr-length-plistp-2, 12 cdr-preserves-disjoint, 20 cond-subsetp, 22 cond-subsetp-append, 22 cons-car-append-all-cars-unique, 6 cons-distributes-over-listcars, 4 cons-preserves-one-way-disjoint

2, 20 cons-preserves-subset, 3 cons-preserves-subset2, 3

definedp, 14, 15 definedp-append-preserves-assoc, 15 definedp-car-assoc, 14 definedp-car-cons, 14 definedp-distributes, 15 definedp-implies-member, 14 definedp-member-assoc, 14 definedp-once, 15 definedp-rewrites-to-member, 14 difference-add1, 9 difference-difference-plus, 9 difference-lessp, 9 difference-lessp2, 10 difference-n-leq, 9 difference-plus-rewrite, 9 difference-rewrite, 8 difference-x-x, 8 disjoint, 20, 21 disjoint-nil, 20 disjoint-preserves-no-duplicate

s, 21 disjoint-right-append, 21 disjoint-right-cdr, 21 disjoint-right-cons, 21 double-cdr-induction, 17

exp, 6

get, 12–14 get-0, 13 get-0-plus, 13 get-add1, 13 get-add1-add1-append, 13 get-add1-length-plus, 13 get-add1-plus, 13 get-append, 13 get-car, 13 get-inverts-put, 14 get-length-car, 13 get-length-car1, 13 get-length-cons, 13 get-length-plus, 13 get-sub1, 13

idifference, 7

ileq, 7 ilessp, 7 index, 11 index-length, 11 inegate, 7 integerp, 7, 10 iplus, 7, 10 iplus-integerp, 7

length, 2–4, 11–13, 15, 16 length-cons, 2 length-distributes, 2 length-plistp, 2, 12 lessp-member-index-length, 11 lessp-transitive, 9 listcars, 4–6, 12, 14, 16–19 listcars-distributes, 4 listcars-plistp, 4 listcars-preserves-length, 4 listcars-restriction-append, 17 listp-implies-non-zero-length, 3

max, 1 member-car-listcars, 6 member-cons, 5 member-defined-name, 14 member-distributes, 3 member-implies-nonzero-index, 11 member-index-lessp-length, 11 member-listcars-assoc, 4 multiple-puts-cancel, 15

name, 1 name-expansion, 1 no-duplicates, 4–6, 16–18, 20, 21 no-duplicates-append, 4 no-duplicates-append-append, 4 no-duplicates-append-implies-one

-way-disjoint, 20 no-duplicates-append-restrict, 17 no-duplicates-commutes-append, 5 no-duplicates-cons-append, 5 no-duplicates-cons-append2, 5 no-duplicates-duplication, 5 no-duplicates-member-append2, 5 no-duplicates-member-cons, 6 no-duplicates-member2, 4 no-duplicates-restriction, 16 not-definedp-assoc-append, 15 not-member-listcars-not-assoc, 4 not-zerop-length-listp, 2 nth, 10, 11 nth-index-elimination, 11

one-way-disjoint, 20, 21 one-way-disjoint-right-cdr, 21 one-way-disjoint-right-cons, 21

plistp, 2–6, 12, 14, 16–19 plistp-append, 12 plistp-atom, 12 plistp-cons, 12 plus-0-rewrite, 8 plus-0-rewrite2, 9 plus-add1, 8 plus-add1-commute, 8 plus-add1-sub1, 9 plus-commutes, 7 plus-equality-lemma1, 8 plus-preserves-lessp, 9 plus-preserves-lessp2, 9 plus-preserves-lessp3, 9 plus-times-3, 10 put, 13–16 put-assoc, 14 put-assoc-expansion, 14 put-car-listp, 14 put-car-nlistp, 14 put-length, 16 put-never-shrinks, 15 put-preserves-length, 15 put-preserves-plistp, 14 put-value-length-rewrite, 15 puts-commute, 15

reorder-subset, 11 restrict, 16–18, 20 restrict-alist-listcars, 16 restrict-append, 18 restrict-append2, 18 restrict-listcars-member, 17 restrict-matching-listcars, 17 restrict-restricts-listcars, 18 restriction-cdr, 18 restriction-induction-hint, 17 restriction-names-cdr, 16 restriction-nil-names, 16 restriction-plistp, 17 reverse, 3, 12 reverse-append-reverse, 12 reverse-append-reverse1, 12 reverse-plistp, 3 reverse-preserves-length, 3 reverse-reverse, 3 right-cdr-preserves-one-way-dis

joint, 21

signature, 19, 20 signature-restrict-commute, 20 signatures-match, 18–20 signatures-match-append1, 19 signatures-match-listcars, 19 signatures-match-listcars-equal, 19 signatures-match-listp, 19 signatures-match-preserves-uniq

ueness-of-cars, 20 signatures-match-reflexive, 18 signatures-match-reflexive1, 18 signatures-match-reorder, 19 signatures-match-restrict, 20 signatures-match-symmetric, 18 signatures-match-transitive, 19 sub1-plus4, 10 sub1-plus5, 10 sub1-preserves-lessp, 8 subset, 3, 5, 11, 22 subset-append1, 11 subset-distributes, 3 subset-preserves-no-duplicates, 5 subset-reflexive, 3 subsetp-implies-cond-subsetp, 22 superset-preserves-membership, 3 times-m-rewrite, 8

value, 1

value-expansion2, 1 value-expansion3, 1

zero-iplus-identity, 7

zero-iplus-right-identity, 10 zero-length-plistp-nil, 12 zerop-difference-lessp, 10