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