Event: Start with the initial nqthm theory.

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

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

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

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

then if car (y) ∈ x then bagdiff (delete (car (y), x), cdr (y))

else bagdiff (x, cdr (y)) endif else x endif

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

then if car (x) ∈ y then cons (car (x), bagint (cdr (x), delete (car (x), y))) else bagint (cdr (x), y) endif

else nil endif

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

then if x = car (l) then 1 + occurrences (x, cdr (l))

else occurrences (x, cdr (l)) endif else 0 endif

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

then if car (x) ∈ y then subbagp (cdr (x), delete (car (x), y))

else f endif else t endif

Theorem: listp-delete listp (delete (x, l)) = if listp (l) then (x ≠ car (l)) ∨ listp (cdr (l))

else f endif

Event: Disable listp-delete.

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

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

Theorem: equal-occurrences-zero (occurrences (x, l) = 0) = (x ∉ l)

Theorem: member-non-list (¬ listp (l)) → (x ∉ l)

Theorem: member-delete (x ∈ delete (y, l)) = if x ∈ l

then if x = y then 1 < occurrences (x, l)

else t endif else f endif

Theorem: member-delete-implies-membership (x ∈ delete (y, l)) → (x ∈ l)

Theorem: occurrences-delete occurrences (x, delete (y, l)) = if x = y

then if x ∈ l then occurrences (x, l) − 1

else 0 endif else occurrences (x, l) endif

Theorem: member-bagdiff (x ∈ bagdiff (a, b)) = (occurrences (x, b) < occurrences (x, a))

Theorem: bagdiff-delete bagdiff (delete (e, x), y) = delete (e, bagdiff (x, y))

Theorem: subbagp-delete subbagp (x, delete (u, y)) → subbagp (x, y)

Theorem: subbagp-cdr1 subbagp (x, y) → subbagp (cdr (x), y)

Theorem: subbagp-cdr2 subbagp (x, cdr (y)) → subbagp (x, y)

Theorem: subbagp-bagint1 subbagp (bagint (x, y), x)

Theorem: subbagp-bagint2 subbagp (bagint (x, y), y)

Theorem: occurrences-bagint occurrences (x, bagint (a, b)) = if occurrences (x, a) < occurrences (x, b) then occurrences (x, a)

else occurrences (x, b) endif

Theorem: occurrences-bagdiff occurrences (x, bagdiff (a, b)) = (occurrences (x, a) − occurrences (x, b))

Theorem: member-bagint (x ∈ bagint (a, b)) = ((x ∈ a) ∧ (x ∈ b))

Event: Let us define the theory bags to consist of the following events: occurrencesbagint, bagdiff-delete, occurrences-bagdiff, member-bagint, member-bagdiff, subbagpbagint2, subbagp-bagint1, subbagp-cdr2, subbagp-cdr1, subbagp-delete.

Event: Make the library "bags".

Index

bagdiff, 1–3 bagdiff-delete, 2 bagint, 1–3 bags, 3

delete, 1, 2 delete-delete, 2 delete-non-member, 2

equal-occurrences-zero, 2

listp-delete, 1

member-bagdiff, 2 member-bagint, 3 member-delete, 2 member-delete-implies-membership,

2 member-non-list, 2

occurrences, 1–3 occurrences-bagdiff, 3 occurrences-bagint, 3 occurrences-delete, 2

subbagp, 1–3 subbagp-bagint1, 2 subbagp-bagint2, 3 subbagp-cdr1, 2 subbagp-cdr2, 2 subbagp-delete, 2