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

Theorem: member-cons (a ∈ l) → (a ∈ cons (x, l))

Theorem: subsetp-cons subsetp (l, m) → subsetp (l, cons (a, m))

Theorem: subsetp-reflexivity subsetp (x, x)

Theorem: cdr-subsetp subsetp (cdr (x), x)

Theorem: member-subsetp ((x ∈ y) ∧ subsetp (y, z)) → (x ∈ z)

Theorem: subsetp-is-transitive (subsetp (x, y) ∧ subsetp (y, z)) → subsetp (x, z)

Theorem: append-is-subsetp subsetp (x, y) → subsetp (append (x, y), y)

Theorem: member-append-2 (x ∈ z) → (x ∈ append (y, z))

Theorem: member-append-1 (x ∈ y) → (x ∈ append (y, z))

Theorem: non-member-eliminates-append-1 (x ∉ y) → ((x ∈ append (y, z)) = (x ∈ z))

Theorem: non-member-eliminates-append-2 (x ∉ z) → ((x ∈ append (y, z)) = (x ∈ y))

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

Theorem: subsetp-of-append-1 subsetp (x, append (x, y))

Theorem: subsetp-of-append-2 subsetp (y, append (x, y))

Theorem: append-preserves-subsetp-second-1 subsetp (x, y) → subsetp (x, append (y, z))

Theorem: append-preserves-subsetp-second-2 subsetp (x, z) → subsetp (x, append (y, z))

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

Theorem: subsetp-append-append (subsetp (a, b) ∧ subsetp (c, d)) → subsetp (append (a, c), append (b, d))

Theorem: union-append-subsetp subsetp (x ∪ y, append (x, y))

Theorem: append-union-subsetp subsetp (append (x, y), x ∪ y)

Theorem: union-is-subsetp subsetp (x, y) → subsetp (x ∪ y, y)

Theorem: member-union-2 (x ∈ z) → (x ∈ (y ∪ z))

Theorem: member-union-1 (x ∈ y) → (x ∈ (y ∪ z))

Theorem: non-member-eliminates-union-1 (x ∉ y) → ((x ∈ (y ∪ z)) = (x ∈ z))

Theorem: non-member-eliminates-union-2 (x ∉ z) → ((x ∈ (y ∪ z)) = (x ∈ y))

Theorem: member-union-3 (x ∈ (y ∪ z)) = ((x ∈ y) ∨ (x ∈ z))

Theorem: subsetp-of-union-1 subsetp (x, x ∪ y)

Theorem: subsetp-of-union-2 subsetp (y, x ∪ y)

Theorem: union-preserves-subsetp-second-1 subsetp (x, y) → subsetp (x, y ∪ z)

Theorem: union-preserves-subsetp-second-2 subsetp (x, z) → subsetp (x, y ∪ z)

Theorem: union-preserves-subsetp-first (subsetp (x, z) ∧ subsetp (y, z)) → subsetp (x ∪ y, z)

Theorem: subsetp-union-union (subsetp (a, b) ∧ subsetp (c, d)) → subsetp (a ∪ c, b ∪ d)

Theorem: union-subsetp subsetp (x, y) → ((x ∪ y) = y)

Definition: make-set (l) = if ¬ listp (l) then nil

elseif car (l) ∈ cdr (l) then make-set (cdr (l)) else cons (car (l), make-set (cdr (l))) endif

Theorem: make-set-preserves-member (x ∈ make-set (l)) = (x ∈ l)

Theorem: make-set-preserves-subsetp-1 subsetp (make-set (x), make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-2 subsetp (x, make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-3 subsetp (make-set (x), y) = subsetp (x, y)

Definition: setp (x) = if ¬ listp (x) then t

else (car (x) ∉ cdr (x)) ∧ setp (cdr (x)) endif

Theorem: make-set-gives-setp setp (make-set (x))

Theorem: union-of-sets-is-setp (setp (x) ∧ setp (y)) → setp (x ∪ y)

Event: Make the library "subset".

Index

append-is-subsetp, 1 append-preserves-subsetp-first, 2 append-preserves-subsetp-second

-1, 2 -2, 2

append-union-subsetp, 2

cdr-subsetp, 1

make-set, 3 make-set-gives-setp, 3 make-set-preserves-member, 3 make-set-preserves-subsetp-1, 3 make-set-preserves-subsetp-2, 3 make-set-preserves-subsetp-3, 3 member-append-1, 1 member-append-2, 1 member-append-3, 1 member-cons, 1 member-subsetp, 1 member-union-1, 2 member-union-2, 2 member-union-3, 2

non-member-eliminates-append-1, 1 non-member-eliminates-append-2, 1 non-member-eliminates-union-1, 2 non-member-eliminates-union-2, 2

setp, 3 subsetp, 1–3 subsetp-append-append, 2 subsetp-cons, 1 subsetp-is-transitive, 1 subsetp-of-append-1, 1 subsetp-of-append-2, 2 subsetp-of-union-1, 2 subsetp-of-union-2, 2 subsetp-reflexivity, 1 subsetp-union-union, 3

union-append-subsetp, 2 union-is-subsetp, 2 union-of-sets-is-setp, 3 union-preserves-subsetp-first, 3 union-preserves-subsetp-second-

1, 2 2, 3 union-subsetp, 3