Gappa works on sets of facts about real-valued expressions. The following predicates are handled internally:

`BND(x,I)`

The value of expression

`x`

is included in interval`I`

.`ABS(x,I)`

The absolute value of expression

`x`

is included in interval`I`

.`REL(x,y,I)`

The values of expressions

`x`

and`y`

satisfy [math] with [math].`FIX(x,k)`

The value of expression

`x`

is such that [math].`FLT(x,k)`

The value of expression

`x`

is such that [math].`NZR(x)`

The value of expression

`x`

is not zero.`EQL(x,y)`

Expressions

`x`

and`y`

have equal values.

In the definitions above, `I`

denotes an interval whose
bounds have known numerical values, while `k`

is a known
integer. In the description of the theorems, these parameters will
usually be ignored. For instance, `BND(x)`

just means that an
enclosure of `x`

is known. In addition, `EQL`

properties are also used to express rewriting hints provided by the
user.