Event: Start with the library "subset".

Definition: newpairs (pair, pairs) = if ¬ listp (pairs) then nil

elseif cdr (pair) = caar (pairs)

then cons (cons (car (pair), cdar (pairs)), newpairs (pair, cdr (pairs))) else newpairs (pair, cdr (pairs)) endif

Definition: all-newpairs (pairs1 , pairs2 ) = if ¬ listp (pairs1 ) then nil

else append (newpairs (car (pairs1 ), pairs2 ), all-newpairs (cdr (pairs1 ), pairs2 )) endif

Definition: all-cars (pairs) = if listp (pairs) then cons (caar (pairs), all-cars (cdr (pairs)))

else nil endif

Definition: all-cdrs (pairs) = if listp (pairs) then cons (cdar (pairs), all-cdrs (cdr (pairs)))

else nil endif

Definition: prod1 (a, l) = if listp (l) then cons (cons (a, car (l)), prod1 (a, cdr (l)))

else nil endif

Definition: prod (l, m) = if listp (l) then append (prod1 (car (l), m), prod (cdr (l), m))

else nil endif

Definition: field (pairs) = prod (all-cars (pairs), all-cdrs (pairs))

Definition: all-pairsp (pairs) = if ¬ listp (pairs) then t

else listp (car (pairs)) ∧ all-pairsp (cdr (pairs)) endif

Theorem: newpairs-prod1-subsetp subsetp (newpairs (pair, pairs), prod1 (car (pair), all-cdrs (pairs)))

Theorem: all-newpairs-field-subsetp-1 subsetp (all-newpairs (pairs1 , pairs2 ), prod (all-cars (pairs1 ), all-cdrs (pairs2 )))

Theorem: all-newpairs-field-subsetp subsetp (all-newpairs (pairs, pairs), field (pairs))

Definition: close1 (pairs) = (make-set (all-newpairs (pairs, pairs)) ∪ pairs)

; My goal is to show that
; (SUBSETP PAIRS (FIELD PAIRS))
; and
; (IMPLIES (SUBSETP X (FIELD PAIRS))
;          (SUBSETP (CLOSE1 X) (FIELD PAIRS))) .
; For then we can prove the following lemma, which will
; show that the following definition should
; be accepted, where CARD is cardinality:
;(IMPLIES (AND (ALL-PAIRSP PAIRS)
;       (NOT (EQUAL PAIRS (CLOSE1 PAIRS))))
;  (EQUAL (LESSP (DIFFERENCE (CARD (FIELD (CLOSE1 PAIRS)))
;    (CARD (CLOSE1 PAIRS)))
;        (DIFFERENCE (CARD (FIELD PAIRS))
;    (CARD PAIRS)))
; T))

Theorem: cdr-all-cars-subsetp subsetp (all-cars (cdr (pairs)), all-cars (pairs))

Theorem: cdr-all-cdrs-subsetp subsetp (all-cdrs (cdr (pairs)), all-cdrs (pairs))

Theorem: prod-subsetp-1 subsetp (x, y) → subsetp (prod (x, z), prod (y, z))

Theorem: prod1-subsetp-2 subsetp (y, z) → subsetp (prod1 (a, y), prod1 (a, z))

Theorem: prod-subsetp-2 subsetp (y, z) → subsetp (prod (x, y), prod (x, z))

Theorem: field-subsetp all-pairsp (pairs) → subsetp (pairs, field (pairs))

Theorem: member-all-cars (a ∈ y) → (car (a) ∈ all-cars (y))

Theorem: subsetp-all-cars subsetp (x, y) → subsetp (all-cars (x), all-cars (y))

Theorem: member-all-cdrs (a ∈ y) → (cdr (a) ∈ all-cdrs (y))

Theorem: subsetp-all-cdrs subsetp (x, y) → subsetp (all-cdrs (x), all-cdrs (y))

Theorem: field-preserves-subsetp subsetp (x, y) → subsetp (field (x), field (y))

Theorem: subsetp-all-cars-prod subsetp (all-cars (prod (x, y)), x)

Theorem: subsetp-all-cdrs-prod subsetp (all-cdrs (prod (x, y)), y)

Theorem: prod-subsetp (subsetp (x1 , x2 ) ∧ subsetp (y1 , y2 )) → subsetp (prod (x1 , y1 ), prod (x2 , y2 ))

Theorem: subsetp-field-twice subsetp (field (field (l)), field (l))

Theorem: subsetp-close1-field subsetp (x, field (pairs)) → subsetp (close1 (x), field (pairs))

Definition: card (x) = if listp (x)

then if car (x) ∈ cdr (x) then card (cdr (x)) else 1 + card (cdr (x)) endif

else 0 endif

Theorem: card-not-0 (x ∈ y) → (card (y) ≠ 0)

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

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

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

Theorem: remove-non-member (a ∉ l) → (remove (a, l) = l)

Theorem: remove-preserves-non-member (a ∉ l) → (a ∉ remove (x, l))

Theorem: remove-subsetp subsetp (remove (a, l), l)

