# Normalisation of Expressions

In order to limit the number of rules in the prover base, expressions are normalized. Every expression that the prover manipulates must have been first normalized. Thus every user rule found in a Pmm file is automatically normalized when it is loaded. However the rules that are stored in the PatchProver need to be manually normalized, otherwise they may induce an anomalous behavior of the prover.

The normal forms are the following:

| Expression  | Normal form                      |
| ----------- | -------------------------------- |
| n > m – 1   | m <= n                           |
| m < n       | m <= n – 1                       |
| a <=> b     | (a => b) & (b => a)              |
| a <: b      | a : POW(b)                       |
| a <<: b     | a : POW (b) & not (a = b)        |
| a /: b      | not (a : b)                      |
| a /= b      | not (a = b)                      |
| a /<: b     | not (a : POW(b))                 |
| a /<<: b    | a : POW(b) => a = b              |
| a : NATURAL | a : INTEGER & 0 <= a             |
| NATURAL1    | NATURAL – {0}                    |
| NAT1        | NAT – {0}                        |
| FIN1(A)     | FIN(A) – {}                      |
| POW1(A)     | POW(A) – {}                      |
| seq1(A)     | seq(A) – {}                      |
| iseq1(A)    | iseq(A) – {{}}                   |
| perm(E)     | iseq(E) / (NATURAL – {0} +->> E) |
| <>          | {}                               |
| {x, y}      | {x} / {y}                        |
| P}          | SET(x).P                         |

When writing a rule, it is necessary to check that this rule is indeed normalized. Otherwise, the rule will be normalized when it is loaded and may no longer be applicable as desired.

For instance, the following rule:

```
btest(0<x)
=>
0<=x**2-1
```

is normalized into

```
btest(0+1<=x)
=>
0<=x**2-1
```

But the guard btest only accepts as argument expression of the form a op b, where a and b are integers. This rule will thus never be applicable. The following rule should be thus preferred:

```
btest(1<=x)
=>
0<=x**2-1
```


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://b-method.gitbook.io/training-resources-for-atelier-b/guides-and-tutorials/applying-the-b-method/mathematical-proof/writing-mathematical-rules/normalisation-of-expressions.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.