type Bit is Boolean, NaturalNumber
   sorts Bit (*! implementedby ADT_BIT comparedby ADT_CMP_BIT
                 enumeratedby ADT_ENUM_BIT printedby ADT_PRINT_BIT *)
   opns 0 (*! implementedby ADT_LOW constructor *) : -> Bit 
        1 (*! implementedby ADT_HIGH constructor *) : -> Bit 
        not (*! implementedby ADT_NEG *) : Bit -> Bit 
	_eq_ (*! implementedby ADT_EQ_BIT *), 
	_ne_ (*! implementedby ADT_NE_BIT *), 
	_lt_ (*! implementedby ADT_LT_BIT *), 
	_le_ (*! implementedby ADT_LE_BIT *), 
	_ge_ (*! implementedby ADT_GE_BIT *), 
	_gt_ (*! implementedby ADT_GT_BIT *) : Bit, Bit -> Bool
	NatNum (*! implementedby ADT_NATNUM_BIT *) : Bit -> Nat
   eqns
      forall x,y : Bit
      ofsort Bit
         not (0) = 1;
         not (1) = 0;
      ofsort Nat
	 NatNum (0) = 0;
 	 NatNum (1) = Succ (0);
      ofsort Bool
 	 x eq y = NatNum (x) eq NatNum (y);
 	 x ne y = NatNum (x) ne NatNum (y);
 	 x lt y = NatNum (x) lt NatNum (y);
 	 x le y = NatNum (x) le NatNum (y);
 	 x ge y = NatNum (x) ge NatNum (y);
 	 x gt y = NatNum (x) gt NatNum (y);
endtype