(B, x0) -> x0
       andBit (B, x1) -> B

       orBit (B, x0) -> B
       orBit (B, x1) -> x1

       xorBit (B, x0) -> B
       xorBit (B, x1) -> notBit (B)

Definitions for sort Octet
--------------------------

We now define octets using a constructor that takes eight bits and returns a byte, together with non-constructors implementing equality, bitwise logical operations, left-shift and right-shift operations on octets, as well as all octet constants needed to formally describe the MAA and its test vectors.

     SORTS
       Octet
     CONS
       buildOctet : Bit Bit Bit Bit Bit Bit Bit Bit -> Octet
       % the first argument of buildOctet contains the most significant bit
     OPNS
       eqOctet : Octet Octet -> Bool
       andOctet : Octet Octet -> Octet
       orOctet : Octet Octet -> Octet
       xorOctet : Octet Octet -> Octet
       leftOctet1 : Octet -> Octet
       leftOctet2 : Octet -> Octet
       leftOctet3 : Octet -> Octet
       leftOctet4 : Octet -> Octet
       leftOctet5 : Octet -> Octet
       leftOctet6 : Octet -> Octet
       leftOctet7 : Octet -> Octet
       rightOctet1 : Octet -> Octet
       rightOctet2 : Octet -> Octet
       rightOctet3 : Octet -> Octet
       rightOctet4 : Octet -> Octet
       rightOctet5 : Octet -> Octet
       rightOctet6 : Octet -> Octet
       rightOctet7 : Octet -> 