#   Author: Paul Fitzpatrick, paulfitz@ai.mit.edu
       #   Copyright (c) 2004 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)
       # Here we count up, then count down, then go through primes, etc.
       # There is a bunch of syntax around the numbers, but that
       # can just be treated as noise at this point - it doesn't matter.
       # The key is to set up the structure of ';'-terminated sequences,
       # and to introduce one simple representation of numbers.
       # Symbols like intro and unary are encoded as binary numbers,
       # which again can be treated as noise for now.
[
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 introduce equality for unary numbers
       # The intro operator does nothing essential, and could be
       # omitted - it just tags the first use of a new operator.
       # The = operator is introduced alongside a duplication of
       # unary numbers. The meaning will not quite by nailed down
       # until we see other relational operators.
[
hear] (intro =);

[hear] (= (unary 1 1 1 0) (unary 1 1 1 0));

[hear] (= (unary 1 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 1 0));

[hear] (= (unary 1 1 1 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 1 0));

[hear] (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0));


       # MATH now introduce other relational operators
       # After this lesson, it should be clear what contexts
       # < > and = are appropriate in.
[
hear] (intro >);

[hear] (> (unary 1 1 1 1 0) (unary 0));

[hear] (> (unary 1 1 1 1 0) (unary 1 0));

[hear] (> (unary 1 1 1 0) (unary 0));

[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 1 0));

[hear] (> (unary 1 1 0) (unary 0));

[hear] (> (unary 1 0) (unary 0));

[hear] (> (unary 1 1 0) (unary 0));

[hear] (> (unary 1 1 0) (unary 0));

[hear] (> (unary 1 1 1 0) (unary 0));

[hear] (> (unary 1 0) (unary 0));

[hear] (> (unary 1 1 1 1 1 0) (unary 1 1 0));

[hear] (intro <);

[hear] (< (unary 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 0) (unary 1 1 1 0));

[hear] (< (unary 0) (unary 1 1 1 0));

[hear] (< (unary 1 0) (unary 1 1 1 0));

[hear] (< (unary 1 1 0) (unary 1 1 1 1 1 1 0));

[hear] (< (unary 0) (unary 1 0));

[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));

[hear] (< (unary 0) (unary 1 1 1 1 1 1 0));

[hear] (< (unary 1 0) (unary 1 1 1 1 0));

       # drive the lesson home
[hear] (= (unary 0) (unary 0));

[hear] (< (unary 0) (unary 1 0));

[hear] (< (unary 0) (unary 1 1 0));

[hear] (> (unary 1 0) (unary 0));

[hear] (= (unary 1 0) (unary 1 0));

[hear] (< (unary 1 0) (unary 1 1 0));

[hear] (> (unary 1 1 0) (unary 0));

[hear] (> (unary 1 1 0) (unary 1 0));

[hear] (= (unary 1 1 0) (unary 1 1 0));

[hear] (< (unary 1 0) (unary 1 1 1 1 1 0));

[hear] (< (unary 1 0) (unary 1 1 1 1 0));

[hear] (< (unary 0) (unary 1 0));

[hear] (> (unary 1 1 1 1 0) (unary 0));

[hear] (< (unary 1 1 0) (unary 1 1 1 0));

[hear] (> (unary 1 1 1 1 0) (unary 1 0));

[hear] (< (unary 0) (unary 1 1 1 1 1 0));

[hear] (> (unary 1 0) (unary 0));

[hear] (< (unary 1 0) (unary 1 1 1 1 0));

[hear] (> (unary 1 1 0) (unary 0));

[hear] (< (unary 1 0) (unary 1 1 0));


       # SYNTAX introduce tail notation
       # I've recently added the / symbol to reduce the need
       # for unnecessary levels of nesting and parentheses.
       # This might be a little early to talk about it, since it
       # is most valuable for complex expressions.
[
hear] (= (unary 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 0) / unary 1 1 0);

[hear] (< (unary 1 1 0) (unary 1 1 1 1 0));

[hear] (< (unary 1 1 0) / unary 1 1 1 1 0);

[hear] (> (unary 1 1 0) (unary 1 0));

[hear] (> (unary 1 1 0) / unary 1 0);


       # MATH introduce the NOT logical operator
[
hear] (intro not);

[hear] (= (unary 1 1 1 1 0) (unary 1 1 1 1 0));

[hear] (not / < (unary 1 1 1 1 0) (unary 1 1 1 1 0));

[hear] (not / > (unary 1 1 1 1 0) (unary 1 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] (= (unary 0) (unary 0));

[hear] (not / < (unary 0) (unary 0));

[hear] (not / > (unary 0) (unary 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] (= (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 0) (unary 1 0));

[hear] (< (unary 0) (unary 1 0));

[hear] (not / > (unary 0) (unary 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 0) (unary 1 1 1 1 0));

[hear] (< (unary 1 1 1 0) (unary 1 1 1 1 0));

[hear] (not / > (unary 1 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 0) (unary 1 1 1 0));

[hear] (< (unary 0) (unary 1 1 1 0));

[hear] (not / > (unary 0) (unary 1 1 1 0));

[hear] (not / = (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0));

[hear] (> (unary 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 1 1 0));

[hear] (not / = (unary 1 0) (unary 0));

[hear] (> (unary 1 0) (unary 0));

[hear] (not / < (unary 1 0) (unary 0));

[hear] (not / = (unary 1 1 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 0));

[hear] (not / < (unary 1 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] (> (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 0) (unary 1 1 0));

[hear] (> (unary 1 1 1 1 0) (unary 1 1 0));

[hear] (not / < (unary 1 1 1 1 0) (unary 1 1 0));

[hear] (not / = (unary 1 1 1 1 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));

[hear] (not / < (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));


       # MATH introduce the AND logical operator
[
hear] (intro and);

[hear] (and (> (unary 1 1 1 0) (unary 1 0)) (< (unary 1 0) (unary 1 1 1 0)));

[hear] (and (= (unary 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 0)));

[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0)) (= (unary 1 0) (unary 1 0)));

[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 0))
             (> (unary 1 1 1 1 0) (unary 1 1 1 0)));

[hear] (and (> (unary 1 1 1 1 1 0) (unary 1 1 1 0)) (> (unary 1 1 1 0) (unary 1 0)));

[hear] (and (> (unary 1 1 1 0) (unary 1 0)) (< (unary 1 1 0) (unary 1 1 1 1 0)));

[hear] (and (> (unary 1 1 1 1 0) (unary 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] (and (< (unary 1 1 0) (unary 1 1 1 1 1 0)) (< (unary 0) (unary 1 1 0)));

[hear] (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 0) (unary 0)));

[hear] (not /
         and (< (unary 1 1 1 1 1 0) (unary 1 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 0))
             (= (unary 1 1 1 0) (unary 1 1 0)));

