# 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 numbers (in unary notation)

(intro (unary ));

(intro (unary (:)));

(intro (unary (:)(:)));

(intro (unary (:)(:)(:)));

(intro (unary (:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)));

(intro (unary (:)(:)(:)));

(intro (unary (:)(:)));

(intro (unary (:)));

(intro (unary ));

(intro (unary ));

(intro (unary (:)));

(intro (unary (:)(:)));

(intro (unary (:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary ));

(intro (unary (:)));

(intro (unary (:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary ));

(intro (unary (:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)));

(intro (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

# MATH now show equality

(intro =);

(= (unary ) (unary ));

(= (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)));

(= (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)));

(= (unary (:)(:)) (unary (:)(:)));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

# MATH now show other relational operators

(intro >);

(> (unary (:)(:)(:)) (unary (:)));

(> (unary (:)) (unary ));

(> (unary (:)(:)(:)(:)(:)(:)) (unary ));

(> (unary (:)(:)(:)(:)) (unary ));

(> (unary (:)(:)(:)(:)(:)) (unary ));

(> (unary (:)(:)(:)(:)) (unary ));

(> (unary (:)) (unary ));

(> (unary (:)(:)(:)(:)(:)(:)) (unary (:)));

(> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)));

(> (unary (:)(:)(:)) (unary (:)));

(> (unary (:)(:)(:)(:)(:)) (unary ));

(intro <);

(< (unary ) (unary (:)(:)(:)(:)(:)(:)));

(< (unary ) (unary (:)));

(< (unary ) (unary (:)));

(< (unary ) (unary (:)(:)));

(< (unary (:)) (unary (:)(:)(:)));

(< (unary ) (unary (:)(:)));

(< (unary (:)(:)) (unary (:)(:)(:)(:)));

(< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)));

(< (unary ) (unary (:)(:)));

(< (unary ) (unary (:)(:)(:)(:)(:)));

(< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)));

(< (unary (:)(:)) (unary (:)(:)(:)));

(> (unary (:)(:)) (unary (:)));

(> (unary (:)(:)(:)(:)(:)) (unary (:)));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

(> (unary (:)) (unary ));

(< (unary (:)) (unary (:)(:)(:)(:)));

(= (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)));

(> (unary (:)(:)(:)) (unary (:)(:)));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

(< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)));

# MATH introduce the NOT logical operator

(intro not);

(= (unary (:)) (unary (:)));

(not (< (unary (:)) (unary (:))));

(not (> (unary (:)) (unary (:))));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

(not (< (unary (:)(:)(:)) (unary (:)(:)(:))));

(not (> (unary (:)(:)(:)) (unary (:)(:)(:))));

(= (unary ) (unary ));

(not (< (unary ) (unary )));

(not (> (unary ) (unary )));

(= (unary (:)(:)(:)) (unary (:)(:)(:)));

(not (< (unary (:)(:)(:)) (unary (:)(:)(:))));

(not (> (unary (:)(:)(:)) (unary (:)(:)(:))));

(= (unary (:)) (unary (:)));

(not (< (unary (:)) (unary (:))));

(not (> (unary (:)) (unary (:))));

(= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (= (unary (:)) (unary (:)(:)(:)(:))));

(< (unary (:)));

(not (> (unary (:)) (unary (:)(:)(:)(:))));

(not (= (unary (:)(:)) (unary (:)(:)(:)(:))));

(< (unary (:)(:)));

