## Predicates

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 $x = y \times (1 + \varepsilon)$ with $\varepsilon\in I$.

FIX(x,k)

The value of expression x is such that $\exists m \in \mathbb{Z},~x = m\cdot 2^k$.

FLT(x,k)

The value of expression x is such that $\exists m,e \in \mathbb{Z},~x = m\cdot 2^e \land |m| \lt 2^k$.

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.