[hear] (not /
         and (= (unary 1 1 1 0) (unary 1 1 1 0))
             (> (unary 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (not /
         and (< (unary 1 1 0) (unary 1 1 1 1 0))
             (> (unary 1 1 1 0) (unary 1 1 1 0)));

[hear] (not /
         and (= (unary 1 1 1 1 0) (unary 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (not / and (= (unary 1 1 1 0) (unary 1 1 0)) (< (unary 0) (unary 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 0) (unary 1 1 1 1 1 1 1 0)));

[hear] (not / and (< (unary 1 1 1 1 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 0)));

[hear] (not / and (> (unary 0) (unary 1 1 0)) (< (unary 1 0) (unary 1 1 1 1 0)));

[hear] (not /
         and (> (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
             (> (unary 1 1 1 1 0) (unary 1 1 0)));

[hear] (not / and (< (unary 1 1 1 1 0) (unary 1 0)) (> (unary 1 0) (unary 1 1 0)));

[hear] (not /
         and (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (> (unary 0) (unary 1 1 0)));

[hear] (not /
         and (= (unary 1 1 1 1 1 0) (unary 1 0))
             (= (unary 1 1 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 0))
             (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (not /
               and (< (unary 1 1 0) (unary 0)) (= (unary 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (not /
               and (= (unary 0) (unary 1 0)) (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)));

[hear] (and (< (unary 0) (unary 1 1 1 0)) (= (unary 1 1 1 0) (unary 1 1 1 0)));

[hear] (not /
         and (> (unary 1 1 1 1 0) (unary 1 1 1 1 0))
             (< (unary 1 1 0) (unary 0)));

[hear] (not /
         and (= (unary 1 1 0) (unary 1 1 1 0))
             (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));

[hear] (and (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
             (< (unary 1 1 1 1 0) (unary 1 1 1 1 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 1 1 0)));

[hear] (not /
         and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
             (> (unary 1 1 1 0) (unary 1 0)));

[hear] (not /
         and (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0))
             (= (unary 1 1 0) (unary 1 1 1 0)));

[hear] (and (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 0))
             (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (not /
               and (= (unary 0) (unary 1 1 1 0)) (= (unary 1 1 1 1 1 0) (unary 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 0) (unary 1 0)));

[hear] (or (< (unary 1 1 0) (unary 1 1 1 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)) (= (unary 1 0) (unary 1 0)));

[hear] (or (> (unary 1 1 0) (unary 1 0)) (> (unary 1 1 1 1 0) (unary 1 1 0)));

[hear] (or (> (unary 1 1 1 0) (unary 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (or (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)) (< (unary 1 0) (unary 1 1 1 0)));

[hear] (or (< (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 1 1 1 0)));

[hear] (or (< (unary 0) (unary 1 0)) (= (unary 1 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (or (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 1 0))
            (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (= (unary 1 0) (unary 1 0)) (< (unary 0) (unary 1 0)));

[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 1 1 1 0)));

[hear] (or (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 0)) (= (unary 1 1 0) (unary 0)));

[hear] (or (< (unary 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (> (unary 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (> (unary 1 1 1 1 0) (unary 1 1 1 0))
            (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (= (unary 1 0) (unary 1 0)) (= (unary 1 1 1 0) (unary 1 1 0)));

[hear] (or (< (unary 1 0) (unary 0)) (= (unary 1 1 0) (unary 1 1 0)));

[hear] (or (< (unary 1 1 1 0) (unary 1 0)) (= (unary 0) (unary 0)));

[hear] (or (> (unary 1 1 0) (unary 1 1 1 1 1 0))
            (> (unary 1 1 1 1 0) (unary 1 1 0)));

[hear] (or (> (unary 1 1 1 0) (unary 1 1 1 1 1 0)) (= (unary 1 1 0) (unary 1 1 0)));

[hear] (or (> (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0))
            (= (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (not / or (= (unary 1 0) (unary 1 1 1 0)) (= (unary 1 0) (unary 0)));

[hear] (not / or (> (unary 1 0) (unary 1 1 0)) (> (unary 1 0) (unary 1 1 1 1 0)));

[hear] (not /
         or (= (unary 1 1 1 0) (unary 1 1 1 1 0))
            (> (unary 1 0) (unary 1 1 1 1 0)));

[hear] (not / or (> (unary 0) (unary 1 1 1 1 0)) (= (unary 1 0) (unary 0)));

[hear] (not /
         or (< (unary 1 1 1 1 0) (unary 1 0))
            (< (unary 1 1 1 1 1 1 0) (unary 1 1 0)));

[hear] (not /
         or (> (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
            (= (unary 1 0) (unary 1 1 1 0)));

[hear] (or (> (unary 1 0) (unary 0)) (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (> (unary 1 0) (unary 0)) (= (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (or (> (unary 0) (unary 1 1 0)) (= (unary 1 1 1 1 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 0) (unary 1 1 1 1 0)));

[hear] (not /
               or (= (unary 1 0) (unary 1 1 0)) (= (unary 1 1 0) (unary 1 1 1 1 0)));

[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 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 1 1 1 0) (unary 0)));

[hear] (or (< (unary 1 0) (unary 1 1 1 1 0)) (< (unary 1 1 1 0) (unary 0)));

[hear] (or (= (unary 1 1 1 0) (unary 1 1 1 0)) (> (unary 1 1 0) (unary 1 1 1 0)));


       # MATH use equality for truth values
[
hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 0))
           (< (unary 1 1 0) (unary 1 1 1 1 1 0)));

[hear] (= (= (unary 1 0) (unary 1 0)) (< (unary 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (= (= (unary 1 0) (unary 1 0)) (> (unary 1 1 1 0) (unary 1 1 0)));

[hear] (= (< (unary 1 1 0) (unary 1 1 1 0))
           (< (unary 1 1 1 1 1 0) (unary 1 1 1 1 1 1 1 1 0)));

[hear] (= (= (unary 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 1 0) (unary 0))
           (> (unary 1 1 1 1 1 1 0) (unary 1 1 1 1 1 1 0)));

[hear] (= (= (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (> (unary 0) (unary 1 1 1 1 1 0)));

[hear] (= (= (unary 1 1 1 0) (unary 1 0)) (= (unary 1 1 0) (unary 1 1 1 0)));

[hear] (= (> (unary 1 1 1 0) (unary 1 1 1 1 0)) (> (unary 0) (unary 1 1 0)));

[hear] (= (= (unary 1 1 1 1 1 0) (unary 0)) (> (unary 1 0) (unary 1 1 1 1 1 1 0)));

[hear] (not / = (> (unary 0) (unary 1 1 1 1 1 1 0)) (= (unary 1 0) (unary 1 0)));

[hear] (not / = (> (unary 1 1 0) (unary 1 1 1 0)) (= (unary 0) (unary 0)));

[hear] (not /
         = (= (unary 1 1 1 1 0) (unary 1 1 1 1 1 0))
           (< (unary 1 0) (unary 1 1 1 1 0)));

[hear] (not / = (< (unary 1 1 1 1 1 1 0) (unary 1 1 1 0)) (= (unary 0) (unary 0)));

[hear] (not / = (= (unary 0) (unary 1 1 1 1 0)) (= (unary 1 1 0) (unary 1 1 0)));

[hear] (not /
         = (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0))
           (> (unary 1 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (not /
         = (< (unary 1 1 1 1 0) (unary 1 1 1 1 1 1 0)) (> (unary 0) (unary 1 1 0)));

[hear] (not /
               = (= (unary 1 1 0) (unary 1 1 0)) (> (unary 1 1 1 0) (unary 1 1 1 0)));

[hear] (not / = (= (unary 1 0) (unary 1 0)) (< (unary 1 1 0) (unary 1 0)));

[hear] (not / = (= (unary 1 0) (unary 1 0)) (= (unary 1 0) (unary 1 1 1 1 0)));

[hear] (intro true);

[hear] (intro false);

[hear] (= (true) (< (unary 0) (unary 1 1 1 0)));

[hear] (= (true) (> (unary 1 1 1 1 0) (unary 1 0)));

[hear] (= (true) (> (unary 1 1 0) (unary 1 0)));

[hear] (= (true) (< (unary 1 0) (unary 1 1 1 1 0)));

[hear] (= (true) (< (unary 0) (unary 1 1 0)));

[hear] (= (= (unary 0) (unary 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 0)) (true));

[hear] (= (< (unary 0) (unary 1 0)) (true));

[hear] (= (> (unary 1 1 1 1 0) (unary 1 0)) (true));

[hear] (= (false) (> (unary 0) (unary 1 1 1 1 0)));

[hear] (= (false) (> (unary 1 1 1 0) (unary 1 1 1 1 0)));

[hear] (= (false) (< (unary 1 1 1 0) (unary 0)));

[hear] (= (false) (< (unary 1 1 1 1 1 0) (unary 1 1 1 0)));

[hear] (= (false) (> (unary 0) (unary 1 1 0)));

[hear] (= (< (unary 1 1 1 0) (unary 0)) (false));

[hear] (= (< (unary 1 1 1 1 1 1 0) (unary 1 0)) (false));

[hear] (= (> (unary 0) (unary 1 1 1 1 0)) (false));

[hear] (= (= (unary 1 0) (unary 1 1 1 0)) (false));

[hear] (= (> (unary 1 0) (unary 1 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 0) (unary 0));

[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 0) / + (unary 0) (unary 1 0));

[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 0) / + (unary 1 1 0) (unary 0));

[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 1 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 1 1 1 0) / + (unary 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 1 1 1 0) / + (unary 1 0) (unary 1 1 1 1 0));


       # MATH introduce subtraction
[
hear] (intro -);

[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 0) (unary 1 0));

[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 0) / - (unary 1 0) (unary 1 0));

[hear] (= (unary 1 1 0) / - (unary 1 1 1 1 1 0) (unary 1 1 1 0));

[hear] (= (unary 0) / - (unary 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 0) / - (unary 1 0) (unary 0));

[hear] (= (unary 1 1 1 1 0) / - (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 1 1 0) / - (unary 1 1 1 1 0) (unary 1 0));

[hear] (= (unary 1 1 1 1 0) / - (unary 1 1 1 1 1 1 1 1 0) (unary 1 1 1 1 0));

[hear] (= (unary 1 0) / - (unary 1 0) (unary 0));


       # MATH introduce multiplication
[
hear] (intro *);

[hear] (= (unary 0) / * (unary 0) (unary 0));

[hear] (= (unary 0) / * (unary 0) (unary 1 0));

[hear] (= (unary 0) / * (unary 0) (unary 1 1 0));

[hear] (= (unary 0) / * (unary 0) (unary 1 1 1 0));

[hear] (= (unary 0) / * (unary 1 0) (unary 0));

[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));

[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));

[hear] (= (unary 0) / * (unary 1 1 0) (unary 0));

[hear] (= (unary 1 1 0) / * (unary 1 1 0) (unary 1 0));

[hear] (= (unary 1 1 1 1 0) / * (unary 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 1 1 1 1 0) / * (unary 1 1 0) (unary 1 1 1 0));

[hear] (= (unary 0) / * (unary 1 1 1 0) (unary 0));

[hear] (= (unary 1 1 1 0) / * (unary 1 1 1 0) (unary 1 0));

[hear] (= (unary 1 1 1 1 1 1 0) / * (unary 1 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 1 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 0) / * (unary 1 1 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));

[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));

[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));

[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));

[hear] (= (unary 1 0) / * (unary 1 0) (unary 1 0));

[hear] (= (unary 1 1 1 0) / * (unary 1 0) (unary 1 1 1 0));

[hear] (= (unary 0) / * (unary 0) (unary 0));

[hear] (= (unary 1 1 0) / * (unary 1 0) (unary 1 1 0));

[hear] (= (unary 0) / * (unary 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 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 1 1 0));

[hear] (= (:.:) (unary 1 1 1 1 1 0));

[hear] (= (.) (unary 0));

[hear] (= (:.:.) (unary 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 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] (= (:.::) (unary 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 0));

[hear] (= (:.) (unary 1 1 0));

[hear] (= (:.::) (unary 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 / = 10 / + 7 / x) 3);

[hear] ((? x / = 5 / + 2 / x) 3);

[hear] ((? x / = 20 / + 7 / x) 13);

[hear] ((? x / = 24 / + 13 / x) 11);

[hear] ((? x / = 19 / + 10 / x) 9);

[hear] ((? x / = 8 / + 0 / x) 8);

[hear] ((? x / = 17 / + 8 / x) 9);

[hear] ((? x / = 13 / + 7 / x) 6);

[hear] (((? x / ? y / = 1 / * (x) (y)) 1) 1);

[hear] (((? x / ? y / = 11 / * (x) (y)) 11) 1);

[hear] (((? x / ? y / = 22 / * (x) (y)) 2) 11);

[hear] (((? x / ? y / = 120 / * (x) (y)) 15) 8);

[hear] (((? x / ? y / = 50 / * (x) (y)) 5) 10);

[hear] (((? x / ? y / = 32 / * (x) (y)) 8) 4);

[hear] (((? x / ? y / = 5 / * (x) (y)) 1) 5);

[hear] (((? x / ? y / = 27 / * (x) (y)) 3) 9);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           60)
          15)
         4);

[hear] ((((? z / ? x / ? y / = (z) / * (x) (y)) 0)
          5)
         0);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           165)
          15)
         11);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           104)
          13)
         8);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           36)
          6)
         6);

[hear] ((((? z / ? x / ? y / = (z) / * (x) (y)) 2)
          2)
         1);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           165)
          15)
         11);

[hear] ((((? z /
            ? x /
            ? y /
            = (z) /
            * (x) (y))
           70)
          10)
         7);


       # MATH show some simple function calls
       # and show a way to remember functions across statements
[
hear] (= 49 /
         (? square / square 7) (? x / * (x) (x)));

[hear] (= 49 /
         (? square / square 7) (? x / * (x) (x)));

[hear] (= 81 /
         (? square / square 9) (? x / * (x) (x)));

[hear] (= 16 /
         (? square / square 4) (? x / * (x) (x)));

[hear] (= 81 /
         (? square / square 9) (? x / * (x) (x)));

[hear] (= 9 /
         (? square / square 3) (? x / * (x) (x)));

[hear] (= 1 /
         (? square / square 1) (? x / * (x) (x)));

[hear] (= 1 /
         (? square / square 1) (? x / * (x) (x)));

[hear] (define square / ? x / * (x) (x));

[hear] (= (square 9) 81);

[hear] (= (square 2) 4);

[hear] (= (square 8) 64);

[hear] (= (square 1) 1);

[hear] (define plusone / ? x / + (x) 1);

[hear] (= (plusone 3) 4);

[hear] (= (plusone 6) 7);

[hear] (= (plusone 3) 4);

[hear] (= (plusone 0) 1);


       # MATH show mechanisms for branching
[
hear] (intro if);

[hear] (= (if (false) 5 0) 0);

[hear] (= (if (true) 3 0) 3);

[hear] (= (if (false) 6 6) 6);

[hear] (= (if (true) 7 9) 7);

[hear] (= (if (false) 6 6) 6);

[hear] (= (if (true) 2 7) 2);

[hear] (= (if (true) 0 6) 0);

[hear] (= (if (true) 6 9) 6);

[hear] (= (if (true) 0 4) 0);

[hear] (= (if (false) 9 8) 8);

[hear] (= (if (true) 4 6) 4);

[hear] (= (if (false) 1 3) 3);

[hear] (= (if (true) 7 3) 7);

[hear] (= (if (false) 4 9) 9);

[hear] (= (if (false) 2 1) 1);

[hear] (= (if (true) 1 0) 1);


       # 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 4) 4 8 5 0) 4);

[hear] (= (list-length / (list 5) 3 1 4 6 5) 5);

[hear] (= (list-length / (list 6) 5 0 3 4 7 8) 6);

[hear] (= (list-length / (list 7) 0 8 7 4 9 1 5) 7);

[hear] (= (list-length / (list 3) 0 3 6) 3);

[hear] (= (head / (list 5) 9 9 12 16 0) 9);

[hear] (list= (tail /
                (list 5) 9 9 12 16 0)
               ((list 4) 9 12 16 0));

[hear] (= (head / (list 2) 1 16) 1);

[hear] (list= (tail / (list 2) 1 16) ((list 1) 16));

[hear] (= (head / (list 8) 17 11 7 14 0 12 13 11) 17);

[hear] (list= (tail /
                (list 8) 17 11 7 14 0 12 13 11)
               ((list 7) 11 7 14 0 12 13 11));

[hear] (= (head / (list 8) 15 17 8 6 10 18 19 14) 15);

[hear] (list= (tail /
                (list 8) 15 17 8 6 10 18 19 14)
               ((list 7) 17 8 6 10 18 19 14));

[hear] (= (head / (list 4) 4 7 12 12) 4);

[hear] (list= (tail /
                (list 4) 4 7 12 12)
               ((list 3) 7 12 12));

[hear] (= (head / (list 4) 6 10 6 8) 6);

[hear] (list= (tail /
                (list 4) 6 10 6 8)
               ((list 3) 10 6 8));

[hear] (= (head / (list 2) 9 4) 9);

[hear] (list= (tail / (list 2) 9 4) ((list 1) 4));

[hear] (= (head / (list 9) 7 4 19 17 14 10 5 7 5) 7);

[hear] (list= (tail /
                (list 9) 7 4 19 17 14 10 5 7 5)
               ((list 8) 4 19 17 14 10 5 7 5));

[hear] (= (head / (list 1) 11) 11);

[hear] (list= (tail / (list 1) 11) ((list 0)));

[hear] (= (head / (list 1) 1) 1);

[hear] (list= (tail / (list 1) 1) ((list 0)));

[hear] (= (list-ref ((list 3) 16 2 19) 1) 2);

[hear] (= (list-ref ((list 9) 19 15 15 13 17 6 10 17 14) 0)
           19);

[hear] (= (list-ref ((list 5) 13 13 10 16 7) 2) 10);

[hear] (= (list-ref ((list 7) 6 17 19 3 0 14 15) 1) 17);

[hear] (= (list-ref ((list 10) 17 3 1 4 15 0 3 10 13 9) 2)
           1);

[hear] (= (list-ref ((list 4) 8 0 6 18) 0) 8);

[hear] (= (list-ref
             ((list 10) 13 19 19 15 13 11 15 11 3 7)
             6)
           15);

[hear] (= (list-ref ((list 5) 10 13 7 10 5) 1) 13);

[hear] (= (list-ref ((list 2) 5 2) 1) 2);

[hear] (= (list-ref ((list 1) 14) 0) 14);

[hear] (list= ((list 0)) ((list 0)));

[hear] (list= ((list 1) 7) ((list 1) 7));

[hear] (list= ((list 2) 9 4) ((list 2) 9 4));

[hear] (list= ((list 3) 1 2 13) ((list 3) 1 2 13));

[hear] (list= ((list 4) 17 17 9 6) ((list 4) 17 17 9 6));

       # this next batch of examples are a bit misleading, should streamline
[hear] (not / list= ((list 0)) ((list 1) 4));

[hear] (not / list= ((list 0)) ((list 1) 3));

[hear] (not / list= ((list 1) 7) ((list 2) 4 7));

[hear] (not / list= ((list 1) 7) ((list 2) 7 0));

[hear] (not /
         list= ((list 2) 17 10) ((list 3) 1 17 10));

[hear] (not /
         list= ((list 2) 17 10) ((list 3) 17 10 3));

[hear] (not /
         list= ((list 3) 12 11 3) ((list 4) 5 12 11 3));

[hear] (not /
         list= ((list 3) 12 11 3) ((list 4) 12 11 3 1));

[hear] (not /
         list= ((list 4) 8 11 3 17)
               ((list 5) 1 8 11 3 17));

[hear] (not /
         list= ((list 4) 8 11 3 17)
               ((list 5) 8 11 3 17 3));

       # some helpful functions
[hear] (list= (prepend 12 ((list 0))) ((list 1) 12));

[hear] (list= (prepend 5 ((list 1) 15)) ((list 2) 5 15));

[hear] (list= (prepend 16 ((list 2) 13 17))
               ((list 3) 16 13 17));

[hear] (list= (prepend 13 ((list 3) 12 4 11))
               ((list 4) 13 12 4 11));

[hear] (list= (prepend 12 ((list 4) 7 16 4 18))
               ((list 5) 12 7 16 4 18));

[hear] (list= (prepend 6 ((list 5) 15 19 17 17 6))
               ((list 6) 6 15 19 17 17 6));

[hear] (list= (prepend 12 ((list 6) 18 3 18 11 7 9))
               ((list 7) 12 18 3 18 11 7 9));

[hear] (list= (prepend 15 ((list 7) 19 14 13 16 8 1 10))
               ((list 8) 15 19 14 13 16 8 1 10));

[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 8) ((list 2) 3 8));

[hear] (= (first / pair 3 8) 3);

[hear] (= (second / pair 3 8) 8);

[hear] (list= (pair 7 4) ((list 2) 7 4));

[hear] (= (first / pair 7 4) 7);

[hear] (= (second / pair 7 4) 4);

[hear] (list= (pair 9 7) ((list 2) 9 7));

[hear] (= (first / pair 9 7) 9);

[hear] (= (second / pair 9 7) 7);

[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 5) 5 4 2 1 0) 4 (example-fail))
           1);

[hear] (= (list-find ((list 1) 5) 5 (example-fail)) 0);

[hear] (= (list-find
             ((list 5) 5 4 3 17 8)
             4
             (example-fail))
           1);

[hear] (= (list-find ((list 4) 10 3 3 2) 10 (example-fail))
           0);

[hear] (= (list-find
             ((list 7) 18 8 12 5 13 13 0)
             13
             (example-fail))
           4);

[hear] (= (list-find
             ((list 6) 0 10 14 15 3 17)
             15
             (example-fail))
           3);

[hear] (= (list-find
             ((list 9) 15 10 16 0 16 2 16 8 9)
             10
             (example-fail))
           1);

[hear] (= (list-find ((list 3) 10 18 14) 18 (example-fail))
           1);

[hear] (= (list-find ((list 2) 13 13) 13 (example-fail))
           0);

[hear] (= (list-find
             ((list 7) 13 19 13 19 9 19 1)
             13
             (example-fail))
           0);

[hear] (= (list-find ((list 4) 1 7 16 15) 6 (example-fail))
           100);

[hear] (= (list-find
             ((list 6) 5 10 13 7 12 19)
             8
             (example-fail))
           100);

[hear] (= (list-find
             ((list 8) 19 7 13 1 11 12 8 2)
             16
             (example-fail))
           100);


       # HACK describe changes to the implicit interpreter to allow new special forms
[
hear] (define base-translate / translate);

[hear] (define translate /
         ? x /
         if (= (x) 10) 15 (base-translate / x));

[hear] (= 10 15);

[hear] (= (+ 10 15) 30);

[hear] (define translate / base-translate);

[hear] (not / = 10 15);

[hear] (= (+ 10 15) 25);

       # now can create a special form for lists
[hear] (define translate /
         ? x /
         if (number? /
           x)
          (base-translate /
           x)
          (if (= (head / x) vector)
            (translate /
             prepend
              ((list 2) list (list-length / tail / x))
              (tail /
               x))
            (base-translate /
             x)));

[hear] (= (vector 1 2 3) ((list 3) 1 2 3));

       # now to desugar let expressions
[hear] (define translate-with-vector / translate);

[hear] (define translate-let-form /
         ? x /
         ? body /
         if (= (list-length / x) 0)
          (translate /
           body)
          (translate-let-form
            (tail /
             x)
            (vector
              (vector ? (head / head / x) (body))
              (head /
               tail /
               head /
               x))));

[hear] (define translate /
         ? x /
         if (number? /
           x)
          (translate-with-vector /
           x)
          (if (= (head / x) let)
            (translate-let-form
              (head /
               tail /
               x)
              (head /
               tail /
               tail /
               x))
            (translate-with-vector /
             x)));

[hear] (let ((x 20)) (= (x) 20));

[hear] (let ((x 50) (y 20)) (= (- (x) (y)) 30));

       # the is-list function is now on dubious ground
       # this stuff will be replaced with typing ASAP
[hear] (define is-list /
         ? x /
         not /
         number? /
         x);

[hear] (is-list / (list 2) 1 3);

[hear] (is-list / (list 0));

[hear] (not / is-list 23);

[hear] (is-list /
         (list 3) ((list 2) 2 3) 1 (? x / + (x) 10));


       # MATH introduce sugar for let
       # if would be good to introduce desugarings more rigorously, but for now...
       # ... just a very vague sketch
[
hear] (intro let);

[hear] (= (let ((x 10)) (+ (x) 5))
           ((? x / + (x) 5) 10));

[hear] (= (let ((x 10) (y 5)) (+ (x) (y)))
           (((? x / ? y / + (x) (y)) 10) 5));


       # MATH build up functions of several variables
[
hear] (= ((? x / ? y / - (x) (y)) 3 3) 0);

[hear] (= ((? x / ? y / - (x) (y)) 8 7) 1);

[hear] (= ((? x / ? y / - (x) (y)) 13 9) 4);

[hear] (= ((? x / ? y / - (x) (y)) 15 9) 6);

[hear] (= ((? x / ? y / - (x) (y)) 8 5) 3);

[hear] (define last /
         ? x /
         list-ref (x) (- (list-length / x) 1));

[hear] (define except-last /
         ? x /
         if (> (list-length / x) 1)
          (prepend
            (head /
             x)
            (except-last /
             tail /
             x))
          (vector));

       # test last and except-last
[hear] (= 15 (last / vector 4 5 15));

[hear] (list= (vector 4 5)
               (except-last /
                vector 4 5 15));

[hear] (intro lambda);

[hear] (define prev-translate / translate);

[hear] (define translate /
         let ((prev (prev-translate)))
          (? x /
           if (number? /
             x)
            (prev /
             x)
            (if (= (head / x) lambda)
              (let ((formals (head / tail / x))
                    (body (head / tail / tail / x)))
                (if (> (list-length / formals) 0)
                  (translate
                    (vector
                      lambda
                      (except-last /
                       formals)
                      (vector ? (last / formals) (body))))
                  (translate (body))))
              (prev /
               x))));

       # test lambda
[hear] (= (? x / - (x) 5) (lambda (x) (- (x) 5)));

[hear] (= (? x /
            ? y /
            - (x) (y))
           (lambda (x y) (- (x) (y))));

[hear] (= ((lambda (x y) (- (x) (y))) 9 1) 8);

[hear] (= ((lambda (x y) (- (x) (y))) 15 7) 8);

[hear] (= ((lambda (x y) (- (x) (y))) 6 0) 6);

[hear] (= ((lambda (x y) (- (x) (y))) 11 8) 3);

[hear] (= ((lambda (x y) (- (x) (y))) 6 6) 0);

[hear] (define apply /
         lambda (x y)
          (if (list= (y) (vector))
            (x)
            (apply ((x) (head / y)) (tail / y))));

[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 8 1))
           7);

[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 11 5))
           6);

[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 8 4))
           4);

