; Pigeon hole principle, as suggested by Randy Pollack.

Event: Start with the initial nqthm theory.

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

elseif car (x) ∈ y then subsetp (cdr (x), y)

else f endif

Definition: dups (l) = if ¬ listp (l) then f

elseif car (l) ∈ cdr (l) then t

else dups (cdr (l)) endif

Definition: remove (x, z) = if ¬ listp (z) then z

elseif x = car (z) then remove (x, cdr (z)) else cons (car (z), remove (x, cdr (z))) endif

Theorem: remove-preserves-subsetp (listp (a) ∧ subsetp (a, b)) → subsetp (remove (x, a), remove (x, b))

Definition: double-list-ind (l, m) = if listp (l) ∧ listp (m)

then double-list-ind (remove (car (m), l), cdr (m))

else t endif

Theorem: remove-car-non-dups (listp (m) ∧ (¬ dups (m))) → (remove (car (m), m) = cdr (m))

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

else 0 endif

Theorem: length-remove-leq (length (l) < length (remove (x, l))) = f

Theorem: length-remove-lessp (x ∈ l) → ((length (remove (x, l)) < length (l)) = t)

Theorem: subsetp-dups ((length (l) < length (m)) ∧ subsetp (m, l)) → dups (m)

Index

double-list-ind, 1 dups, 1

length, 1 length-remove-leq, 1 length-remove-lessp, 1

remove, 1 remove-car-non-dups, 1 remove-preserves-subsetp, 1

subsetp, 1 subsetp-dups, 1