# 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)
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 0));
[hear] (intro (unary 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 0));
[hear] (intro (unary 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 0));
[hear] (intro (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
       # MATH now show equality
[hear] (intro =);
[hear] (= (unary 0) (unary 0));
[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (= (unary 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
       # MATH now show other relational operators
[hear] (intro >);
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 0) (unary 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 0));
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 0));
[hear] (intro <);
[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 0) (unary 1 1 0));
[hear] (< (unary 0) (unary 1 1 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (< (unary 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 1 0) (unary 1 0));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (> (unary 1 0) (unary 0));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (> (unary 1 1 1 0) (unary 1 1 0));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 1 0));
       # MATH introduce the NOT logical operator
[hear] (intro not);
[hear] (= (unary 1 0) (unary 1 0));
[hear] (not (< (unary 1 0) (unary 1 0)));
[hear] (not (> (unary 1 0) (unary 1 0)));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (unary 0) (unary 0));
[hear] (not (< (unary 0) (unary 0)));
[hear] (not (> (unary 0) (unary 0)));
[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (not (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (unary 1 0) (unary 1 0));
[hear] (not (< (unary 1 0) (unary 1 0)));
[hear] (not (> (unary 1 0) (unary 1 0)));
[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 0) (unary 1 1 1 1 0)));
[hear] (< (unary 1 0) (unary 1 1 1 1 0));
[hear] (not (> (unary 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));
[hear] (not (> (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 0) (unary 1 1 1 0)));
[hear] (< (unary 1 0) (unary 1 1 1 0));
[hear] (not (> (unary 1 0) (unary 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0));
[hear] (not (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 0) (unary 1 0)));
[hear] (> (unary 1 1 1 0) (unary 1 0));
[hear] (not (< (unary 1 1 1 0) (unary 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0));
[hear] (not (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
       # MATH introduce the AND logical operator
[hear] (intro and);
[hear] (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (and (= (unary 1 0) (unary 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 0) (unary 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 0)));
[hear] (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (= (unary 1 1 0) (unary 1 1 0))
            (< (unary 0) (unary 1 1 0)));
[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 1 1 0))
            (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (and (< (unary 1 0) (unary 1 1 0))
            (= (unary 1 1 0) (unary 1 1 0)));
[hear] (not (and (> (unary 1 1 1 1 0) (unary 1 1 1 0)) (> (unary 0) (unary 1 0))));
[hear] (not
        (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (> (unary 1 0) (unary 1 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (= (unary 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (and (= (unary 1 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
[hear] (not (and (> (unary 1 1 0) (unary 1 1 1 0)) (< (unary 1 0) (unary 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 1 1 0) (unary 1 0))
             (> (unary 1 1 1 0) (unary 1 1 0))));
[hear] (not
        (and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (> (unary 1 1 0) (unary 0))));
[hear] (not
        (and (= (unary 1 0) (unary 0))
             (> (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not
        (and (> (unary 1 1 1 0) (unary 1 1 1 1 1 0))
             (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not
        (and (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not (and (= (unary 1 1 1 1 0) (unary 0)) (> (unary 0) (unary 1 1 1 0))));
[hear] (not
        (and (= (unary 1 1 1 1 1 0) (unary 0))
             (> (unary 1 1 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 0) (unary 1 1 1 1 0)) (> (unary 1 1 0) (unary 1 1 0))));
[hear] (not (and (= (unary 0) (unary 1 1 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 0))));
[hear] (not (and (< (unary 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 0))));
[hear] (and (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (not
        (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
             (> (unary 1 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 1 0) (unary 0)) (< (unary 1 1 1 0) (unary 1 1 0))));
[hear] (and (< (unary 0) (unary 1 1 0))
            (> (unary 1 0) (unary 0)));
[hear] (not (and (= (unary 1 1 1 1 0) (unary 1 0)) (> (unary 0) (unary 1 1 1 0))));
[hear] (not
        (and (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 0))));
[hear] (not (and (= (unary 1 1 0) (unary 1 0)) (> (unary 1 0) (unary 1 1 1 0))));
[hear] (not (and (> (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 1 0))));
[hear] (not
        (and (> (unary 1 1 0) (unary 1 1 0))
             (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
       # MATH introduce the OR logical operator
[hear] (intro or);
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (or (< (unary 1 0) (unary 1 1 0))
           (> (unary 1 1 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 0) (unary 1 0))
           (< (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (< (unary 1 0) (unary 1 1 1 1 0))
           (> (unary 1 0) (unary 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 0) (unary 0))
           (= (unary 1 1 0) (unary 1 1 0)));
[hear] (or (< (unary 0) (unary 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (< (unary 0) (unary 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 1 0)));
[hear] (or (> (unary 1 1 1 0) (unary 1 0))
           (= (unary 0) (unary 1 1 0)));
[hear] (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (= (unary 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 0) (unary 1 1 1 1 0))
           (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 0))
           (> (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (or (> (unary 0) (unary 1 1 1 1 0))
           (= (unary 0) (unary 0)));
[hear] (or (= (unary 1 1 0) (unary 0))
           (< (unary 0) (unary 1 1 0)));
[hear] (or (< (unary 1 1 1 1 1 1 0) (unary 1 1 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 1 1 0) (unary 0))
           (= (unary 0) (unary 0)));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
           (< (unary 1 0) (unary 1 1 0)));
[hear] (not
        (or (> (unary 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (or (> (unary 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (or (> (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 0))));
[hear] (not
        (or (> (unary 1 1 1 0) (unary 1 1 1 0))
            (< (unary 1 1 1 1 1 0) (unary 1 1 1 0))));
[hear] (not (or (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)) (> (unary 0) (unary 0))));
[hear] (not (or (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 0))));
[hear] (not (or (> (unary 1 0) (unary 1 1 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
[hear] (or (> (unary 0) (unary 1 1 1 0))
           (> (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));
[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 0) (unary 1 1 0)));
[hear] (not
        (or (< (unary 1 1 1 1 1 0) (unary 1 1 1 0))
            (< (unary 1 1 0) (unary 1 0))));
[hear] (or (> (unary 1 1 1 1 0) (unary 1 0))
           (> (unary 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (not (or (> (unary 0) (unary 0)) (= (unary 1 1 0) (unary 1 1 1 0))));
[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 0))
           (< (unary 1 1 1 0) (unary 1 0)));
       # MATH use equality for truth values
[hear] (= (> (unary 1 1 1 1 0) (unary 1 1 0))
          (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (= (unary 1 1 0) (unary 1 1 0))
          (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0)));
[hear] (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
          (> (unary 1 1 1 0) (unary 1 0)));
[hear] (= (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))
          (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 0) (unary 1 1 0)) (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 0)) (= (unary 1 0) (unary 0)));
[hear] (= (> (unary 0) (unary 1 0)) (< (unary 1 1 1 1 0) (unary 1 0)));
[hear] (= (> (unary 1 0) (unary 1 1 1 1 1 0)) (> (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (< (unary 1 0) (unary 0)));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 0) (unary 1 1 1 1 0)));
[hear] (not
        (= (= (unary 1 0) (unary 0)) (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))));
[hear] (not (= (= (unary 1 1 1 1 1 0) (unary 1 1 0)) (= (unary 0) (unary 0))));
[hear] (not
        (= (< (unary 1 1 1 1 1 0) (unary 1 1 0))
           (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))));
[hear] (not (= (= (unary 0) (unary 1 0)) (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
           (= (unary 1 1 1 1 0) (unary 1 0))));
[hear] (not
        (= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
           (> (unary 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not (= (< (unary 0) (unary 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 0))));
[hear] (not
        (= (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 0) (unary 0))));
[hear] (not
        (= (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 1 1 0) (unary 0))));
[hear] (intro true);
[hear] (intro false);
[hear] (= (true) (= (unary 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (true) (= (unary 0) (unary 0)));
[hear] (= (true) (> (unary 1 1 1 1 1 0) (unary 1 1 0)));
[hear] (= (true) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (true) (> (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));
[hear] (= (< (unary 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (= (unary 1 1 1 0) (unary 1 1 1 0)) (true));
[hear] (= (< (unary 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (true));
[hear] (= (false) (> (unary 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (false) (= (unary 1 1 0) (unary 1 1 1 1 0)));
[hear] (= (false) (< (unary 1 1 0) (unary 0)));
[hear] (= (false) (> (unary 1 1 1 0) (unary 1 1 1 1 1 1 0)));
[hear] (= (false) (< (unary 1 1 1 1 0) (unary 1 1 1 0)));
[hear] (= (> (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
[hear] (= (= (unary 1 1 0) (unary 1 0)) (false));
[hear] (= (= (unary 1 1 0) (unary 1 1 1 1 1 0)) (false));
[hear] (= (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)) (false));
[hear] (= (< (unary 1 1 1 0) (unary 1 0)) (false));
[hear] (= (true) (true));
[hear] (= (false) (false));
[hear] (not (= (true) (false)));
[hear] (not (= (false) (true)));
       # MATH introduce addition
[hear] (intro +);
[hear] (= (+ (unary 1 1 1 0) (unary 1 1 1 1 0)) (unary 1 1 1 1 1 1 1 0));
[hear] (= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (+ (unary 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 0) (unary 0)) (unary 0));
[hear] (= (+ (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 1 0) (unary 0)) (unary 1 0));
[hear] (= (+ (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 0));
[hear] (= (+ (unary 0) (unary 0)) (unary 0));
       # MATH introduce subtraction
[hear] (intro -);
[hear] (= (- (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 0));
[hear] (= (- (unary 1 0) (unary 1 0)) (unary 0));
[hear] (= (- (unary 0) (unary 0)) (unary 0));
[hear] (= (- (unary 1 1 0) (unary 0)) (unary 1 1 0));
[hear] (= (- (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (- (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (unary 0));
[hear] (= (- (unary 1 1 1 0) (unary 0)) (unary 1 1 1 0));
       # MATH introduce multiplication
[hear] (intro *);
[hear] (= (* (unary 0) (unary 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 1 0)) (unary 0));
[hear] (= (* (unary 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 0) (unary 1 0)) (unary 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 1 0) (unary 1 0)) (unary 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 0));
[hear] (= (* (unary 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 0)) (unary 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 0)) (unary 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 0)) (unary 1 1 1 0));
[hear] (= (* (unary 1 1 1 0) (unary 1 1 1 0)) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (* (unary 1 0) (unary 1 1 0)) (unary 1 1 0));
[hear] (= (* (unary 0) (unary 1 0)) (unary 0));
[hear] (= (* (unary 0) (unary 1 1 1 0)) (unary 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.
[hear] (= (unary 0) (.));
[hear] (= (unary 1 0) (:));
[hear] (= (unary 1 1 0) (:.));
[hear] (= (unary 1 1 1 0) (::));
[hear] (= (unary 1 1 1 1 0) (:..));
[hear] (= (unary 1 1 1 1 1 0) (:.:));
[hear] (= (unary 1 1 1 1 1 1 0) (::.));
[hear] (= (unary 1 1 1 1 1 1 1 0) (:::));
[hear] (= (unary 1 1 1 1 1 1 1 1 0) (:...));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) (:..:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 0) (:.:.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 0) (:.::));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 0) (::..));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::.:));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (:::.));
[hear] (= (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (::::));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::) (unary 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (::::) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:..:) (unary 1 1 1 1 1 1 1 1 1 0));
[hear] (= (::.) (unary 1 1 1 1 1 1 0));
[hear] (= (:::) (unary 1 1 1 1 1 1 1 0));
[hear] (= (:..) (unary 1 1 1 1 0));
[hear] (= (::.:) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:::) (unary 1 1 1 1 1 1 1 0));
[hear] (= (:::.) (unary 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0));
[hear] (= (:.:) (unary 1 1 1 1 1 0));
[hear] (= (+ (:.) (:.:)) (:::));
[hear] (= (+ (::.) (::.))
          (::..));
[hear] (= (+ (::..) (::))
          (::::));
[hear] (= (+ (:.) (::)) (:.:));
[hear] (= (+ (:...) (:...))
          (:....));
[hear] (= (+ (::.:) (:::.))
          (::.::));
[hear] (= (+ (:::) (:.:.))
          (:...:));
[hear] (= (+ (::..) (:.::))
          (:.:::));
[hear] (= (* (::.:) (:..:))
          (:::.:.:));
[hear] (= (* (::..) (::.:))
          (:..:::..));
[hear] (= (* (::..) (:.:.))
          (::::...));
[hear] (= (* (::..) (::::))
          (:.::.:..));
[hear] (= (* (:) (::.)) (::.));
[hear] (= (* (::.) (:.:.))
          (::::..));
[hear] (= (* (:..) (:::.))
          (:::...));
[hear] (= (* (::::) (:..:))
          (:....:::));
       # MATH demonstrate idea of leaving gaps in an expression
       # and then filling them in afterwards
       # the examples given leave a lot to be desired!
[hear] ((? x (= (+ 2 (x)) 13)) 11);
[hear] ((? x (= (+ 11 (x)) 21)) 10);
[hear] ((? x (= (+ 9 (x)) 11)) 2);
[hear] ((? x (= (+ 12 (x)) 18)) 6);
[hear] ((? x (= (+ 6 (x)) 20)) 14);
[hear] ((? x (= (+ 8 (x)) 10)) 2);
[hear] ((? x (= (+ 11 (x)) 18)) 7);
[hear] ((? x (= (+ 8 (x)) 13)) 5);
[hear] (((? x (? y (= (* (x) (y)) 12))) 6) 2);
[hear] (((? x (? y (= (* (x) (y)) 84))) 12) 7);
[hear] (((? x (? y (= (* (x) (y)) 45))) 15) 3);
[hear] (((? x (? y (= (* (x) (y)) 18))) 3) 6);
[hear] (((? x (? y (= (* (x) (y)) 90))) 15) 6);
[hear] (((? x (? y (= (* (x) (y)) 36))) 3) 12);
[hear] (((? x (? y (= (* (x) (y)) 30))) 2) 15);
[hear] (((? x (? y (= (* (x) (y)) 32))) 8) 4);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 11) 1)
        11);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 121) 11)
        11);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 156) 12)
        13);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 16) 2)
        8);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 0) 4) 0);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 108) 12)
        9);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 80) 10)
        8);
[hear] ((((? z (? x (? y (= (* (x) (y)) (z))))) 8) 8) 1);
       # MATH show some simple function calls
       # and show a way to remember functions across statements
[hear] (= ((? square (square 1)) (? x (* (x) (x)))) 1);
[hear] (= ((? square (square 2)) (? x (* (x) (x)))) 4);
[hear] (= ((? square (square 0)) (? x (* (x) (x)))) 0);
[hear] (= ((? square (square 8)) (? x (* (x) (x)))) 64);
[hear] (= ((? square (square 5)) (? x (* (x) (x)))) 25);
[hear] (= ((? square (square 1)) (? x (* (x) (x)))) 1);
[hear] (= ((? square (square 8)) (? x (* (x) (x)))) 64);
[hear] (= ((? square (square 3)) (? x (* (x) (x)))) 9);
[hear] (define square (? x (* (x) (x))));
[hear] (= (square 0) 0);
[hear] (= (square 7) 49);
[hear] (= (square 5) 25);
[hear] (= (square 6) 36);
[hear] (define plusone (? x (+ (x) 1)));
[hear] (= (plusone 7) 8);
[hear] (= (plusone 3) 4);
[hear] (= (plusone 6) 7);
[hear] (= (plusone 9) 10);
       # MATH show mechanisms for branching
[hear] (intro if);
[hear] (= (if (true) 8 4) 8);
[hear] (= (if (true) 0 0) 0);
[hear] (= (if (true) 2 7) 2);
[hear] (= (if (true) 9 7) 9);
[hear] (= (if (true) 0 3) 0);
[hear] (= (if (true) 0 4) 0);
[hear] (= (if (true) 4 9) 4);
[hear] (= (if (false) 7 9) 9);
[hear] (= (if (false) 0 8) 8);
[hear] (= (if (false) 6 3) 3);
[hear] (= (if (false) 2 8) 8);
[hear] (= (if (false) 0 3) 3);
[hear] (= (if (true) 8 0) 8);
[hear] (= (if (false) 2 1) 1);
[hear] (= (if (true) 4 7) 4);
[hear] (= (if (false) 2 6) 6);
       # MATH some pure lambda calculus definitions - optional
       # these definitions are not quite what we want
       # since thinking of everything as a function requires headscratching
       # it would be better to use these as a parallel means of evaluation
       # ... for expressions
[hear] (define pure-if (? x (? y (? z (x (y) (z))))));
[hear] (define pure-true (? y (? z (y))));
[hear] (define pure-false (? y (? z (z))));
[hear] (define pure-cons
         (? x (? y (? z (pure-if (z) (x) (y))))));
[hear] (define pure-car (? x (x (pure-true))));
[hear] (define pure-cdr (? x (x (pure-false))));
[hear] (define zero (? f (? x (x))));
[hear] (define one (? f (? x (f (x)))));
[hear] (define two (? f (? x (f (f (x))))));
[hear] (define succ (? n (? f (? x (f ((n (f)) (x)))))));
[hear] (define add (? a (? b ((a (succ)) (b)))));
[hear] (define mult (? a (? b ((a (add (b))) (zero)))));
[hear] (define pred
         (? n
           (pure-cdr
             ((n (? p
                   (pure-cons (succ (pure-car (p))) (pure-car (p)))))
              (pure-cons (zero) (zero))))));
[hear] (define is-zero
         (? n ((n (? dummy (pure-false)) (pure-true)))));
[hear] (define fixed-point
         (? f ((? x (f (x (x)))) (? x (f (x (x)))))));
       # .. but for rest of message will assume that define does fixed-point for us
       # now build a link between numbers and church number functions
[hear] (define unchurch (? c (c (? x (+ (x) 1)) 0)));
[hear] (= 0 (unchurch (zero)));
[hear] (= 1 (unchurch (one)));
[hear] (= 2 (unchurch (two)));
[hear] (define church
         (? x
           (if (= 0 (x)) (zero) (succ (church (- (x) 1))))));
       # MATH show an example of recursive evaluation
       # skipping over a lot of definitions and desugarings
[hear] (define easy-factorial
         (? f
           (? x (if (> (x) 0) (* (x) (f (f) (- (x) 1))) 1))));
[hear] (define factorial
         (? x
           (if (> (x) 0) (* (x) (factorial (- (x) 1))) 1)));
[hear] (= (easy-factorial (easy-factorial) 0) 1);
[hear] (= (easy-factorial (easy-factorial) 1) 1);
[hear] (= (easy-factorial (easy-factorial) 2) 2);
[hear] (= (easy-factorial (easy-factorial) 3) 6);
[hear] (= (easy-factorial (easy-factorial) 4) 24);
[hear] (= (easy-factorial (easy-factorial) 5) 120);
[hear] (= (factorial 0) 1);
[hear] (= (factorial 1) 1);
[hear] (= (factorial 2) 2);
[hear] (= (factorial 3) 6);
[hear] (= (factorial 4) 24);
[hear] (= (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
[hear] (intro forall);
[hear] (< 5 (+ 5 1));
[hear] (< 4 (+ 4 1));
[hear] (< 3 (+ 3 1));
[hear] (< 2 (+ 2 1));
[hear] (< 1 (+ 1 1));
[hear] (< 0 (+ 0 1));
[hear] (forall (? x (< (x) (+ (x) 1))));
[hear] (< 5 (* 5 2));
[hear] (< 4 (* 4 2));
[hear] (< 3 (* 3 2));
[hear] (< 2 (* 2 2));
[hear] (< 1 (* 1 2));
[hear] (not (< 0 (* 0 2)));
[hear] (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
[hear] (not (= 5 (* 2 2)));
[hear] (= 4 (* 2 2));
[hear] (not (= 3 (* 2 2)));
[hear] (not (= 2 (* 2 2)));
[hear] (not (= 1 (* 2 2)));
[hear] (not (= 0 (* 2 2)));
[hear] (intro exists);
[hear] (exists (? x (= (x) (* 2 2))));
[hear] (not (= 5 (+ 5 2)));
[hear] (not (= 4 (+ 4 2)));
[hear] (not (= 3 (+ 3 2)));
[hear] (not (= 2 (+ 2 2)));
[hear] (not (= 1 (+ 1 2)));
[hear] (not (= 0 (+ 0 2)));
[hear] (not (exists (? x (= (x) (+ (x) 2)))));
       # MATH introduce logical implication
[hear] (intro =>);
[hear] (define => (? x (? y (not (and (x) (not (y)))))));
[hear] (=> (true) (true));
[hear] (not (=> (true) (false)));
[hear] (=> (false) (true));
[hear] (=> (false) (false));
[hear] (forall
         (? x
           (forall
             (? y (=> (=> (x) (y)) (=> (not (y)) (not (x))))))));
       # MATH illustrate lists and some list operators
       # to make list describable as a function, need to preceed lists
       # ... with an argument count
       # lists will be written as [1 2 1] = (list 3 1 2 1) after this lesson
       # it would be nice to include such syntactic sugar in the message but that
       # ... is a fight for another day
       # finally, lists keep an explicit record of their length
       # this is to avoid the need for using a special 'nil' symbol
       # ... which cannot itself be placed in the list.
       #
       # MISSING - intro to cons, car, cdr
       # used to be pure-cons pure-car pure-cdr but changed for better interface to scheme
       # also should introduce number? check function
       #
[hear] (define list-helper
         (? n
           (? ret
             (if (> (n) 1)
               (? x
                 (list-helper
                   (- (n) 1)
                   (? y (? z (ret (+ 1 (y)) (cons (x) (z)))))))
               (? x (ret 1 (x)))))));
[hear] (define list
         (? n
           (if (= (n) 0)
             (cons 0 0)
             (list-helper (n) (? y (? z (cons (y) (z))))))));
[hear] (define head
         (? lst
           (if (= (car (lst)) 0)
             (undefined)
             (if (= (car (lst)) 1)
               (cdr (lst))
               (car (cdr (lst)))))));
[hear] (define tail
         (? lst
           (if (= (car (lst)) 0)
             (undefined)
             (if (= (car (lst)) 1)
               (cons 0 0)
               (cons (- (car (lst)) 1) (cdr (cdr (lst))))))));
[hear] (define list-length (? lst (car (lst))));
[hear] (define list-ref
         (? lst
           (? n
             (if (= (list-ref (lst)) 0)
               (undefined)
               (if (= (n) 0)
                 (head (lst))
                 (list-ref (tail (lst)) (- (n) 1)))))));
[hear] (define prepend
         (? x
           (? lst
             (if (= (list-length (lst)) 0)
               (cons 1 (x))
               (cons (+ (list-length (lst)) 1)
                     (cons (x) (cdr (lst))))))));
[hear] (define list=
         (? x
           (? y
             (if (= (list-length (x)) (list-length (y)))
               (if (> (list-length (x)) 0)
                 (and (= (head (x)) (head (y)))
                      (list= (tail (x)) (tail (y))))
                 (true))
               (false)))));
[hear] (= (list-length ((list 1) 3)) 1);
[hear] (= (list-length ((list 8) 9 8 0 4 7 3 6 5)) 8);
[hear] (= (list-length ((list 5) 8 6 4 2 5)) 5);
[hear] (= (list-length ((list 9) 5 8 4 3 9 6 1 7 2)) 9);
[hear] (= (list-length ((list 7) 2 4 9 6 5 0 8)) 7);
[hear] (= (head ((list 8) 12 1 4 13 17 3 10 4)) 12);
[hear] (list= (tail ((list 8) 12 1 4 13 17 3 10 4))
              ((list 7) 1 4 13 17 3 10 4));
[hear] (= (head ((list 9) 6 13 15 4 12 1 0 5 6)) 6);
[hear] (list= (tail ((list 9) 6 13 15 4 12 1 0 5 6))
              ((list 8) 13 15 4 12 1 0 5 6));
[hear] (= (head ((list 6) 19 4 12 2 15 12)) 19);
[hear] (list= (tail ((list 6) 19 4 12 2 15 12))
              ((list 5) 4 12 2 15 12));
[hear] (= (head ((list 10) 3 4 4 2 15 3 17 6 11 3)) 3);
[hear] (list= (tail ((list 10) 3 4 4 2 15 3 17 6 11 3))
              ((list 9) 4 4 2 15 3 17 6 11 3));
[hear] (= (head ((list 2) 15 2)) 15);
[hear] (list= (tail ((list 2) 15 2)) ((list 1) 2));
[hear] (= (head ((list 10) 15 12 17 11 0 12 14 8 17 5))
          15);
[hear] (list= (tail ((list 10) 15 12 17 11 0 12 14 8 17 5))
              ((list 9) 12 17 11 0 12 14 8 17 5));
[hear] (= (head ((list 5) 11 1 10 7 9)) 11);
[hear] (list= (tail ((list 5) 11 1 10 7 9))
              ((list 4) 1 10 7 9));
[hear] (= (head ((list 3) 19 10 14)) 19);
[hear] (list= (tail ((list 3) 19 10 14))
              ((list 2) 10 14));
[hear] (= (head ((list 5) 4 2 7 12 18)) 4);
[hear] (list= (tail ((list 5) 4 2 7 12 18))
              ((list 4) 2 7 12 18));
[hear] (= (head ((list 5) 13 1 0 5 10)) 13);
[hear] (list= (tail ((list 5) 13 1 0 5 10))
              ((list 4) 1 0 5 10));
[hear] (= (list-ref ((list 1) 9) 0) 9);
[hear] (= (list-ref ((list 10) 4 4 14 0 14 4 17 7 3 17) 0)
          4);
[hear] (= (list-ref ((list 8) 10 13 6 14 3 13 9 18) 0)
          10);
[hear] (= (list-ref ((list 4) 3 1 0 2) 2) 0);
[hear] (= (list-ref ((list 5) 13 7 18 13 12) 1) 7);
[hear] (= (list-ref ((list 3) 19 16 9) 2) 9);
[hear] (= (list-ref ((list 5) 12 14 5 14 4) 4) 4);
[hear] (= (list-ref ((list 2) 10 17) 1) 17);
[hear] (= (list-ref ((list 4) 1 12 10 18) 3) 18);
[hear] (= (list-ref ((list 8) 17 7 2 4 19 15 4 9) 0) 17);
[hear] (list= ((list 0)) ((list 0)));
[hear] (list= ((list 1) 7) ((list 1) 7));
[hear] (list= ((list 2) 1 19) ((list 2) 1 19));
[hear] (list= ((list 3) 18 1 18) ((list 3) 18 1 18));
[hear] (list= ((list 4) 13 15 10 6)
              ((list 4) 13 15 10 6));
       # this next batch of examples are a bit misleading, should streamline
[hear] (not (list= ((list 0)) ((list 1) 0)));
[hear] (not (list= ((list 0)) ((list 1) 6)));
[hear] (not (list= ((list 1) 9) ((list 2) 6 9)));
[hear] (not (list= ((list 1) 9) ((list 2) 9 7)));
[hear] (not (list= ((list 2) 1 6) ((list 3) 2 1 6)));
[hear] (not (list= ((list 2) 1 6) ((list 3) 1 6 0)));
[hear] (not (list= ((list 3) 10 9 12) ((list 4) 5 10 9 12)));
[hear] (not (list= ((list 3) 10 9 12) ((list 4) 10 9 12 3)));
[hear] (not (list= ((list 4) 17 9 1 0) ((list 5) 4 17 9 1 0)));
[hear] (not (list= ((list 4) 17 9 1 0) ((list 5) 17 9 1 0 4)));
       # some helpful functions
[hear] (list= (prepend 12 ((list 0))) ((list 1) 12));
[hear] (list= (prepend 0 ((list 1) 14)) ((list 2) 0 14));
[hear] (list= (prepend 10 ((list 2) 8 19))
              ((list 3) 10 8 19));
[hear] (list= (prepend 12 ((list 3) 10 2 1))
              ((list 4) 12 10 2 1));
[hear] (list= (prepend 14 ((list 4) 6 16 14 5))
              ((list 5) 14 6 16 14 5));
[hear] (list= (prepend 4 ((list 5) 15 2 3 11 8))
              ((list 6) 4 15 2 3 11 8));
[hear] (list= (prepend 12 ((list 6) 9 2 19 7 2 0))
              ((list 7) 12 9 2 19 7 2 0));
[hear] (list= (prepend 11 ((list 7) 17 17 2 4 16 5 14))
              ((list 8) 11 17 17 2 4 16 5 14));
[hear] (define pair (? x (? y ((list 2) (x) (y)))));
[hear] (define first (? lst (head (lst))));
[hear] (define second (? lst (head (tail (lst)))));
[hear] (list= (pair 3 6) ((list 2) 3 6));
[hear] (= (first (pair 3 6)) 3);
[hear] (= (second (pair 3 6)) 6);
[hear] (list= (pair 8 8) ((list 2) 8 8));
[hear] (= (first (pair 8 8)) 8);
[hear] (= (second (pair 8 8)) 8);
[hear] (list= (pair 9 2) ((list 2) 9 2));
[hear] (= (first (pair 9 2)) 9);
[hear] (= (second (pair 9 2)) 2);
[hear] (define list-find-helper
         (? lst
           (? key
             (? fail
               (? idx
                 (if (= (list-length (lst)) 0)
                   (fail 0)
                   (if (= (head (lst)) (key))
                     (idx)
                     (list-find-helper
                       (tail (lst))
                       (key)
                       (fail)
                       (+ (idx) 1)))))))));
[hear] (define list-find
         (? lst
           (? key
             (? fail (list-find-helper (lst) (key) (fail) 0)))));
[hear] (define example-fail (? x 100));
[hear] (= (list-find ((list 1) 15) 15 (example-fail)) 0);
[hear] (= (list-find ((list 2) 9 6) 9 (example-fail)) 0);
[hear] (= (list-find
            ((list 4) 19 7 14 6)
            19
            (example-fail))
          0);
[hear] (= (list-find
            ((list 8) 10 0 6 9 5 10 2 2)
            5
            (example-fail))
          4);
[hear] (= (list-find ((list 4) 14 5 7 6) 6 (example-fail))
          3);
[hear] (= (list-find ((list 1) 2) 2 (example-fail)) 0);
[hear] (= (list-find
            ((list 7) 19 7 12 4 18 8 7)
            4
            (example-fail))
          3);
[hear] (= (list-find ((list 1) 2) 2 (example-fail)) 0);
[hear] (= (list-find
            ((list 4) 5 19 13 13)
            19
            (example-fail))
          1);
[hear] (= (list-find
            ((list 10) 17 14 17 8 6 1 2 12 10 4)
            1
            (example-fail))
          5);
[hear] (= (list-find
            ((list 4) 15 13 6 17)
            14
            (example-fail))
          100);
[hear] (= (list-find
            ((list 6) 16 13 10 3 0 19)
            2
            (example-fail))
          100);
[hear] (= (list-find
            ((list 8) 13 19 4 17 11 9 2 3)
            15
            (example-fail))
          100);
       # HACK describe changes to the implicit interpreter to allow new special forms
[hear] (define base-translate (translate));
[hear] (define translate