The RISC ProofNavigator Tutorial and Manual -- A.1.1 Atomic Types

A.1.1 Atomic Types

BOOLEAN
NAT
INT
REAL

Apart from atomic types introduced by the user via type declarations, there are the following builtin atomic types:

BOOLEAN: This type denotes the domain of truth values with literal constants TRUE and FALSE.
NAT: This type denotes the domain of natural numbers with literal constants 0, 1, 2, ...and the addition function + and the multiplication function * on natural numbers.
INT: This type denotes the domain of integer numbers whose values can be constructed from NAT values by application of the negation function -.
REAL: This type denotes the domain of real numbers of which some values can be constructed from INT values by application of the division function /.

NAT is a subtype of INT which is in turn a subtype of REAL. Formulas are constructed from values

of type BOOLEAN.

The type NAT is essentially equivalent to the subtype

SUBTYPE(LAMBDA(x:INT): x >= 0)

A.1.1 Atomic Types