have been put together and separated with blank lines when appropriate. Also, the arguments of certain non-constructors are separated by semicolons rather than commas when it helps to distinguish arguments of different nature (e.g., summand bits, carry, or sum bits).

All machine words (octets, blocks, etc.) are represented according to the “big endian” convention, i.e., the first argument of each corresponding constructor denote the most significant bit.

Definitions for sort Bool
-------------------------

We first define Booleans using the and constructors, together with two non-constructors implementing logical conjunction and disjunction.

     SORTS
       Bool
     CONS
       false : -> Bool
       true : -> Bool
     OPNS
       andBool : Bool Bool -> Bool
       orBool : Bool Bool -> Bool
     VARS
       L : Bool
     RULES
       andBool (false, L) -> false
       andBool (true, L) -> L

       orBool (false, L) -> L
       orBool (true, L) -> true

Definitions for sort Nat
------------------------

We then define natural numbers in the Peano style using the and constructors, together with non-constructors implementing addition, multiplication, equality, strict order, and a few constants.

     SORTS
       Nat
     CONS
       zero : -> Nat
       succ : Nat -> Nat
     OPNS
       addNat : Nat Nat -> Nat
       multNat : Nat Nat -> Nat
       eqNat : Nat Nat -> Bool
       