Theorem: remove-preserves-member ((b ∈ l) ∧ (a ≠ b)) → (b ∈ remove (a, l))

; Interestingly, I couldn't get the following at first, but in the
; course of performing a manual proof I found the rewrite lemmas
; (added above) that I needed.  By the way, as things are now the
; induction hint below is necessary.

Theorem: remove-card (a ∈ l) → (card (remove (a, l)) = (card (l) − 1))

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

else 0 endif

Theorem: length-remove (length (remove (a, x)) ≠ length (x)) → (length (remove (a, x)) < length (x))

Theorem: card-subsetp-ind-help listp (x) → (length (remove (car (x), x)) < length (x))

Definition: card-subsetp-ind (x, y) = if listp (x) then card-subsetp-ind (remove (car (x), x), remove (car (x), y))

else t endif

Theorem: remove-preserves-subsetp subsetp (x, y) → subsetp (remove (a, x), remove (a, y))

; Interestingly, I came to proving the following lemma by
; trying to do a hand proof of the one after it and
; realizing that the former was conceptually simpler.
; I'm still surprised that the theorem-prover handled the
; former but not (directly) the latter.

Theorem: card-subsetp subsetp (x, y) → (card (x) ≤ card (y))

Theorem: card-subsetp-rewrite (subsetp (x, y) ∧ (card (x) ≠ card (y))) → ((card (x) < card (y)) = t)

; Recall that we proved
; SUBSETP-CLOSE1-FIELD :
; (IMPLIES (SUBSETP X (FIELD PAIRS))
;    (SUBSETP (CLOSE1 X) (FIELD PAIRS)))

Theorem: field-of-close1-is-subsetp all-pairsp (x) → subsetp (field (close1 (x)), field (x))

Theorem: field-of-close1-is-superset subsetp (field (x), field (close1 (x)))

Theorem: close1-preserves-card-of-field all-pairsp (x) → (card (field (close1 (x))) = card (field (x)))

Theorem: union-card-lessp ((x ∪ y) ≠ y) → (card (y) < card (x ∪ y))

Theorem: trans-accept-1 (all-pairsp (pairs) ∧ (pairs ≠ close1 (pairs))) → ((card (pairs) < card (close1 (pairs))) = t)

Theorem: card-field-lessp (all-pairsp (x) ∧ (card (x) ≠ card (field (x)))) → ((card (x) < card (field (x))) = t)

Theorem: union-preserves-all-pairsp (all-pairsp (x) ∧ all-pairsp (y)) → all-pairsp (x ∪ y)

Theorem: append-preserves-all-pairsp (all-pairsp (x) ∧ all-pairsp (y)) → all-pairsp (append (x, y))

Theorem: newpairs-preserves-all-pairsp (all-pairsp (pairs1 ) ∧ all-pairsp (pairs2 )) → all-pairsp (newpairs (pairs1 , pairs2 ))

Theorem: all-newpairs-preserves-all-pairsp (all-pairsp (pairs1 ) ∧ all-pairsp (pairs2 )) → all-pairsp (all-newpairs (pairs1 , pairs2 ))

Theorem: make-set-preserves-all-pairsp all-pairsp (pairs) → all-pairsp (make-set (pairs))

Theorem: close-1-preserves-all-pairsp all-pairsp (pairs) → all-pairsp (close1 (pairs))

Theorem: lessp-difference-for-trans-accept ((c < a) ∧ (c < b)) → (((a − b) < (a − c)) = t)

Theorem: card-field-not-lessp all-pairsp (x) → ((card (field (x)) < card (x)) = f)

Theorem: trans-accept (all-pairsp (pairs) ∧ (pairs ≠ close1 (pairs))) → (((card (field (close1 (pairs))) − card (close1 (pairs)))

< (card (field (pairs)) − card (pairs))) = t)

Event: Disable field.

Event: Disable close1.

; It's unfortunate that the following is needed.

Event: Disable close1-preserves-card-of-field.

Definition: trans (pairs) = if all-pairsp (pairs)

then if pairs = close1 (pairs) then pairs else trans (close1 (pairs)) endif

else pairs endif

Theorem: all-newpairs-closes ((cons (x, y) ∈ pairs1 ) ∧ (cons (y, z) ∈ pairs2 )) → (cons (x, z) ∈ all-newpairs (pairs1 , pairs2 ))

Theorem: close1-closes (all-pairsp (pairs) ∧ (cons (x, y) ∈ pairs) ∧ (cons (y, z) ∈ pairs)) → (cons (x, z) ∈ close1 (pairs))

Theorem: trans-closes (all-pairsp (pairs) ∧ (cons (x, y) ∈ pairs) ∧ (cons (y, z) ∈ pairs)) → (cons (x, z) ∈ trans (pairs))

; Finally, we prove that TRANS gives the least transitive set
; containing the original pairs.

Definition: transp (l) = (all-pairsp (l) ∧ subsetp (all-newpairs (l, l), l))

;; ok to here 1/04/87 09:49:47