[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 13 5))
           8);

[hear] (= (apply (lambda (x y) (- (x) (y))) (vector 9 4))
           5);


       # MATH show map function for applying a function across the elements of a list
[
hear] (define map /
         lambda (p lst)
          (if (> (list-length / lst) 0)
            (prepend
              (p (head / lst))
              (map (p) (tail / lst)))
            (vector)));

[hear] (= (map (? x / * (x) 2) (vector 7 8 9))
           (vector 14 16 18));

[hear] (= (map (? x / * (x) 2) (vector 19 7 13 10))
           (vector 38 14 26 20));

[hear] (= (map (? x / * (x) 2) (vector 4 10 7 1 2))
           (vector 8 20 14 2 4));

[hear] (= (map (? x / * (x) 2) (vector 3 18 16 7 9 13))
           (vector 6 36 32 14 18 26));

[hear] (= (map (? x 42) (vector 5 16 15))
           (vector 42 42 42));

[hear] (= (map (? x 42) (vector 13 9 7 14))
           (vector 42 42 42 42));

[hear] (= (map (? x 42) (vector 1 16 3 19 15))
           (vector 42 42 42 42 42));

[hear] (= (map (? x 42) (vector 15 5 2 12 16 14))
           (vector 42 42 42 42 42 42));

[hear] (define crunch /
         lambda (p lst)
          (if (>= (list-length / lst) 2)
            (p (head / lst) (crunch (p) (tail / lst)))
            (if (= (list-length / lst) 1)
              (head /
               lst)
              (undefined))));

