# Author: Paul Fitzpatrick, paulfitz@ai.mit.edu
# Copyright (c) 2003 Paul Fitzpatrick
#
# This file is part of CosmicOS.
#
# CosmicOS is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# CosmicOS is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with CosmicOS; if not, write to the Free Software
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
#

# MATH introduce counting
(0)(.0)(..0)(...0)(....0)(.....0);
(.....0)(....0)(...0)(..0)(.0)(0);
# MATH now show equality
(= 0 0);
(= ..0 ..0);
(= .....0 .....0);
(= ..0 ..0);
(= ...0 ...0);
(= 0 0);
# MATH now show other comparisons
(> ..0 0);
(> .....0 .0);
(> ...0 .0);
(> .0 0);
(> ......0 0);
(> ....0 0);
(> .....0 0);
(> ....0 0);
(> .0 0);
(> ......0 .0);
(> ......0 ..0);
(< .0 ...0);
(< 0 .....0);
(< 0 ......0);
(< 0 .0);
(< 0 .0);
(< 0 ..0);
(< .0 ...0);
(< 0 ..0);
(< ..0 ....0);
(< ...0 .....0);
(< 0 ..0);
(> ....0 0);
(> .....0 ....0);
(< ..0 ...0);
(> ..0 .0);
(> .....0 .0);
(= ...0 ...0);
(= ...0 ...0);
(> .0 0);
(< .0 ....0);
(= ....0 ....0);
(> ...0 ..0);
# MATH introduce the NOT logical operator
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(= .....0 .....0);
(not (< .....0 .....0));
(not (> .....0 .....0));
(= .0 .0);
(not (< .0 .0));
(not (> .0 .0));
(= ...0 ...0);
(not (< ...0 ...0));
(not (> ...0 ...0));
(not (= 0 ..0));
(< 0);
(not (> 0 ..0));
(not (= .0 ....0));
(< .0);
(not (> .0 ....0));
(not (= .0 ....0));
(< .0);
(not (> .0 ....0));
(not (= ..0 ....0));
(< ..0);
(not (> ..0 ....0));
(not (= .....0 .......0));
(< .....0);
(not (> .....0 .......0));
(not (= .....0 .......0));
(< .....0);
(not (> .....0 .......0));
(not (= ...0 .0));
(> ...0 .0);
(not (< ...0 .0));
(not (= ......0 .....0));
(> ......0 .....0);
(not (< ......0 .....0));
(not (= .....0 ....0));
(> .....0 ....0);
(not (< .....0 ....0));
(not (= .......0 .....0));
(> .......0 .....0);
(not (< .......0 .....0));
(not (= .......0 .....0));
(> .......0 .....0);
(not (< .......0 .....0));
(not (= ...0 .0));
(> ...0 .0);
(not (< ...0 .0));
# MATH introduce the AND logical operator
(and (> .....0 ...0) (> .....0 ..0));
(and (< ....0 ......0) (= .0 .0));
(and (= 0 0) (> .......0 .....0));
(and (= .....0 .....0) (= ....0 ....0));
(and (< .....0 ......0) (= .....0 .....0));
(and (> .......0 .....0) (= ..0 ..0));
(and (< ...0 ......0) (> .....0 ....0));
(and (= ..0 ..0) (< 0 ..0));
(and (> .....0 ..0) (= ..0 ..0));
(and (< .0 ....0) (= ....0 ....0));
(not (and (< .0 ..0) (= ..0 .....0)));
(not (and (< .0 ...0) (= .0 ...0)));
(not (and (< ...0 ....0) (< .....0 ..0)));
(not (and (> .....0 ..0) (= ....0 ..0)));
(not (and (> ...0 ..0) (< ......0 0)));
(not (and (= .....0 ......0) (> ....0 ..0)));
(not (and (> .0 ...0) (< .....0 ......0)));
(not (and (< ..0 .0) (= ....0 ....0)));
(not (and (> ....0 .....0) (= ..0 ..0)));
(not (and (= .0 0) (> .......0 .....0)));
(not (and (> ...0 .....0) (> ...0 ......0)));
(not (and (< .....0 ....0) (> ......0 ......0)));
(not (and (= ....0 0) (> 0 ...0)));
(not (and (= .....0 0) (> ...0 ...0)));
(not (and (> 0 ....0) (> ..0 ..0)));
(not (and (> 0 ......0) (= ....0 .0)));
(not (and (> ...0 ...0) (= .....0 ......0)));
(and (> ........0 .....0) (< 0 ...0));
(and (> ....0 ..0) (< 0 ...0));
(not (and (< ...0 ..0) (< .....0 ..0)));
(not (and (> .0 .0) (= ..0 0)));
(not (and (> ..0 0) (> .....0 .....0)));
(and (= ..0 ..0) (= ..0 ..0));
(not (and (= ...0 .0) (> 0 ......0)));
(and (< .0 ..0) (= ...0 ...0));
# MATH introduce the OR logical operator
(or (< ..0 ...0) (< .....0 ......0));
(or (= .....0 .....0) (> ......0 ...0));
(or (< .0 ..0) (> ..0 0));
(or (> ....0 .0) (< ..0 ....0));
(or (< .0 ....0) (> .0 0));
(or (< ....0 .....0) (= 0 0));
(or (> .....0 ..0) (= .....0 .....0));
(or (> .....0 ..0) (> ......0 .....0));
(or (< .....0 ........0) (< .....0 ........0));
(or (= 0 0) (= ..0 ..0));
(or (< 0 ...0) (= 0 ..0));
(or (= ...0 ...0) (= ....0 ..0));
(or (> ...0 .0) (= 0 ..0));
(or (= .....0 .....0) (= .0 .....0));
(or (< ..0 ....0) (< ......0 .....0));
(or (> ...0 ....0) (> ...0 .0));
(or (> 0 ....0) (= 0 0));
(or (= ..0 0) (< 0 ..0));
(or (< ......0 ..0) (< .....0 .......0));
(or (= ..0 0) (= 0 0));
(not (or (> .....0 ......0) (> .0 .0)));
(not (or (> .0 ......0) (> ....0 ....0)));
(not (or (> ..0 ......0) (> ..0 .....0)));
(not (or (> ...0 ....0) (= .0 0)));
(not (or (> ...0 ...0) (< .....0 ...0)));
(or (< ..0 0) (= .0 .0));
(or (= 0 ..0) (> ....0 ..0));
(or (= .....0 ...0) (= 0 0));
(or (> 0 ...0) (> ....0 ...0));
(or (< ....0 0) (< .....0 ........0));
(or (= ...0 ...0) (= ..0 ..0));
(not (or (< .....0 ...0) (< ..0 .0)));
(or (> ....0 .0) (> .0 ......0));
(or (< ....0 ...0) (= ....0 ....0));
(not (or (> 0 0) (= ..0 ...0)));
# MATH use equality for truth values
(= (< 0 ...0) (< .....0 ........0));
(= (< .0 ....0) (< ...0 ......0));
(= (> ..0 .0) (< ..0 .....0));
(= (> .......0 ....0) (= .....0 .....0));
(= (= ...0 ...0) (> .....0 ....0));
(= (< ......0 .0) (= ...0 ..0));
(= (> 0 ...0) (> .0 .0));
(= (= ..0 0) (= ....0 ...0));
(= (= ....0 0) (< .....0 ...0));
(= (< .....0 ..0) (< ..0 .0));
(not (= (= 0 ...0) (> ..0 .0)));
(not (= (> .0 ..0) (= ...0 ...0)));
(not (= (> 0 0) (> ...0 ..0)));
(not (= (= ....0 .....0) (< 0 ...0)));
(not (= (= 0 .0) (> .....0 ....0)));
(not (= (> ....0 .0) (< ....0 .0)));
(not (= (> ......0 ...0) (= ....0 .0)));
(not (= (< ....0 ......0) (> ...0 ....0)));
(not (= (< 0 ..0) (= .....0 ....0)));
(not (= (> ......0 ....0) (< ..0 0)));
(= true (< ....0 .....0));
(= true (= ...0 ...0));
(= true (= 0 0));
(= true (< 0 .0));
(= true (> .....0 ..0));
(= (< ...0 ....0) true);
(= (> ........0 .....0) true);
(= (< .0 ....0) true);
(= (< ...0 ....0) true);
(= (= ...0 ...0) true);
(= false (< ...0 ..0));
(= false (= ....0 .....0));
(= false (< ......0 0));
(= false (< .....0 ..0));
(= false (= 0 ..0));
(= (> ......0 ......0) false);
(= (> ...0 ....0) false);
(= (< .....0 ..0) false);
(= (> .0 .0) false);
(= (< ......0 ....0) false);
(= true true);
(= false false);
(not (= true false));
(not (= false true));
# MATH introduce addition
(= (+ ....0 .0) .....0);
(= (+ ..0 ..0) ....0);
(= (+ 0 ...0) ...0);
(= (+ ....0 0) ....0);
(= (+ ...0 0) ...0);
(= (+ ...0 .0) ....0);
(= (+ 0 0) 0);
(= (+ 0 .0) .0);
(= (+ ...0 .0) ....0);
(= (+ 0 .0) .0);
# MATH introduce subtraction
(= (- ..0 ..0) 0);
(= (- ...0 0) ...0);
(= (- ...0 ...0) 0);
(= (- .......0 ....0) ...0);
(= (- ......0 ...0) ...0);
(= (- .......0 ...0) ....0);
(= (- ..0 0) ..0);
(= (- .0 0) .0);
(= (- ..0 ..0) 0);
(= (- ....0 ....0) 0);
# MATH introduce multiplication
(= (* 0 0) 0);
(= (* 0 .0) 0);
(= (* 0 ..0) 0);
(= (* 0 ...0) 0);
(= (* .0 0) 0);
(= (* .0 .0) .0);
(= (* .0 ..0) ..0);
(= (* .0 ...0) ...0);
(= (* ..0 0) 0);
(= (* ..0 .0) ..0);
(= (* ..0 ..0) ....0);
(= (* ..0 ...0) ......0);
(= (* ...0 0) 0);
(= (* ...0 .0) ...0);
(= (* ...0 ..0) ......0);
(= (* ...0 ...0) .........0);
(= (* ..0 0) 0);
(= (* ...0 ...0) .........0);
(= (* 0 ...0) 0);
(= (* 0 0) 0);
(= (* .0 0) 0);
(= (* .0 0) 0);
(= (* .0 0) 0);
(= (* ..0 ...0) ......0);
(= (* .0 ...0) ...0);
(= (* ...0 .0) ...0);
# MATH introduce doubling as a special case of multiplication
# as prelude to binary representation
(= (: 0) 0);
(= (: .0) ..0);
(= (: ..0) ....0);
(= (: ...0) ......0);
(= (: ....0) ........0);
(= 0 (: 0));
(= ..0 (: .0));
(= ....0 (: ..0));
(= ......0 (: ...0));
(= ........0 (: ....0));
(= (* 0 ..0) (: 0));
(= (* .0 ..0) (: .0));
(= (* ..0 ..0) (: ..0));
(= (* ...0 ..0) (: ...0));
(= (* ....0 ..0) (: ....0));
(= :0 (: 0));
(= :.0 (: .0));
(= :..0 (: ..0));
(= :...0 (: ...0));
(= :....0 (: ....0));
# MATH introduce a simple form of binary notation
# After this lesson, in the higher-level version of the message,
# will expand decimal to stand for the binary notation given.
(= 0 0);
(= .0 .0);
(= ..0 :.0);
(= ...0 .:.0);
(= ....0 ::.0);
(= .....0 .::.0);
(= ......0 :.:.0);
(= .......0 .:.:.0);
(= ........0 :::.0);
(= .........0 .:::.0);
(= ..........0 :.::.0);
(= ...........0 .:.::.0);
(= ............0 ::.:.0);
(= .............0 .::.:.0);
(= ..............0 :.:.:.0);
(= ...............0 .:.:.:.0);
(= :.::.0 ..........0);
(= :.0 ..0);
(= :.:.0 ......0);
(= .:.0 ...0);
(= .:.:.:.0 ...............0);
(= .::.:.0 .............0);
(= .:.0 ...0);
(= .::.:.0 .............0);
(= .::.0 .....0);
(= .:::.0 .........0);
(= .::.:.0 .............0);
(= .::.0 .....0);
(= .:.:.:.0 ...............0);
(= .:::.0 .........0);
(= :.:.0 ......0);
(= .:.:.0 .......0);
(= (+ ::.0 .::.:.0) .::::.0);
(= (+ .:.:.0 :.:.:.0) .::.::.0);
(= (+ .::.0 :.0) .:.:.0);
(= (+ .::.0 :.:.0) .:.::.0);
(= (+ :.:.0 ::.:.0) :.:::.0);
(= (+ .:.0 :.0) .::.0);
(= (+ .:.0 :::.0) .:.::.0);
(= (+ :::.0 .::.:.0) .::.::.0);
(= (* :.:.:.0 .:.:.0) :.::::.:.0);
(= (* :.::.0 ::.:.0) :::.:.:.:.0);
(= (* .:.::.0 .::.:.0) .:.:.:.::::.0);
(= (* .:::.0 ::.:.0) ::.:.::.:.0);
(= (* .::.:.0 ::.:.0) ::.:.:.:::.0);
(= (* :.::.0 ::.:.0) :::.:.:.:.0);
(= (* .:.:.:.0 .0) .:.:.:.0);
(= (* :.:.0 :.:.0) ::.:::.0);
# MATH demonstrate idea of leaving gaps in an expression
# and then filling them in afterwards
# the examples given leave a lot to be desired!
((? x (= (+ 10 x) 14)) 4);
((? x (= (+ 14 x) 29)) 15);
((? x (= (+ 9 x) 11)) 2);
((? x (= (+ 11 x) 22)) 11);
((? x (= (+ 10 x) 19)) 9);
((? x (= (+ 2 x) 14)) 12);
((? x (= (+ 6 x) 12)) 6);
((? x (= (+ 14 x) 22)) 8);
(((? x (? y (= (* x y) 22))) 2) 11);
(((? x (? y (= (* x y) 56))) 7) 8);
(((? x (? y (= (* x y) 30))) 5) 6);
(((? x (? y (= (* x y) 24))) 2) 12);
(((? x (? y (= (* x y) 105))) 7) 15);
(((? x (? y (= (* x y) 9))) 3) 3);
(((? x (? y (= (* x y) 90))) 6) 15);
(((? x (? y (= (* x y) 18))) 6) 3);
((((? x (? y (? z (= (* x y) z)))) 24) 12) 2);
((((? x (? y (? z (= (* x y) z)))) 120) 15) 8);
((((? x (? y (? z (= (* x y) z)))) 4) 4) 1);
((((? x (? y (? z (= (* x y) z)))) 121) 11) 11);
((((? x (? y (? z (= (* x y) z)))) 132) 11) 12);
((((? x (? y (? z (= (* x y) z)))) 26) 13) 2);
((((? x (? y (? z (= (* x y) z)))) 32) 8) 4);
((((? x (? y (? z (= (* x y) z)))) 0) 0) 12);
# MATH show some simple function calls
# and show a way to remember functions across statements
(= ((? square (square 6)) (? x (* x x))) 36);
(= ((? square (square 6)) (? x (* x x))) 36);
(= ((? square (square 5)) (? x (* x x))) 25);
(= ((? square (square 5)) (? x (* x x))) 25);
(= ((? square (square 0)) (? x (* x x))) 0);
(= ((? square (square 1)) (? x (* x x))) 1);
(= ((? square (square 2)) (? x (* x x))) 4);
(= ((? square (square 0)) (? x (* x x))) 0);
(define square (? x (* x x)));
(= (square 8) 64);
(= (square 5) 25);
(= (square 1) 1);
(= (square 8) 64);
(define plusone (? x (+ x 1)));
(= (plusone 3) 4);
(= (plusone 0) 1);
(= (plusone 7) 8);
(= (plusone 5) 6);
# MATH show mechanisms for branching
(= (if true 7 3) 7);
(= (if true 9 7) 9);
(= (if true 4 5) 4);
(= (if false 0 9) 9);
(= (if false 7 8) 8);
(= (if true 7 8) 7);
(= (if false 3 5) 5);
(= (if false 4 8) 8);
(= (if false 9 1) 1);
(= (if true 9 1) 9);
(= (if false 8 4) 4);
(= (if true 3 1) 3);
(= (if false 8 3) 3);
(= (if false 3 6) 6);
(= (if true 0 1) 0);
(= (if false 1 7) 7);
# MATH show an example of recursive evaluation
# skipping over a lot of definitions and desugarings
(define factorial (? x (if (> x 0) (* x (factorial (- x 1))) 1)));
(= (factorial 0) 1);
(= (factorial 1) 1);
(= (factorial 2) 2);
(= (factorial 3) 6);
(= (factorial 4) 24);
(= (factorial 5) 120);
# MATH introduce universal quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(< 5 (+ 5 1));
(< 4 (+ 4 1));
(< 3 (+ 3 1));
(< 2 (+ 2 1));
(< 1 (+ 1 1));
(< 0 (+ 0 1));
(forall (? x (< x (+ x 1))));
(< 5 (* 5 2));
(< 4 (* 4 2));
(< 3 (* 3 2));
(< 2 (* 2 2));
(< 1 (* 1 2));
(not (< 0 (* 0 2)));
(not (forall (? x (< x (* x 2)))));
# MATH introduce existential quantifier
# really need to link with sets for true correctness
# and the examples here are REALLY sparse, need much more
(not (= 5 (* 2 2)));
(= 4 (* 2 2));
(not (= 3 (* 2 2)));
(not (= 2 (* 2 2)));
(not (= 1 (* 2 2)));
(not (= 0 (* 2 2)));
(exists (? x (= x (* 2 2))));
(not (= 5 (+ 5 2)));
(not (= 4 (+ 4 2)));
(not (= 3 (+ 3 2)));
(not (= 2 (+ 2 2)));
(not (= 1 (+ 1 2)));
(not (= 0 (+ 0 2)));
(not (exists (? x (= x (+ x 2)))));
# MATH introduce logical implication
(=> true true);
(not (=> true false));
(=> false true);
(=> false false);
(forall x (forall y (=> (=> x y) (=> (not y) (not x)))));
# MATH introduce sets and set membership
(element 2 (set 6 1 4 7 2));
(element 7 (set 6 1 4 7 2));
(element 1 (set 6 1 4 7 2));
(element 1 (set 6 1 4 3 7 9));
(element 1 (set 6 1 4 3 7 9));
(element 1 (set 6 1 4 3 7 9));
(element 8 (set 8 1 7 9 5));
(element 5 (set 8 1 7 9 5));
(element 5 (set 8 1 7 9 5));
(element 9 (set 6 0 9));
(element 6 (set 6 0 9));
(element 9 (set 6 0 9));
(element 9 (set 8 3 7 9 5));
(element 3 (set 8 3 7 9 5));
(element 7 (set 8 3 7 9 5));
(not (element 6 (set 9 5)));
(not (element 6 (set 4 2 5)));
(not (element 8 (set 1 9 2)));
(not (element 6 (set 4 0 7 2 5)));
(not (element 8 (set 6 1 2 5)));
(= (set 1 5 9) (set 5 1 9));
(= (set 1 5 9) (set 9 1 5));
(not (= (set 1 5 9) (set 1 5)));
(element 5 (all (? x (= (+ x 10) 15))));
(element 3 (all (? x (= (* x 3) (+ x 6)))));
(define empty_set (set));
(element 0 natural_set);
(forall (? x (=> (element x natural_set) (element (+ x 1) natural_set))));
(element 1 natural_set);
(element 2 natural_set);
(element 3 natural_set);
(element 4 natural_set);
(element 5 natural_set);
(element 6 natural_set);
(element 7 natural_set);
(element 8 natural_set);
(element 9 natural_set);
(not (element true natural_set));
(not (element false natural_set));
(define boolean_set (set true false));
(element true boolean_set);
(element false boolean_set);
(not (element 0 boolean_set));
(define even_natural_set (all (? x (exists (? y (and (element y natural_set) (equals (* 2 y) x)))))));
(element 0 natural_set);
(element 0 even_natural_set);
(element 1 natural_set);
(not (element 1 even_natural_set));
(element 2 natural_set);
(element 2 even_natural_set);
(element 3 natural_set);
(not (element 3 even_natural_set));
(element 4 natural_set);
(element 4 even_natural_set);
(element 5 natural_set);
(not (element 5 even_natural_set));
(element 6 natural_set);
(element 6 even_natural_set);