Z

   $Counter \defs [ n : \nat | n \geq 0 ] $
   $Counter::Incr \defs [ \%D Counter, v? : \nat | n' = n + v? ]$
   $Counter::Decr \defs [ \%D Counter | n > 0;  n' = n - 1 ]$
   $Counter::Value \defs [ \%X Counter; v! : \nat | v! = n ]$
  

   $Bounded::Counter \defs [ Counter | n \leq Max ]$
   $Bounded::Incr \defs [ Counter::Incr | n < Max ]$