[hear] (= (crunch (+) (vector 1 8 18)) 27);

[hear] (= (crunch (+) (vector 3 11 0 5)) 19);

[hear] (= (crunch (+) (vector 7 15 6 11 9)) 48);

[hear] (= (crunch (+) (vector 18 14 19 4 5 17)) 77);


       # MATH introduce mutable objects, and side-effects
[
hear] (intro make-cell);

[hear] (intro set!);

[hear] (intro get!);

[hear] (define demo-mut1 / make-cell 0);

[hear] (set! (demo-mut1) 15);

[hear] (= (get! / demo-mut1) 15);

[hear] (set! (demo-mut1) 5);

[hear] (set! (demo-mut1) 7);

[hear] (= (get! / demo-mut1) 7);

[hear] (define demo-mut2 / make-cell 11);

[hear] (= (get! / demo-mut2) 11);

[hear] (set! (demo-mut2) 22);

[hear] (= (get! / demo-mut2) 22);

[hear] (= (get! / demo-mut1) 7);

[hear] (= (+ (get! / demo-mut1) (get! / demo-mut2))
           29);

[hear] (if (= (get! / demo-mut1) 7)
          (set! (demo-mut1) 88)
          (set! (demo-mut1) 99));

[hear] (= (get! / demo-mut1) 88);

