fmod BINARY is
  protecting INT .
  sorts Bit Bits .
  subsort Bit < Bits .

  ops 0 1 : -> Bit .

  op __ : Bits Bits -> Bits [assoc prec 1 gather (e E)] .
  op |_| : Bits -> Int .
  op normalize : Bits -> Bits .
  op bits : Bits Int Int -> Bits .
  op _++_  : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] .
  op _**_  : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] .
  op _>_  : Bits Bits -> Bool [prec 6 gather (E E)] .
  op not_ : Bits -> Bits [prec 2 gather (E)] .
  op _-- : Bits -> Bits [prec 2 gather (E)] .

  vars S T : Bits .
  vars B C : Bit .
  var L : Bool .
  vars I J : Int .

  *** Length
  eq | B | = 1 .
  eq | S B | = | S | + 1 .

  *** Extract Bits...
  eq bits(S B,0,0) = B .
  eq bits(B,J,0) = B .
  ceq bits(S B,J,0) = bits(S, J - 1,0) B if J > 0 .
  ceq bits(S B,J,I) = bits(S,J - 1,I - 1) if I > 0 and J > 0 .

  *** Not
  eq not (S T) = (not S) (not T) .
  eq not 0 = 1 .
  eq not 1 = 0 .

  *** Normalize supresses zeros at the
  *** left of a binary number
  eq normalize(0) = 0 .
  eq normalize(1) = 1 .
  eq normalize(0 S) = normalize(S) .
  eq normalize(1 S) = 1 S .

  *** Greater than
  eq 0 > S = false .
  eq 1 > (0).Bit = true .
  eq 1 > (1).Bit = false .
  eq B > (0 S) = B > S .
  eq B > (1 S) = false .
  eq (1 S) > B = true .
  eq (B S) > (C T)
    = if | normalize(B S) | > | normalize(C T) |
      then true
      else if | normalize(B S) | < | normalize(C T) |
           then false
           else (S > T)
           fi
      fi .

  *** Binary addition
  eq 0 ++ S = S .
  eq 1 ++ 1 = 1 0 .
  eq 1 ++ (T 0) = T 1 .
  eq 1 ++ (T 1) = (T ++ 1) 0 .
  eq (S B) ++ (T 0) = (S ++ T) B .
  eq (S 1) ++ (T 1) = (S ++ T ++ 1) 0 .

  *** Binary multiplication
  eq 0 ** T = 0 .
  eq 1 ** T = T .
  eq (S B) ** T = ((S ** T) 0) ++ (B ** T) .

  *** Decrement
  eq 0 -- = 0 .
  eq 1 -- = 0 .
  eq (S 1) -- = normalize(S 0) .
  ceq (S 0) -- = normalize(S --) 1 if normalize(S) =/= 0 .
  ceq (S 0) -- = 0 if normalize(S) == 0 .

endfm