Theorem: member-newpairs (all-pairsp (l) ∧ (b ∈ l) ∧ (cdr (a) = car (b))) → (cons (car (a), cdr (b)) ∈ newpairs (a, l))

Theorem: newpairs-preserves-subsetp (all-pairsp (l) ∧ all-pairsp (m) ∧ subsetp (l, m)) → subsetp (newpairs (a, l), newpairs (a, m))

Theorem: all-newpairs-preserves-subsetp-2 (all-pairsp (l) ∧ all-pairsp (m1 ) ∧ all-pairsp (m2 ) ∧ subsetp (m1 , m2 )) → subsetp (all-newpairs (l, m1 ), all-newpairs (l, m2 ))

Theorem: member-newpairs-all-newpairs (a ∈ l) → subsetp (newpairs (a, m), all-newpairs (l, m))

Theorem: all-newpairs-preserves-subsetp-1 (all-pairsp (l1 ) ∧ all-pairsp (l2 ) ∧ all-pairsp (m) ∧ subsetp (l1 , l2 )) → subsetp (all-newpairs (l1 , m), all-newpairs (l2 , m))

Theorem: all-newpairs-preserves-subsetp-both (all-pairsp (l1 ) ∧ all-pairsp (l2 ) ∧ all-pairsp (m1 ) ∧ all-pairsp (m2 ) ∧ subsetp (l1 , l2 ) ∧ subsetp (m1 , m2 )) → subsetp (all-newpairs (l1 , m1 ), all-newpairs (l2 , m2 ))

Theorem: close1-preserves-subsetp (all-pairsp (l) ∧ all-pairsp (m) ∧ subsetp (l, m)) → subsetp (close1 (l), close1 (m))

Theorem: trans-is-least-transp (all-pairsp (pairs) ∧ subsetp (pairs, l) ∧ transp (l)) → subsetp (trans (pairs), l)

; Now let's show that the transitive closure of a transitive set is itself.
; In particular, (TRANS (TRANS PAIRS)) = (TRANS PAIRS) for a list PAIRS of
; pairs.  Interestingly, though, the latter result is easily proved by
; a trivial induction on trans:

Theorem: trans-is-idempotent trans (trans (pairs)) = trans (pairs)

Theorem: close1-of-transp transp (pairs) → (close1 (pairs) = pairs)

Theorem: trans-of-transp transp (pairs) → (trans (pairs) = pairs)

Theorem: trans-closes-again (all-pairsp (pairs) ∧ (cons (x, y) ∈ trans (pairs)) ∧ (cons (y, z) ∈ trans (pairs))) → (cons (x, z) ∈ trans (pairs))

Index

all-cars, 1–3 all-cdrs, 1–3 all-newpairs, 1, 2, 5–7 all-newpairs-closes, 6 all-newpairs-field-subsetp, 2 all-newpairs-field-subsetp-1, 2 all-newpairs-preserves-all-pair

sp, 5 all-newpairs-preserves-subsetp-

1, 7 2, 7 both, 7

all-pairsp, 1, 2, 5–8 append-preserves-all-pairsp, 5

card, 3–6 card-field-lessp, 5 card-field-not-lessp, 6 card-not-0, 3 card-subsetp, 4 card-subsetp-ind, 4 card-subsetp-ind-help, 4 card-subsetp-rewrite, 5 cdr-all-cars-subsetp, 2 cdr-all-cdrs-subsetp, 2 close-1-preserves-all-pairsp, 6 close1, 2, 3, 5–8 close1-closes, 6 close1-of-transp, 8 close1-preserves-card-of-field, 5 close1-preserves-subsetp, 7

field, 1–3, 5, 6 field-of-close1-is-subsetp, 5 field-of-close1-is-superset, 5 field-preserves-subsetp, 3 field-subsetp, 2

length, 4 length-remove, 4 lessp-difference-for-trans-accept, 6 make-set, 2, 5 make-set-preserves-all-pairsp, 5 member-all-cars, 2 member-all-cdrs, 3 member-newpairs, 7 member-newpairs-all-newpairs, 7

newpairs, 1, 5, 7 newpairs-preserves-all-pairsp, 5 newpairs-preserves-subsetp, 7 newpairs-prod1-subsetp, 1

prod, 1–3 prod-subsetp, 3 prod-subsetp-1, 2 prod-subsetp-2, 2 prod1, 1, 2 prod1-subsetp-2, 2

remove, 3, 4 remove-card, 4 remove-non-member, 3 remove-preserves-member, 4 remove-preserves-non-member, 4 remove-preserves-subsetp, 4 remove-subsetp, 4

subsetp, 1–5, 7 subsetp-all-cars, 3 subsetp-all-cars-prod, 3 subsetp-all-cdrs, 3 subsetp-all-cdrs-prod, 3 subsetp-close1-field, 3 subsetp-field-twice, 3

trans, 6–8 trans-accept, 6 trans-accept-1, 5 trans-closes, 6 trans-closes-again, 8 trans-is-idempotent, 8 trans-is-least-transp, 7 trans-of-transp, 8 transp, 7, 8

union-card-lessp, 5 union-preserves-all-pairsp, 5