[hear] (if (= (get! / demo-mut1) 7)
          (set! (demo-mut1) 88)
          (set! (demo-mut1) 99));

[hear] (= (get! / demo-mut1) 99);


       # MATH show how to execute a sequence of instructions
[
hear] (intro begin);

[hear] (define prev-translate / translate);

[hear] (define reverse /
         ? x /
         if (>= (list-length / x) 1)
          (prepend
            (last /
             x)
            (reverse /
             except-last /
             x))
          (x));

       # test reverse
[hear] (list= (vector 1 2 3) (reverse / vector 3 2 1));

[hear] (define translate /
         let ((prev (prev-translate)))
          (? x /
           if (number? /
             x)
            (prev /
             x)
            (if (= (head / x) begin)
              (translate
                (vector
                  (vector ? x (vector head (vector x)))
                  (prepend vector (reverse / tail / x))))
              (prev /
               x))));

[hear] (= (begin 1 7 2 4) 4);

[hear] (= (begin
             (set! (demo-mut1) 88)
             (set! (demo-mut1) 6)
             (get! /
              demo-mut1))
           6);

[hear] (= (begin
             (set! (demo-mut2) 88)
             (set! (demo-mut1) 6)
             (get! /
              demo-mut2))
           88);

[hear] (= (begin
             (set! (demo-mut1) 88)
             (set! (demo-mut1) 6)
             (get! /
              demo-mut1)
             4)
           4);


       # 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)
