Event: Start with the library "subset".

Definition: set-equal (x, y) = (subsetp (x, y) ∧ subsetp (y, x))

Theorem: set-equal-char set-equal (x, y) → ((a ∈ x) = (a ∈ y))

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

then if car (x) ∈ y then diff (cdr (x), y)

else cons (car (x), diff (cdr (x), y)) endif else x endif

Definition: sym-diff (x, y) = (diff (x, y) ∪ diff (y, x))

Theorem: diff-with-nil (¬ listp (x)) → (diff (y, x) = y)

Definition: not-subsetp-skolem (x, y) = if ¬ listp (x) then nil

elseif car (x) ∈ y then not-subsetp-skolem (cdr (x), y)

else car (x) endif

Theorem: subsetp-witness ((not-subsetp-skolem (x, y) ∉ x) ∨ (not-subsetp-skolem (x, y) ∈ y)) → subsetp (x, y)

Theorem: diff-non-member (a ∈ diff (x, y)) → (a ∉ y)

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

Theorem: sym-diff-char-1 (a ∈ sym-diff (x, y)) → if a ∈ x then a ∉ y

else a ∈ y endif

Theorem: sym-diff-char-2 if a ∈ x then a ∉ y else a ∈ y endif → (a ∈ sym-diff (x, y))

Event: Disable sym-diff.

Theorem: sym-diff-char (a ∈ sym-diff (x, y)) = if a ∈ x then a ∉ y

else a ∈ y endif

Theorem: sym-diff-assoc set-equal (sym-diff (sym-diff (x, y), z), sym-diff (x, sym-diff (y, z)))

;(PROVE-LEMMA SYM-DIFF-ASSOC (REWRITE)
;      (SET-EQUAL (SYM-DIFF (SYM-DIFF X Y) Z)
; (SYM-DIFF X (SYM-DIFF Y Z))))

Event: Enable sym-diff.

Theorem: sym-diff-comm set-equal (sym-diff (x, y), sym-diff (y, x))

Index

diff, 1 diff-non-member, 1 diff-with-nil, 1

member-union, 1

not-subsetp-skolem, 1

set-equal, 1, 2 set-equal-char, 1 subsetp, 1 subsetp-witness, 1 sym-diff, 1, 2 sym-diff-assoc, 2 sym-diff-char, 2 sym-diff-char-1, 1 sym-diff-char-2, 1 sym-diff-comm, 2