# MATH introduce sets and set membership
[hear] (intro element);
[hear] (define element /
? x /
? lst /
not /
= (list-find (lst) (x) (? y / false)) (false));
[hear] (element 8 (vector 8 6 4 1 9));
[hear] (element 9 (vector 8 6 4 1 9));
[hear] (element 1 (vector 8 6 4 1 9));
[hear] (element 6 (vector 8 6 4 1 0 7));
[hear] (element 8 (vector 8 6 4 1 0 7));
[hear] (element 4 (vector 8 6 4 1 0 7));
[hear] (element 7 (vector 8 1 0 7 9));
[hear] (element 7 (vector 8 1 0 7 9));
[hear] (element 0 (vector 8 1 0 7 9));
[hear] (element 8 (vector 8 0 7 9 5));
[hear] (element 8 (vector 8 0 7 9 5));
[hear] (element 9 (vector 8 0 7 9 5));
[hear] (element 8 (vector 8 6 1 3 9));
[hear] (element 3 (vector 8 6 1 3 9));
[hear] (element 1 (vector 8 6 1 3 9));
[hear] (not / element 6 (vector 7 2 5));
[hear] (not / element 6 (vector 4 7 2 5));
[hear] (not / element 6 (vector 3 0 5));
[hear] (not / element 8 (vector 4 0 3 7));
[hear] (not / element 1 (vector 0 3 9));
# 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] (not / element (true) (natural-set));
[hear] (not / element (false) (natural-set));
[hear] (define boolean-set / vector (true) (false));
[hear] (element (true) (boolean-set));
[hear] (element (false) (boolean-set));
[hear] (not / element 0 (boolean-set));
[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));