TYPE Integers IS
  SORTS
    number
  OPNS
    one: -> number
    succ (*| partial check ($1) |*): number -> number
  ENDTYPE