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