(not (> (unary (:)(:)) (unary (:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(< (unary (:)(:)(:)(:)(:)));

(not (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(< (unary (:)(:)(:)(:)(:)));

(not (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(not (= (unary (:)) (unary (:)(:)(:))));

(< (unary (:)));

(not (> (unary (:)) (unary (:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(< (unary (:)(:)(:)(:)(:)));

(not (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(> (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(> (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (= (unary (:)(:)(:)) (unary (:))));

(> (unary (:)(:)(:)) (unary (:)));

(not (< (unary (:)(:)(:)) (unary (:))));

(not (= (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(> (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (= (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))));

(> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)));

(not (< (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))));

# MATH introduce the AND logical operator

(intro and);

(and (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))) (> (unary (:)(:)(:)(:)) (unary (:)(:)(:))));

(and (= (unary (:)) (unary (:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(and (> (unary (:)(:)(:)(:)) (unary (:)(:)(:))) (> (unary (:)(:)(:)(:)) (unary (:))));

(and (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(and (> (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (= (unary (:)(:)) (unary (:)(:))));

(and (< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(and (= (unary (:)(:)) (unary (:)(:))) (< (unary ) (unary (:)(:))));

(and (> (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (= (unary (:)(:)) (unary (:)(:))));

(and (< (unary (:)) (unary (:)(:)(:)(:))) (= (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(and (< (unary (:)) (unary (:)(:))) (= (unary (:)(:)) (unary (:)(:))));

(not (and (> (unary (:)(:)(:)(:)) (unary (:)(:)(:))) (> (unary ) (unary (:)))));

(not (and (< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:))) (= (unary (:)(:)) (unary (:)(:)(:)(:)))));

(not (and (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)) (unary (:)(:)(:)(:)(:)))));

(not (and (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (= (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)))));

(not (and (= (unary (:)) (unary (:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)))));

(not (and (> (unary (:)(:)) (unary (:)(:)(:))) (< (unary (:)) (unary (:)(:)(:)))));

(not (and (< (unary (:)(:)(:)(:)(:)(:)) (unary (:))) (> (unary (:)(:)(:)) (unary (:)(:)))));

(not (and (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (> (unary (:)(:)) (unary ))));

(not (and (= (unary (:)) (unary )) (> (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)))));

(not (and (> (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:))) (< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)))));

(not (and (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)))));

(not (and (= (unary (:)(:)(:)(:)) (unary )) (> (unary ) (unary (:)(:)(:)))));

(not (and (= (unary (:)(:)(:)(:)(:)) (unary )) (> (unary (:)(:)(:)) (unary (:)(:)(:)))));

(not (and (> (unary ) (unary (:)(:)(:)(:))) (> (unary (:)(:)) (unary (:)(:)))));

(not (and (= (unary ) (unary (:)(:)(:)(:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)))));

(not (and (< (unary (:)(:)) (unary (:)(:)(:)(:))) (< (unary (:)(:)(:)) (unary (:)))));

(and (< (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)(:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(not (and (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))) (> (unary (:)(:)) (unary (:)(:)(:)))));

(not (and (> (unary (:)) (unary )) (< (unary (:)(:)(:)) (unary (:)(:)))));

(and (< (unary ) (unary (:)(:))) (> (unary (:)) (unary )));

(not (and (= (unary (:)(:)(:)(:)) (unary (:))) (> (unary ) (unary (:)(:)(:)))));

(not (and (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (= (unary (:)(:)) (unary (:)(:)))));

(not (and (= (unary (:)(:)) (unary (:))) (> (unary (:)) (unary (:)(:)(:)))));

(not (and (> (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:))) (= (unary (:)) (unary (:)))));

(not (and (> (unary (:)(:)) (unary (:)(:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)))));

# MATH introduce the OR logical operator

(intro or);

(or (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))));

(or (< (unary (:)) (unary (:)(:))) (> (unary (:)(:)) (unary )));

(or (> (unary (:)(:)(:)(:)) (unary (:))) (< (unary (:)(:)) (unary (:)(:)(:)(:))));

(or (< (unary (:)) (unary (:)(:)(:)(:))) (> (unary (:)) (unary )));

(or (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (= (unary ) (unary )));

(or (> (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(or (> (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(or (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:)(:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:)(:))));

(or (= (unary ) (unary )) (= (unary (:)(:)) (unary (:)(:))));

(or (< (unary ) (unary (:)(:)(:))) (= (unary ) (unary )));

(or (< (unary ) (unary (:)(:))) (= (unary (:)(:)(:)(:)) (unary (:)(:))));

(or (> (unary (:)(:)(:)) (unary (:))) (= (unary ) (unary (:)(:))));

(or (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (= (unary (:)) (unary (:)(:)(:)(:)(:))));

(or (< (unary (:)(:)) (unary (:)(:)(:)(:))) (< (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(or (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:))) (> (unary (:)(:)) (unary (:)(:)(:)(:))));

(or (> (unary ) (unary (:)(:)(:)(:))) (= (unary ) (unary )));

(or (= (unary (:)(:)) (unary )) (< (unary ) (unary (:)(:))));

(or (< (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(or (= (unary (:)(:)) (unary )) (= (unary ) (unary )));

(or (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (< (unary (:)) (unary (:)(:))));

(not (or (> (unary (:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)))));

(not (or (> (unary (:)(:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)(:)) (unary (:)(:)(:)(:)(:)))));

(not (or (> (unary (:)(:)(:)) (unary (:)(:)(:)(:))) (= (unary (:)) (unary ))));

(not (or (> (unary (:)(:)(:)) (unary (:)(:)(:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)))));

(not (or (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (> (unary ) (unary ))));

(not (or (> (unary ) (unary (:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)))));

(not (or (> (unary (:)) (unary (:)(:)(:)(:)(:)(:))) (< (unary (:)(:)) (unary ))));

(or (> (unary ) (unary (:)(:)(:))) (> (unary (:)(:)(:)(:)) (unary (:)(:)(:))));

(or (< (unary (:)(:)(:)(:)) (unary )) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:)(:))));

(or (= (unary (:)(:)(:)) (unary (:)(:)(:))) (= (unary (:)(:)) (unary (:)(:))));

(not (or (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:))) (< (unary (:)(:)) (unary (:)))));

(or (> (unary (:)(:)(:)(:)) (unary (:))) (> (unary (:)) (unary (:)(:)(:)(:)(:)(:))));

(or (< (unary (:)(:)(:)(:)) (unary (:)(:)(:))) (= (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(not (or (> (unary ) (unary )) (= (unary (:)(:)) (unary (:)(:)(:)))));

(or (> (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (< (unary (:)(:)(:)) (unary (:))));

# MATH use equality for truth values

(= (> (unary (:)(:)(:)(:)) (unary (:)(:))) (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))));

(= (= (unary (:)(:)) (unary (:)(:))) (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)(:))));

(= (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (> (unary (:)(:)(:)) (unary (:))));

(= (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(= (= (unary (:)(:)) (unary (:)(:))) (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(= (= (unary (:)(:)(:)) (unary (:)(:))) (= (unary (:)) (unary )));

(= (> (unary ) (unary (:))) (< (unary (:)(:)(:)(:)) (unary (:))));

(= (> (unary (:)) (unary (:)(:)(:)(:)(:))) (> (unary (:)(:)(:)) (unary (:)(:)(:))));

(= (> (unary (:)(:)) (unary (:)(:)(:)(:)(:))) (< (unary (:)) (unary )));

(= (= (unary (:)(:)(:)) (unary (:)(:)(:)(:))) (= (unary ) (unary (:)(:)(:)(:))));

(not (= (= (unary (:)) (unary )) (< (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:)))));

(not (= (= (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (= (unary ) (unary ))));

(not (= (< (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)))));

(not (= (= (unary ) (unary (:))) (> (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)))));

(not (= (> (unary (:)) (unary (:)(:)(:)(:))) (< (unary (:)(:)(:)) (unary (:)(:)(:)(:)))));

(not (= (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))) (= (unary (:)(:)(:)(:)) (unary (:)))));

(not (= (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))) (> (unary (:)(:)(:)) (unary (:)(:)(:)(:)))));

(not (= (< (unary ) (unary (:)(:))) (= (unary (:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)))));

(not (= (> (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (< (unary (:)(:)) (unary ))));

(not (= (< (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))) (= (unary (:)(:)(:)) (unary ))));

(intro true);

(intro false);

(= (true) (= (unary (:)(:)(:)) (unary (:)(:)(:))));

(= (true) (= (unary ) (unary )));

(= (true) (> (unary (:)(:)(:)(:)(:)) (unary (:)(:))));

(= (true) (< (unary (:)(:)(:)) (unary (:)(:)(:)(:))));

(= (true) (> (unary (:)(:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:)(:))));

(= (< (unary (:)) (unary (:)(:)(:)(:))) (true));

(= (< (unary (:)(:)(:)) (unary (:)(:)(:)(:))) (true));

(= (= (unary (:)(:)(:)) (unary (:)(:)(:))) (true));

(= (< (unary (:)(:)(:)) (unary (:)(:)(:)(:))) (true));

(= (= (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:))) (true));

(= (false) (> (unary (:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(= (false) (= (unary (:)(:)) (unary (:)(:)(:)(:))));

(= (false) (< (unary (:)(:)) (unary )));

(= (false) (> (unary (:)(:)(:)) (unary (:)(:)(:)(:)(:)(:))));

(= (false) (< (unary (:)(:)(:)(:)) (unary (:)(:)(:))));

(= (> (unary (:)(:)) (unary (:)(:)(:)(:)(:))) (false));

(= (= (unary (:)(:)) (unary (:))) (false));

(= (= (unary (:)(:)) (unary (:)(:)(:)(:)(:))) (false));

(= (< (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:))) (false));

(= (< (unary (:)(:)(:)) (unary (:))) (false));

(= (true) (true));

(= (false) (false));

(not (= (true) (false)));

(not (= (false) (true)));

# MATH introduce addition

(intro +);

(= (+ (unary (:)(:)(:)) (unary (:)(:)(:)(:))) (unary (:)(:)(:)(:)(:)(:)(:)));

(= (+ (unary ) (unary (:)(:)(:))) (unary (:)(:)(:)));

(= (+ (unary ) (unary (:)(:)(:))) (unary (:)(:)(:)));

(= (+ (unary (:)) (unary )) (unary (:)));

(= (+ (unary ) (unary )) (unary ));

(= (+ (unary (:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)));

(= (+ (unary (:)) (unary )) (unary (:)));

(= (+ (unary (:)) (unary )) (unary (:)));

(= (+ (unary (:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)(:)));

(= (+ (unary ) (unary )) (unary ));

# MATH introduce subtraction

(intro -);

(= (- (unary (:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)));

(= (- (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)));

(= (- (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:)(:))) (unary (:)(:)(:)));

(= (- (unary (:)(:)(:)(:)(:)) (unary (:)(:))) (unary (:)(:)(:)));

(= (- (unary (:)) (unary (:))) (unary ));

(= (- (unary ) (unary )) (unary ));

(= (- (unary (:)(:)) (unary )) (unary (:)(:)));

(= (- (unary (:)(:)(:)(:)(:)(:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)));

(= (- (unary (:)(:)(:)(:)) (unary (:)(:)(:)(:))) (unary ));

(= (- (unary (:)(:)(:)) (unary )) (unary (:)(:)(:)));

# MATH introduce multiplication

(intro *);

(= (* (unary ) (unary )) (unary ));

(= (* (unary ) (unary (:))) (unary ));

(= (* (unary ) (unary (:)(:))) (unary ));

(= (* (unary ) (unary (:)(:)(:))) (unary ));

(= (* (unary (:)) (unary )) (unary ));

(= (* (unary (:)) (unary (:))) (unary (:)));

(= (* (unary (:)) (unary (:)(:))) (unary (:)(:)));

(= (* (unary (:)) (unary (:)(:)(:))) (unary (:)(:)(:)));

(= (* (unary (:)(:)) (unary )) (unary ));

(= (* (unary (:)(:)) (unary (:))) (unary (:)(:)));

(= (* (unary (:)(:)) (unary (:)(:))) (unary (:)(:)(:)(:)));

(= (* (unary (:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)(:)(:)));

(= (* (unary (:)(:)(:)) (unary )) (unary ));

(= (* (unary (:)(:)(:)) (unary (:))) (unary (:)(:)(:)));

(= (* (unary (:)(:)(:)) (unary (:)(:))) (unary (:)(:)(:)(:)(:)(:)));

(= (* (unary (:)(:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (* (unary (:)(:)(:)) (unary )) (unary ));

(= (* (unary ) (unary (:))) (unary ));

(= (* (unary ) (unary (:))) (unary ));

(= (* (unary ) (unary (:))) (unary ));

(= (* (unary ) (unary (:)(:))) (unary ));

(= (* (unary (:)(:)(:)) (unary (:))) (unary (:)(:)(:)));

(= (* (unary (:)(:)(:)) (unary (:)(:)(:))) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (* (unary (:)) (unary (:)(:))) (unary (:)(:)));

(= (* (unary ) (unary (:))) (unary ));

(= (* (unary ) (unary (:)(:)(:))) (unary ));

# 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.

(= (unary ) (.));

(= (unary (:)) (:));

(= (unary (:)(:)) (:.));

(= (unary (:)(:)(:)) (::));

(= (unary (:)(:)(:)(:)) (:..));

(= (unary (:)(:)(:)(:)(:)) (:.:));

(= (unary (:)(:)(:)(:)(:)(:)) (::.));

(= (unary (:)(:)(:)(:)(:)(:)(:)) (:::));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)) (:...));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)) (:..:));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (:.:.));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (:.::));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (::..));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (::.:));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (:::.));

(= (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)) (::::));

(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (::) (unary (:)(:)(:)));

(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (:.:) (unary (:)(:)(:)(:)(:)));

(= (:..:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (:.:) (unary (:)(:)(:)(:)(:)));

(= (::::) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (:..:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (::.) (unary (:)(:)(:)(:)(:)(:)));

(= (:::) (unary (:)(:)(:)(:)(:)(:)(:)));

(= (:..) (unary (:)(:)(:)(:)));

(= (::.:) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (:::) (unary (:)(:)(:)(:)(:)(:)(:)));

(= (:::.) (unary (:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)(:)));

(= (:.:) (unary (:)(:)(:)(:)(:)));

(= (+ (:.) (:.:)) (:::));

(= (+ (::.) (::.)) (::..));

(= (+ (::..) (::)) (::::));

(= (+ (:.) (::)) (:.:));

(= (+ (:...) (:...)) (:....));

(= (+ (::.:) (:::.)) (::.::));

(= (+ (:::) (:.:.)) (:...:));

(= (+ (::..) (:.::)) (:.:::));

(= (* (::.:) (:..:)) (:::.:.:));

(= (* (::..) (::.:)) (:..:::..));

(= (* (::..) (:.:.)) (::::...));

(= (* (::..) (::::)) (:.::.:..));

(= (* (:) (::.)) (::.));

(= (* (::.) (:.:.)) (::::..));

(= (* (:..) (:::.)) (:::...));

(= (* (::::) (:..:)) (:....:::));

# 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 (= (+ 2 (x)) 13)) 11);

((? x (= (+ 11 (x)) 21)) 10);

((? x (= (+ 9 (x)) 11)) 2);

((? x (= (+ 12 (x)) 18)) 6);

((? x (= (+ 6 (x)) 20)) 14);

((? x (= (+ 8 (x)) 10)) 2);

((? x (= (+ 11 (x)) 18)) 7);

((? x (= (+ 8 (x)) 13)) 5);

(((? x (? y (= (* (x) (y)) 12))) 6) 2);

(((? x (? y (= (* (x) (y)) 84))) 12) 7);

(((? x (? y (= (* (x) (y)) 45))) 15) 3);

(((? x (? y (= (* (x) (y)) 18))) 3) 6);

(((? x (? y (= (* (x) (y)) 90))) 15) 6);

(((? x (? y (= (* (x) (y)) 36))) 3) 12);

(((? x (? y (= (* (x) (y)) 30))) 2) 15);

(((? x (? y (= (* (x) (y)) 32))) 8) 4);

((((? x (? y (? z (= (* (x) (y)) (z))))) 11) 1) 11);

((((? x (? y (? z (= (* (x) (y)) (z))))) 121) 11) 11);

((((? x (? y (? z (= (* (x) (y)) (z))))) 156) 12) 13);

((((? x (? y (? z (= (* (x) (y)) (z))))) 16) 2) 8);

((((? x (? y (? z (= (* (x) (y)) (z))))) 0) 4) 0);

((((? x (? y (? z (= (* (x) (y)) (z))))) 108) 12) 9);

((((? x (? y (? z (= (* (x) (y)) (z))))) 80) 10) 8);

((((? x (? y (? z (= (* (x) (y)) (z))))) 8) 8) 1);

# MATH show some simple function calls

# and show a way to remember functions across statements

(= ((? square (square 1)) (? x (* (x) (x)))) 1);

(= ((? square (square 2)) (? x (* (x) (x)))) 4);

(= ((? square (square 0)) (? x (* (x) (x)))) 0);

(= ((? square (square 8)) (? x (* (x) (x)))) 64);

(= ((? square (square 5)) (? x (* (x) (x)))) 25);

(= ((? square (square 1)) (? x (* (x) (x)))) 1);

(= ((? square (square 8)) (? x (* (x) (x)))) 64);

(= ((? square (square 3)) (? x (* (x) (x)))) 9);

(define square (? x (* (x) (x))));

(= (square 0) 0);

(= (square 7) 49);

(= (square 5) 25);

(= (square 6) 36);

(define plusone (? x (+ (x) 1)));

(= (plusone 7) 8);

(= (plusone 3) 4);

(= (plusone 6) 7);

(= (plusone 9) 10);

# MATH show mechanisms for branching

(intro if);

(= (if (true) 8 4) 8);

(= (if (true) 0 0) 0);

(= (if (true) 2 7) 2);

(= (if (true) 9 7) 9);

(= (if (true) 0 3) 0);

(= (if (true) 0 4) 0);

(= (if (true) 4 9) 4);

(= (if (false) 7 9) 9);

(= (if (false) 0 8) 8);

(= (if (false) 6 3) 3);

(= (if (false) 2 8) 8);

(= (if (false) 0 3) 3);

(= (if (true) 8 0) 8);

(= (if (false) 2 1) 1);

(= (if (true) 4 7) 4);

(= (if (false) 2 6) 6);

# 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

(intro forall);

(< 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)));

(intro exists);

(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

(intro =>);

(=> (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 7 (set 1 7 9 2));

(element 1 (set 1 7 9 2));

(element 7 (set 1 7 9 2));

(element 6 (set 6 3 9 2 5));

(element 2 (set 6 3 9 2 5));

(element 5 (set 6 3 9 2 5));

(element 6 (set 6 0 7 9));

(element 7 (set 6 0 7 9));

(element 9 (set 6 0 7 9));

(element 0 (set 8 0 7 9 5));

(element 5 (set 8 0 7 9 5));

(element 5 (set 8 0 7 9 5));

(element 2 (set 7 9 2 5));

(element 2 (set 7 9 2 5));

(element 5 (set 7 9 2 5));

(not (element 6 (set 4 2 5)));

(not (element 8 (set 1 9 2 5)));

(not (element 6 (set 4 0 7 9 5)));

(not (element 8 (set 6 1 2 5)));

(not (element 6 (set 8 3 7 2)));

(= (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));

# MATH illustrate lists and some list operators

# still using examples rather than definition by formula -

# could change this to reduce ambiguity, but that would create

# more order constraints in the lessons

(= (head (list 0)) 0);

(= (tail (list 0)) (list));

(= (head (list 6 11 19)) 6);

(= (tail (list 6 11 19)) (list 11 19));

(= (head (list 12 2 15)) 12);

(= (tail (list 12 2 15)) (list 2 15));

(= (head (list 19 3 4 4 2 15 3)) 19);

(= (tail (list 19 3 4 4 2 15 3)) (list 3 4 4 2 15 3));

(= (head (list 6 11 3 2 15 2 19 15 12)) 6);

(= (tail (list 6 11 3 2 15 2 19 15 12)) (list 11 3 2 15 2 19 15 12));

(= (head (list 11 0 12 14 8 17 5 9 11)) 11);

(= (tail (list 11 0 12 14 8 17 5 9 11)) (list 0 12 14 8 17 5 9 11));

(= (head (list 10)) 10);

(= (tail (list 10)) (list));

(= (head (list 9 4 19 10)) 9);

(= (tail (list 9 4 19 10)) (list 4 19 10));

(= (head (list 8 4 2 7 12 18 9 13)) 8);

(= (tail (list 8 4 2 7 12 18 9 13)) (list 4 2 7 12 18 9 13));

(= (head (list 0)) 0);

(= (tail (list 0)) (list));

(= (list-ref (list 10 1 9) 2) 9);

(= (list-ref (list 4 4 14 0 14 4 17 7 3 17) 0) 4);

(= (list-ref (list 10 13 6 14 3 13 9 18) 0) 10);

(= (list-ref (list 3 1 0 2) 2) 0);

(= (list-ref (list 13 7 18 13 12) 1) 7);

(= (list-ref (list 19 16 9) 2) 9);

(= (list-ref (list 12 14 5 14 4) 4) 4);

(= (list-ref (list 10 17) 1) 17);

(= (list-ref (list 1 12 10 18) 3) 18);

(= (list-ref (list 17 7 2 4 19 15 4 9) 0) 17);

(= (list) (list));

(= (list 7) (list 7));

(= (list 1 19) (list 1 19));

(= (list 18 1 18) (list 18 1 18));

(= (list 13 15 10 6) (list 13 15 10 6));

# this next batch of examples are a bit misleading, should streamline

(not (= (list) (list 0)));

(not (= (list) (list 6)));

(not (= (list 9) (list 6 9)));

(not (= (list 9) (list 9 7)));

(not (= (list 1 6) (list 2 1 6)));

(not (= (list 1 6) (list 1 6 0)));

(not (= (list 10 9 12) (list 5 10 9 12)));

(not (= (list 10 9 12) (list 10 9 12 3)));

(not (= (list 17 9 1 0) (list 4 17 9 1 0)));

(not (= (list 17 9 1 0) (list 17 9 1 0 4)));

# some helpful functions

(= (prepend 12 (list)) (list 12));

(= (prepend 0 (list 14)) (list 0 14));

(= (prepend 10 (list 8 19)) (list 10 8 19));

(= (prepend 12 (list 10 2 1)) (list 12 10 2 1));

(= (prepend 14 (list 6 16 14 5)) (list 14 6 16 14 5));

(= (prepend 4 (list 15 2 3 11 8)) (list 4 15 2 3 11 8));

(= (prepend 12 (list 9 2 19 7 2 0)) (list 12 9 2 19 7 2 0));

(= (prepend 11 (list 17 17 2 4 16 5 14)) (list 11 17 17 2 4 16 5 14));

(define list-length (? x (if (= (x) (list)) 0 (+ 1 (list-length (tail (x)))))));

(= (list-length (list 6 8 2)) 3);

(= (list-length (list 0 6 4 1 2 8 7 3)) 8);

(= (list-length (list 7 2 1 4 3 0 9 5 6)) 9);

(= (list-length (list 1 0 4 2 7 9 5)) 7);

(= (list-length (list 1)) 1);

(define pair (? x (? y (list (x) (y)))));

(= (pair 5 9) (list 5 9));

(= (first (pair 5 9)) 5);

(= (second (pair 5 9)) 9);

(= (pair 0 7) (list 0 7));

(= (first (pair 0 7)) 0);

(= (second (pair 0 7)) 7);

(= (pair 1 5) (list 1 5));

(= (first (pair 1 5)) 1);

(= (second (pair 1 5)) 5);

# Note that in functions like the next one, there is no care taken to deal

# with error conditions. We simply don't say what happens in such cases.

# As long as we avoid such situations, then this is not a problem.

(define find-list (? lst (? key (if (= (head (lst)) (key)) 0 (+ (find-list (tail (lst)) (key)) 1)))));

(= (list-find (list 11 14 16) 16) 2);

(= (list-find (list 16 19 9 9) 19) 1);

(= (list-find (list 19 3 14 5 15 3 10 15 12 0) 3) 1);

(= (list-find (list 14 12 4 0 3 15 4 18 16) 18) 7);

(= (list-find (list 2 3 19 14 14 13 11 15) 13) 5);

(= (list-find (list 5 19 15 13 3 5 3 12 5) 19) 1);

(= (list-find (list 3 18 15 0 1) 18) 1);

(= (list-find (list 12 1 6 15 3 13 3) 3) 4);

(= (list-find (list 19 16) 19) 0);

(= (list-find (list 17 11 13 4 7 1 12 12) 1) 5);

# MATH build up functions of several variables

(= ((? x (? y (- (x) (y)))) 6 3) 3);

(= ((? x (? y (- (x) (y)))) 14 9) 5);

(= ((? x (? y (- (x) (y)))) 1 1) 0);

(= ((? x (? y (- (x) (y)))) 1 0) 1);

(= ((? x (? y (- (x) (y)))) 18 9) 9);

(intro lambda);

(= (? x (- (x) 5)) (lambda (x) (- (x) 5)));

(= (? x (? y (- (x) (y)))) (lambda (x y) (- (x) (y))));

(= ((lambda (x y) (- (x) (y))) 4 1) 3);

(= ((lambda (x y) (- (x) (y))) 6 1) 5);

(= ((lambda (x y) (- (x) (y))) 6 5) 1);

(= ((lambda (x y) (- (x) (y))) 8 3) 5);

(= ((lambda (x y) (- (x) (y))) 11 3) 8);

(define apply (lambda (x y) (if (= (y) (list)) (x) (apply ((x) (head (y))) (tail (y))))));

(= (apply (lambda (x y) (- (x) (y))) (list 11 5)) 6);

(= (apply (lambda (x y) (- (x) (y))) (list 12 7)) 5);

(= (apply (lambda (x y) (- (x) (y))) (list 6 3)) 3);

(= (apply (lambda (x y) (- (x) (y))) (list 11 8)) 3);

(= (apply (lambda (x y) (- (x) (y))) (list 9 5)) 4);

# MATH show map function for applying a function across the elements of a list

(define map (lambda (p lst) (if (> (list-length (lst)) 0) (prepend (p (head (lst))) (map (p) (tail (lst)))))));

(= (map (? x (* (x) 2)) (list 11 16 7)) (list 22 32 14));

(= (map (? x (* (x) 2)) (list 2 13 8 12)) (list 4 26 16 24));

(= (map (? x (* (x) 2)) (list 10 9 11 18 15)) (list 20 18 22 36 30));

(= (map (? x (* (x) 2)) (list 17 8 9 7 14 13)) (list 34 16 18 14 28 26));

(= (map (? x 42) (list 2 18 17)) (list 42 42 42));

(= (map (? x 42) (list 6 15 12 17)) (list 42 42 42 42));

(= (map (? x 42) (list 15 6 10 17 13)) (list 42 42 42 42 42));

(= (map (? x 42) (list 8 9 3 10 17 18)) (list 42 42 42 42 42 42));

# MATH introduce mutable objects, and side-effects

(intro make-cell);

(intro set!);

(intro get!);

(define demo-mut1 (make-cell 0));

(set! (demo-mut1) 15);

(= (get! (demo-mut1)) 15);

(set! (demo-mut1) 5);

(set! (demo-mut1) 7);

(= (get! (demo-mut1)) 7);

(define demo-mut2 (make-cell 11));

(= (get! (demo-mut2)) 11);

(set! (demo-mut2) 22);

(= (get! (demo-mut2)) 22);

(= (get! (demo-mut1)) 7);

(= (+ (get! (demo-mut1)) (get! (demo-mut2))) 29);

(if (= (get! (demo-mut1)) 7) (set! (demo-mut1) 88) (set! (demo-mut1) 99));

(= (get! (demo-mut1)) 88);

(if (= (get! (demo-mut1)) 7) (set! (demo-mut1) 88) (set! (demo-mut1) 99));

(= (get! (demo-mut1)) 99);

# MATH introduce sugar for let

# if would be good to introduce desugarings more rigorously, but for now...

# ... just a very vague sketch

(intro let);

(= (let ((x 10)) (+ (x) 5)) ((? x (+ (x) 5)) 10));

(= (let ((x 10) (y 5)) (+ (x) (y))) (((? x (? y (+ (x) (y)))) 10) 5));

# MATH introduce environment/hashmap structure

# this section needs a LOT more examples :-)

# note that at the time of writing (h 1 2) is same as ((h) 1 2)

(define hash-add (lambda (h x y z) (if (= (z) (x)) (y) (h (z)))));

(define hash-ref (lambda (h x) (h (x))));

(define hash-null (? x (undefined)));

(define test-hash (hash-add (hash-add (hash-null) 3 2) 4 9));

(= (hash-ref (test-hash) 4) 9);

(= (hash-ref (test-hash) 3) 2);

(= (hash-ref (test-hash) 8) (undefined));

(= (hash-ref (test-hash) 15) (undefined));

(= (hash-ref (hash-add (test-hash) 15 33) 15) 33);

(= (hash-ref (test-hash) 15) (undefined));

(define make-hash (? x (= (x) (list)) (hash-null) (hash-add (make-hash (tail (x))) (first (head (x))) (second (head (x))))));

(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 3) 10);

(= (hash-ref (make-hash (list (pair 3 10) (pair 2 20) (pair 1 30))) 1) 30);

# MATH show a pattern matching mechanism

# just by example, not definition, for now

# it is a bit subtle to be relying on examples only.

# especially as few as there are right now.

(intro match);

(= ((match x (pair (true) 2) (pair (false) 3) (pair (true) (x))) 42) 2);

(= ((match x (pair (false) 3) (pair (true) (x)) (pair (true) 2)) 42) 42);

(= ((match x (pair (true) 2) (pair (false) 3) (pair (true) 4)) 42) 2);

(= ((match x (pair (false) 3) (pair (true) 4) (pair (true) 2)) 42) 4);

(define test-match1 (match x (pair (= (x) 42) 10) (? y (pair (and (= (x) (* (y) 2)) (element (y) (natural_set))) (y))) (pair (true) 3)));

(= (test-match1 42) 10);

(= (test-match1 100) 50);

(= (test-match1 30) 15);

(= (test-match1 33) 3);

(= (test-match1 39) 3);

# MATH introduce a basic type system

# not really sure how this is going to work out

# need to implement domain constructors T+T / T*T / T->T / etc

(intro type);

(define get-type-base (make-cell (? x ((match e (list (pair (element (e) (natural_set)) integer) (pair (element (e) (boolean_set)) boolean) (? T (pair (= (first (e)) (type (T))) (T))) (pair (true) (undefined)))) (x)))));

(define get-type (get! (get-type-base)));

# above leaves a hook for incrementally introducing new basic types

(define get-raw (? x ((match e (list (pair (element (e) (natural_set)) (e)) (pair (element (e) (boolean_set)) (e)) (? T (pair (= (first (e)) (type (T))) (second (e)))) (pair (true) (undefined)))) (x))));

(define typed (? x (pair (type (get-type (x))) (get-raw (x)))));

(= (get-type 13) integer);

(= (get-type 10) integer);

(= (get-type 3) integer);

(= (get-type 17) integer);

(= (get-type 15) integer);

(forall (? x (=> (element (x) (natural_set)) (= (get-type (x)) integer))));

(= (get-type (true)) boolean);

(= (get-type (false)) boolean);

(= (typed 11) (type integer 11));

(= (typed 16) (type integer 16));

(= (typed 15) (type integer 15));

(= (typed (type integer 9)) (type integer 9));

(= (typed (type integer 7)) (type integer 7));

(= (typed (type integer 1)) (type integer 1));

(forall (? x (forall (? y (=> (and (= (get-type (x)) integer) (= (get-type (y)) integer)) (= (+ (x) (y)) (+ (get-raw (x)) (get-raw (y)))))))));

(= (+ (type integer 5) (type integer 10)) 15);

(define type-compatible-integer-primop (? op (forall (? x (forall (? y (=> (and (= (get-type (x)) integer) (= (get-type (y)) integer)) (= (op (x) (y)) (op (get-raw (x)) (get-raw (y)))))))))));

(type-compatible-integer-primop +);

(type-compatible-integer-primop *);

(type-compatible-integer-primop -);

(type-compatible-integer-primop =);

# note constraint to integers for now

(= (type integer 5) 5);

# There is a lot to add here to layer types over existing infrastructure.

# Let's just pretend it is here and doesn't involve any serious contradictions!

# give a typed version of lambda by example - really need to define this!

(= (lambda ((x integer) (y boolean)) (if (y) (x) 0)) (lambda (x y) (if (and (= (get-type (x)) integer) (= (get-type (y)) boolean)) (if (y) (x) 0) (undefined))));

# MATH introduce graph structures

define make-graph (lambda (nodes links) (pair (nodes) (links)));

define test-graph (make-graph (list g1 g2 g3 g4) (list (pair g1 g2) (pair g2 g3) (pair g1 g4)));

define graph-linked (lambda (g n1 n2) (exists (? idx (= (list-ref (second (g)) (idx)) (pair (n1) (n2))))));

(= (graph-linked (test-graph) g1 g2) (true));

(= (graph-linked (test-graph) g1 g3) (false));

(= (graph-linked (test-graph) g2 g4) (false));

(define graph-linked* (lambda (g n1 n2) (or (= (n1) (n2)) (or (graph-linked (g) (n1)) (exists (? n3 (and (graph-linked (g) (n1) (n3)) (graph-linked* (g) (n3) (n2)))))))));

(= (graph-linked* (test-graph) g1 g2) (true));

(= (graph-linked* (test-graph) g1 g3) (true));

(= (graph-linked* (test-graph) g2 g4) (false));

# OBJECT introduce simple mutable structures

(define mutable-struct (? lst (let ((data (map (? x (make-cell 0)) (lst)))) (? key (list-ref (data) (find-list (lst) (key)))))));

(define test-struct1 (mutable-struct (list item1 item2 item3)));

(set! (test-struct1 item1) 15);

(= (get! (test-struct1 item1)) 15);

# OBJECT introduce method handler wrappers

define add-method (lambda (object name method) (hash-add (object) (name) (method (object))));

(define mutable-struct (? lst (let ((data (map (? x (make-cell 0)) (lst)))) (? key (list-ref (data) (find-list (lst) (key)))))));

(define test-struct2 (mutable-struct (list x y)));

(set! (test-struct2 x) 10);

(set! (test-struct2 y) 20);

(= (get! (test-struct2 x)) 10);

(= (get! (test-struct2 y)) 20);

(define test-struct3 (add-method (test-struct2) sum (? self (+ (get! (self x)) (get! (self y))))));

(= (get! (test-struct3 x)) 10);

(= (get! (test-struct3 y)) 20);

(= (test-struct3 sum) 30);

(set! (test-struct3 y) 10);

(= (test-struct3 sum) 20);

(set! (test-struct2 y) 5);

(= (test-struct3 sum) 15);