(n1)
       n3 -> succ (n2)
       n4 -> succ (n3)
       n5 -> succ (n4)
       n6 -> succ (n5)
       n7 -> succ (n6)
       n8 -> succ (n7)
       n9 -> succ (n8)
       n10 -> succ (n9)
       n11 -> succ (n10)
       n12 -> succ (n11)
       n13 -> succ (n12)
       n14 -> succ (n13)
       n15 -> succ (n14)
       n16 -> succ (n15)
       n17 -> succ (n16)
       n18 -> succ (n17)
       n19 -> succ (n18)
       n20 -> succ (n19)
       n21 -> succ (n20)
       n22 -> succ (n21)

       n254 -> addNat (n12, multNat (n11, n22))

       n256 -> multNat (n16, n16)

       n4100 -> addNat (n4, multNat (n16, n256))

Definitions for sort Bit
------------------------

We now define bits using two constructors and , together with non-constructors implementing bit equality and logical operations on bits.

     SORTS
       Bit
     CONS
       x0 : -> Bit
       x1 : -> Bit
     OPNS
       eqBit : Bit Bit -> Bool
       notBit : Bit -> Bit
       andBit : Bit Bit -> Bit
       orBit : Bit Bit -> Bit
       xorBit : Bit Bit -> Bit
     VARS
       B : Bit
     RULES
       eqBit (x0, x0) -> true
       eqBit (x0, x1) -> false
       eqBit (x1, x0) -> false
       eqBit (x1, x1) -> true

       notBit (x0) -> x1
       notBit (x1) -> x0

       andBit 