[
hear] (define hash-add /
         lambda (h x y z) (if (= (z) (x)) (y) (h (z))));

[hear] (define hash-ref / lambda (h x) (h (x)));

[hear] (define hash-null / ? x / undefined);

[hear] (define test-hash /
         hash-add (hash-add (hash-null) 3 2) 4 9);

[hear] (= (hash-ref (test-hash) 4) 9);

[hear] (= (hash-ref (test-hash) 3) 2);

[hear] (= (hash-ref (test-hash) 8) (undefined));

[hear] (= (hash-ref (test-hash) 15) (undefined));

[hear] (= (hash-ref (hash-add (test-hash) 15 33) 15) 33);

[hear] (= (hash-ref (test-hash) 15) (undefined));

[hear] (define make-hash /
         ? x /
         if (list= (x) (vector))
          (hash-null)
          (hash-add
            (make-hash (tail / x))
            (first /
             head /
             x)
            (second /
             head /
             x)));

[hear] (= (hash-ref
             (make-hash /
              vector (pair 3 10) (pair 2 20) (pair 1 30))
             3)
           10);

[hear] (= (hash-ref
             (make-hash /
              vector (pair 3 10) (pair 2 20) (pair 1 30))
             1)
           30);


       # OBJECT introduce simple mutable structures
[
hear] (define mutable-struct /
         ? lst /
         let ((data (map (? x / make-cell 0) (lst))))
          (? key /
           list-ref (data) (list-find (lst) (key) (? x 0))));

[hear] (define test-struct1 /
         mutable-struct /
         vector item1 item2 item3);

[hear] (set! (test-struct1 item1) 15);

[hear] (= (get! / test-struct1 item1) 15);


       # OBJECT introduce method handler wrappers
[
hear] (define add-method /
         lambda (object name method)
          (hash-add
            (object)
            (name)
            (? dummy /
             method /
             object)));

[hear] (define call / ? x / x 0);

[hear] (define test-struct2 /
         mutable-struct /
         vector x y);

[hear] (set! (test-struct2 x) 10);

[hear] (set! (test-struct2 y) 20);

[hear] (= (get! / test-struct2 x) 10);

[hear] (= (get! / test-struct2 y) 20);

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

[hear] (= (get! / test-struct3 x) 10);

[hear] (= (get! / test-struct3 y) 20);

[hear] (= (call / test-struct3 sum) 30);

[hear] (set! (test-struct3 y) 10);

[hear] (= (call / test-struct3 sum) 20);

[hear] (set! (test-struct2 y) 5);

[hear] (= (call / test-struct3 sum) 15);


       # TURING introduce turing machine model
       # just for fun!
[
hear] (define safe-tail /
         ? x /
         if (> (list-length / x) 0)
          (if (> (list-length / x) 1)
            (tail /
             x)
            (vector /
             false))
          (? vector /
           false));

[hear] (define safe-head /
         ? x /
         if (> (list-length / x) 0)
          (head /
           x)
          (false));

[hear] (define tape-read /
         ? tape /
         let ((x (second / tape)))
          (if (> (list-length / x) 0)
            (head /
             x)
            (false)));

