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