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