[hear] (define tape-transition /
         lambda (tape shift value)
          (if (= (shift) 1)
            (pair (prepend (value) (first / tape))
                  (safe-tail /
                   second /
                   tape))
            (if (= (shift) 0)
              (pair (safe-tail /
                     first /
                     tape)
                    (prepend
                      (safe-head /
                       first /
                       tape)
                      (prepend (value) (safe-tail / second / tape))))
              (pair (first /
                     tape)
                    (prepend (value) (safe-tail / second / tape))))));

[hear] (define turing /
         lambda (machine current last tape)
          (if (= (current) (last))
            (tape)
            (let ((next (machine (current) (tape-read / tape))))
              (turing
                (machine)
                (list-ref (next) 0)
                (last)
                (tape-transition
                  (tape)
                  (list-ref (next) 1)
                  (list-ref (next) 2))))));

[hear] (define make-tape /
         ? x /
         pair (vector) (x));

[hear] (define remove-trail /
         ? x /
         ? lst /
         if (> (list-length / lst) 0)
          (if (= (last / lst) (x))
            (remove-trail (x) (except-last / lst))
            (lst))
          (lst));

[hear] (define extract-tape /
         ? x /
         remove-trail (false) (second / x));

[hear] (define tm-binary-increment /
         make-hash /
         vector
          (pair right
                (make-hash /
                 vector
                  (pair 0 (vector right 1 0))
                  (pair 1 (vector right 1 1))
                  (pair (false) (vector inc 0 (false)))))
          (pair inc
                (make-hash /
                 vector
                  (pair 0 (vector noinc 0 1))
                  (pair 1 (vector inc 0 0))
                  (pair (false) (vector halt 2 1))))
          (pair noinc
                (make-hash /
                 vector
                  (pair 0 (vector noinc 0 0))
                  (pair 1 (vector noinc 0 1))
                  (pair (false) (vector halt 1 (false)))))
          (pair halt (make-hash / vector)));

[hear] (= (extract-tape /
            turing
             (tm-binary-increment)
             right
             halt
             (make-tape /
              vector 1 0 0 1))
           (vector 1 0 1 0));

[hear] (= (extract-tape /
            turing
             (tm-binary-increment)
             right
             halt
             (make-tape /
              vector 1 1 1))
           (vector 1 0 0 0));

[hear] (= (extract-tape /
            turing
             (tm-binary-increment)
             right
             halt
             (make-tape /
              vector 1 1 1 0 0 0 1 1 1))
           (vector 1 1 1 0 0 1 0 0 0));


       # MATH introduce sets and set membership
[
hear] (intro element);

[hear] (define element /
         ? x /
         ? lst /
         not /
         = (list-find (lst) (x) (? y / false)) (false));

[hear] (element 8 (vector 8 6 4 1 9));

[hear] (element 9 (vector 8 6 4 1 9));

[hear] (element 1 (vector 8 6 4 1 9));

[hear] (element 6 (vector 8 6 4 1 0 7));

[hear] (element 8 (vector 8 6 4 1 0 7));

[hear] (element 4 (vector 8 6 4 1 0 7));

[hear] (element 7 (vector 8 1 0 7 9));

[hear] (element 7 (vector 8 1 0 7 9));

[hear] (element 0 (vector 8 1 0 7 9));

[hear] (element 8 (vector 8 0 7 9 5));

[hear] (element 8 (vector 8 0 7 9 5));

[hear] (element 9 (vector 8 0 7 9 5));

[hear] (element 8 (vector 8 6 1 3 9));

[hear] (element 3 (vector 8 6 1 3 9));

[hear] (element 1 (vector 8 6 1 3 9));

[hear] (not / element 6 (vector 7 2 5));

[hear] (not / element 6 (vector 4 7 2 5));

[hear] (not / element 6 (vector 3 0 5));

[hear] (not / element 8 (vector 4 0 3 7));

[hear] (not / element 1 (vector 0 3 9));

       # rules for set equality
[hear] (define set-subset /
         ? x /
         ? y /
         if (> (list-length / x) 0)
          (and (element (head / x) (y))
               (set-subset (tail / x) (y)))
          (true));

[hear] (define set= /
         ? x /
         ? y /
         and (set-subset (x) (y)) (set-subset (y) (x)));

[hear] (set= (vector 1 5 9) (vector 5 1 9));

[hear] (set= (vector 1 5 9) (vector 9 1 5));

[hear] (not / set= (vector 1 5 9) (vector 1 5));

       # let's go leave ourselves wide open to Russell's paradox
       # ... by using characteristic functions
       # ... since it doesn't really matter for communication purposes
       # ... and so far this is just used / tested with sets of integers really
[hear] (element 5 (all (? x / = (+ (x) 10) 15)));

[hear] (element 3 (all (? x / = (* (x) 3) (+ (x) 6))));

[hear] (define empty-set / vector);

[hear] (element 0 (natural-set));

[hear] (forall
          (? x /
           => (element (x) (natural-set))
              (element (+ (x) 1) (natural-set))));

[hear] (element 1 (natural-set));

[hear] (element 2 (natural-set));

[hear] (element 3 (natural-set));

[hear] (element 4 (natural-set));

[hear] (element 5 (natural-set));

[hear] (element 6 (natural-set));

[hear] (element 7 (natural-set));

[hear] (element 8 (natural-set));

[hear] (element 9 (natural-set));

[hear] (not / element (true) (natural-set));

[hear] (not / element (false) (natural-set));

[hear] (define boolean-set / vector (true) (false));

[hear] (element (true) (boolean-set));

[hear] (element (false) (boolean-set));

[hear] (not / element 0 (boolean-set));

[hear] (define even-natural-set /
         all /
         ? x /
         exists /
         ? y /
         and (element (y) (natural-set))
             (= (* 2 (y)) (x)));

[hear] (element 0 (natural-set));

[hear] (element 0 (even-natural-set));

[hear] (element 1 (natural-set));

[hear] (not / element 1 (even-natural-set));

[hear] (element 2 (natural-set));

[hear] (element 2 (even-natural-set));

[hear] (element 3 (natural-set));

[hear] (not / element 3 (even-natural-set));

[hear] (element 4 (natural-set));

[hear] (element 4 (even-natural-set));

[hear] (element 5 (natural-set));

[hear] (not / element 5 (even-natural-set));

[hear] (element 6 (natural-set));

[hear] (element 6 (even-natural-set));


       # MATH introduce graph structures
[
hear] (define make-graph /
         lambda (nodes links) (pair (nodes) (links)));

[hear] (define test-graph /
         make-graph
          (vector 1 2 3 4)
          (vector (vector 1 2) (vector 2 3) (vector 1 4)));

[hear] (define graph-linked /
         lambda (g n1 n2)
          (exists /
           ? idx /
           if (and (>= (idx) 0)
                   (< (idx) (list-length / list-ref (g) 1)))
            (list= (list-ref (list-ref (g) 1) (idx))
                   (vector (n1) (n2)))
            (false)));

[hear] (= (graph-linked (test-graph) 1 2) (true));

[hear] (= (graph-linked (test-graph) 1 3) (false));

