||              bin      bbat      -7
PROOFMETHOD		opn	keyl	11
PROOFLEVEL		bin	keyl	-9
AUTOPROOF		bin	keyl	-9
NORMAL			bin	keyl	-9
FORWARD			bin	keyl	-9
NORMALTHEORIES		bin	keyl	-9
FORWARDTHEORIES		bin	keyl	-9
THEORIES		bin	keyl	-9
MACHINE			opn	keyl	11
CONSTRAINTS		bin	keyl	-9
SEES			bin	keyl	-9
SETS			bin	keyl	-9
CONSTANTS		bin	keyl	-9
VISIBLE_CONSTANTS	bin	keyl	-9
CONCRETE_CONSTANTS	bin	keyl	-9
HIDDEN_CONSTANTS	bin	keyl	-9
ABSTRACT_CONSTANTS	bin	keyl	-9
PROPERTIES		bin	keyl	-9
INCLUDES		bin	keyl	-9
PROMOTES		bin	keyl	-9
EXTENDS			bin	keyl	-9
USES			bin	keyl	-9
VARIABLES		bin	keyl	-9
HIDDEN_VARIABLES	bin	keyl	-9
ABSTRACT_VARIABLES	bin	keyl	-9
VISIBLE_VARIABLES	bin	keyl	-9
CONCRETE_VARIABLES	bin	keyl	-9
INVARIANT		bin	keyl	-9
ASSERTIONS		bin	keyl	-9
INITIALISATION		bin	keyl	-9
OPERATIONS		bin	keyl	-9
REFINEMENT		opn	keyl	11
REFINES			bin	keyl	-9
IMPLEMENTATION		opn	keyl	11
IMPORTS			bin	keyl	-9
VALUES			bin	keyl	-9
DEFINITIONS		bin	keyl	-9

finite			unr nrml    11
infinite		unr nrml    11
choice			unr nrml    11

or				bin blba    -5
not				unr nrml    11
/:				bin	nrml	 0
[]				bin blba    -7
==>				bin blba    -6
::				bin blka    -4
skip			atm	nrml	 0
BEGIN			opn	keyl	11
ASSERT			opn	keyl	11
PRE				opn	keyl	11
IF				opn	keyw	11
THEN			bin	keyl	-9
ELSIF			bin	keyw	-9
ELSE			bin	keyl	-9
ANY				opn	keyw	11
WHERE			bin	keyl	-9
LET				opn	keyw	11
BE				bin	keyl	-9
IN				bin	keyl	-9
CHOICE			opn	keyl	11
OR				bin	keyw	-9
SELECT			opn	keyw	11
WHEN			bin	keyw	-9
CASE			opn	keyw	11
OF				bin	keyl	-9
EITHER			opn	keyw	11
VAR				opn	keyw	11
WHILE			opn	keyw	11
DO				bin	keyl	-9
VARIANT			bin	keyl	-9
bool			unr	nrml	11
<--				bin blba    -1

INTEGER			atm	nrml	 0
INT				atm	nrml	 0
NATURAL			atm	nrml	 0
NATURAL1		atm	nrml	 0
NAT				atm	nrml	 0
NAT1			atm	nrml	 0
BOOL			atm	nrml	 0
STRING			atm	nrml	 0

TRUE			atm nrml     0
FALSE			atm nrml     0

|->				bin	nrml	 0

POW				unr	nrml	11
FIN				unr	nrml	11
FINI				unr	nrml	11
{}				atm	nrml	0
POW1			unr	nrml	11
FIN1			unr	nrml	11
FINI1			unr	nrml	11

<:				bin	blba	-2
<<:				bin	blba	-2
/<:				bin	blba	-2
/<<:			bin	blba	-2
prj1			unr	nrml	11
prj2			unr	nrml	11
\/				bin	blba	0
/\				bin	blba	0
..				bin	nrml	1
union			unr	nrml	11
inter			unr	nrml	11
UNION			unr	nrml	11
INTER			unr	nrml	11

<->				bin	blba	-1
+->				bin	blba	-1
-->				bin	blba	-1
>+>				bin	blba	-1
>->				bin	blba	-1
+->>			bin	blba	-1
-->>			bin	blba	-1
>->>			bin	blba	-1

id				unr	nrml	11
><				bin	nrml	 0
<|				bin	nrml	 0
<<|				bin	nrml	 0
|>				bin	nrml	 0
|>>				bin	nrml	 0
<+				bin	nrml	 0
+>				bin	nrml	 0
dom				unr	nrml	11
ran				unr	nrml	11
iterate			unr nrml    11
closure			unr nrml    11
closure1		unr nrml    11
fnc				unr nrml    11
rel				unr nrml    11

card			unr	nrml	11
succ			atm	nrml	 0
pred			atm	nrml	 0
max				unr	nrml	11
min				unr	nrml	11
MAXINT			atm	nrml	 0
MININT			atm	nrml	 0
mod				bin	blba	 3
**				bin nrml	 4
SIGMA			unr	nrml	11
PI				unr	nrml	11

<>				atm	nrml	0
seq				unr	nrml	11
iseq			unr	nrml	11
seq1			unr	nrml	11
iseq1			unr	nrml	11
perm			unr	nrml	11
conc			unr	nrml	11
front			unr	nrml	11
tail			unr	nrml	11
first			unr	nrml	11
last			unr	nrml	11
size			unr	nrml	11
rev				unr	nrml	11
->				bin	nrml	 0
<-				bin	nrml	 0
/|\				bin	blba	 0
\|/				bin	blba	 0
plus			atm      nrml      0
minus			atm      nrml      0
multiply		atm      nrml      0
divide			atm      nrml      0
SET			unr	nrml	11
SPESPE			bin	nrml	10
cod                          unr     nrml    11

_multE	bin	blba	3
_multA	bin	blba	3
_moinsE	bin	blba	2
_moinsA	bin	blba	2

