Section 27Want more of a challenge? View in iconic form (experimental)

# MATH introduce sets and set membership
[hear] (intro element);

[hear] (define element /
? x /
? lst /
not /
= (list-find-helper (lst) (x) (? y 0) 1) 0);

[hear] (element 2 (vector 8 9 2));

[hear] (element 8 (vector 8 9 2));

[hear] (element 9 (vector 8 9 2));

[hear] (element 4 (vector 6 1 4 9));

[hear] (element 1 (vector 6 1 4 9));

[hear] (element 6 (vector 6 1 4 9));

[hear] (element 1 (vector 8 1 0 3 5));

[hear] (element 3 (vector 8 1 0 3 5));

[hear] (element 0 (vector 8 1 0 3 5));

[hear] (element 3 (vector 4 0 3 7 9));

[hear] (element 0 (vector 4 0 3 7 9));

[hear] (element 9 (vector 4 0 3 7 9));

[hear] (element 3 (vector 4 1 3 9));

[hear] (element 9 (vector 4 1 3 9));

[hear] (element 4 (vector 4 1 3 9));

[hear] (not / element 8 (vector 4 1 0 9));

[hear] (not / element 8 (vector 6 4 0 7 5));

[hear] (not / element 1 (vector 0 7));

[hear] (not / element 4 (vector 1 3 2 5));

[hear] (not / element 8 (vector 3 7 2 5));

# rules for set equality
[hear] (define set-subset /
? x /
? y /
if (> (list-length / x) 0)
(and (element (head / x) (y))
(set-subset (tail / x) (y)))
(true));

[hear] (define set= /
? x /
? y /
and (set-subset (x) (y)) (set-subset (y) (x)));

[hear] (set= (vector 1 5 9) (vector 5 1 9));

[hear] (set= (vector 1 5 9) (vector 9 1 5));

[hear] (not / set= (vector 1 5 9) (vector 1 5));

# let's go leave ourselves wide open to Russell's paradox
# ... by using characteristic functions
# ... since it doesn't really matter for communication purposes
# ... and so far this is just used / tested with sets of integers really
[hear] (element 5 (all (? x / = (+ (x) 10) 15)));

[hear] (element 3 (all (? x / = (* (x) 3) (+ (x) 6))));

[hear] (define empty-set / vector);

[hear] (element 0 (natural-set));

[hear] (forall
(? x /
=> (element (x) (natural-set))
(element (+ (x) 1) (natural-set))));

[hear] (element 1 (natural-set));

[hear] (element 2 (natural-set));

[hear] (element 3 (natural-set));

[hear] (element 4 (natural-set));

[hear] (element 5 (natural-set));

[hear] (element 6 (natural-set));

[hear] (element 7 (natural-set));

[hear] (element 8 (natural-set));

[hear] (element 9 (natural-set));

[hear] (define boolean-set / vector (true) (false));

[hear] (element (true) (boolean-set));

[hear] (element (false) (boolean-set));

# actually, to simplify semantics elsewhere, true and false
# are now just 0 and 1 so they are not distinct from ints
[hear] (define even-natural-set /
all /
? x /
exists /
? y /
and (element (y) (natural-set))
(= (* 2 (y)) (x)));

[hear] (element 0 (natural-set));

[hear] (element 0 (even-natural-set));

[hear] (element 1 (natural-set));

[hear] (not / element 1 (even-natural-set));

[hear] (element 2 (natural-set));

[hear] (element 2 (even-natural-set));

[hear] (element 3 (natural-set));

[hear] (not / element 3 (even-natural-set));

[hear] (element 4 (natural-set));

[hear] (element 4 (even-natural-set));

[hear] (element 5 (natural-set));

[hear] (not / element 5 (even-natural-set));

[hear] (element 6 (natural-set));

[hear] (element 6 (even-natural-set));