[hear] (= (graph-linked (test-graph) 2 4) (false));

       # 'if' is used a lot in the next definition in place of and / or
       # this is because I haven't established lazy evaluation forms for and / or
       # so this very inefficient algorithm completely bogs down when combined
       # ... during testing with a dumb implementation for 'exists'.
[hear] (define graph-linked* /
         lambda (g n1 n2)
          (if (= (n1) (n2))
            (true)
            (if (graph-linked (g) (n1) (n2))
              (true)
              (exists
                (? n3 /
                 if (graph-linked (g) (n1) (n3))
                  (graph-linked* (g) (n3) (n2))
                  (false))))));

[hear] (= (graph-linked* (test-graph) 1 2) (true));

[hear] (= (graph-linked* (test-graph) 1 3) (true));

[hear] (= (graph-linked* (test-graph) 2 4) (false));


       # OBJECT introduce simple form of typing, for ease of documentation.
       # An object is simply a function that takes an argument.
       # The argument is the method to call on the object.
       # Types are here taken to be just the existence of a particular method,
       # with that method returning an object of the appropriate type.
[
hear] (define make-integer
         (lambda (v)
           (lambda (x)
             (if (= (x) int)
             (v)
             0))));

[hear] (define objectify
         (? x
            (if (number? (x))
            (make-integer (x))
            (x))));

[hear] (define instanceof
         (lambda (T t)
           (if (number? (t))
           (= (T) int)
           (not (number? ((objectify (t)) (T)))))));

       # add version of lambda that allows types to be declared
[hear] (define prev-translate (translate));

[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) lambda)
                 (let ((formals (head (tail (x))))
                       (body (head (tail (tail (x))))))
                   (if (> (list-length (formals)) 0)
               (if (number? (last (formals)))
                   (translate
                    (vector
                     lambda
                     (except-last (formals))
                     (vector ? (last (formals)) (body))))
                   (let ((formal-name (first (last (formals))))
                     (formal-type (second (last (formals)))))
                     (translate
                      (vector
                   lambda
                   (except-last (formals))
                   (vector
                    ?
                    (formal-name)
                    (vector
                     let
                     (vector (vector
                          (formal-name)
                          (vector
                           (vector objectify (vector (formal-name)))
                           (formal-type))))
                     (body)))))))
               (translate (body))))
                 (prev (x)))))));

       # add conditional form
[hear] (define prev-translate (translate));

[hear] (define translate
         (let ((prev (prev-translate)))
           (? x
             (if (number? (x))
               (prev (x))
               (if (= (head (x)) cond)
                 (let ((cnd (head (tail (x))))
                       (rem (tail (tail (x)))))
                   (if (> (list-length (rem)) 0)
               (translate
                (vector
                         if
                 (first (cnd))
                 (second (cnd))
                 (prepend cond (rem))))
               (translate (cnd))))
                 (prev (x)))))));

[hear] (= 99 (cond 99));

[hear] (= 8 (cond ((true) 8) 11));

[hear] (= 11 (cond ((false) 8) 11));

[hear] (= 7 (cond ((false) 3) ((true) 7) 11));

[hear] (= 3 (cond ((true) 3) ((true) 7) 11));

[hear] (= 11 (cond ((false) 3) ((false) 7) 11));

[hear] (define remove-match
         (lambda (test lst)
           (if (> (list-length (lst)) 0)
           (if (test (head (lst)))
               (remove-match (test) (tail (lst)))
               (prepend (head (lst)) (remove-match (test) (tail (lst)))))
           (lst))));

[hear] (define remove-element
         (lambda (x)
           (remove-match (lambda (y) (= (y) (x))))));

[hear] (list= (vector 1 2 3 5) (remove-element 4 (vector 1 2 3 4 5)));

[hear] (list= (vector 1 2 3 5) (remove-element 4 (vector 1 4 2 4 3 4 5)));

[hear] (define return
         (lambda (T t)
           (let ((obj (objectify (t))))
             (obj (T)))));

[hear] (define tester
         (lambda ((x int) (y int))
           (return int (+ (x) (y)))));

[hear] (= 42 (tester (make-integer 10) (make-integer 32)));

[hear] (= 42 (tester 10 32));

[hear] (define reflective
         (lambda (f)
           ((lambda (x)
              (f (lambda (y) ((x (x)) (y)))))
            (lambda (x)
              (f (lambda (y) ((x (x)) (y))))))));


       # OBJECT an example object -- a 2D point
[
hear] (define point
         (lambda (x y)
           (reflective
            (lambda (self msg)
              (cond ((= (msg) x) (x))
                ((= (msg) y) (y))
                ((= (msg) point) (self))
                ((= (msg) +)
                 (lambda ((p point))
               (point (+ (x) (p x))
                      (+ (y) (p y)))))
                ((= (msg) =)
                 (lambda ((p point))
               (and (= (x) (p x))
                    (= (y) (p y)))))
                0)))));

[hear] (define point1 (point 1 11));

[hear] (define point2 (point 2 22));

[hear] (= 1 (point1 x));

[hear] (= 22 (point2 y));

[hear] (= 11 ((point 11 12) x));

[hear] (= 11 (((point 11 12) point) x));

[hear] (= 16 (((point 16 17) point) x));

[hear] (= 33 (point1 + (point2) y));

[hear] (point1 + (point2) = (point 3 33));

[hear] (point2 + (point1) = (point 3 33));

[hear] ((point 100 200) + (point 200 100) = (point 300 300));

[hear] (instanceof point (point1));

[hear] (not (instanceof int (point1)));

[hear] (instanceof int 5);

[hear] (not (instanceof point 5));


       # OBJECT an example object -- a container
[
hear] (define container
         (lambda (x)
           (let ((contents (make-cell (vector))))
             (reflective
              (lambda (self msg)
            (cond ((= (msg) container) (self))
                  ((= (msg) inventory) (get! (contents)))
                  ((= (msg) add)
               (lambda (x)
                 (if (not (element (x) (get! (contents))))
                     (set! (contents) (prepend (x) (get! (contents))))
                     (false))))
                  ((= (msg) remove)
               (lambda (x)
                 (set! (contents) (remove-element (x) (get! (contents))))))
                  ((= (msg) =)
               (lambda ((c container))
                 (set= (self inventory) (c inventory))))
                  0))))));

       # Can pass anything to container function to create an object
       # Should eventually use a consistent protocol for all objects,
       # but all this stuff is still in flux
[hear] (define pocket (container new));

[hear] (pocket add 77);

[hear] (pocket add 88);

[hear] (pocket add 99);

[hear] (set= (pocket inventory) (vector 77 88 99));

[hear] (pocket remove 88);

[hear] (set= (pocket inventory) (vector 77 99));

[hear] (define pocket2 (container new));

[hear] (pocket2 add 77);

[hear] (pocket2 add 99);

[hear] (pocket2 = (pocket));


       # OBJECT expressing inheritance
       # counter-container adds one method to container: count
[
hear] (define counter-container
         (lambda (x)
           (let ((super (container new)))
             (reflective
              (lambda (self msg)
            (cond ((= (msg)