| symbol | specification | entry |
|---|
| # | array | function,
array → nat |
| # | set-basic | function,
set → nat |
| # | table | function,
table → nat |
| + | nat-basic2 | function,
nat × nat → nat |
| ++ | set-basic | function,
set × elem → set |
| +1 | nat-basic1 | function,
nat → nat |
| - | nat | function,
nat × nat → nat |
| -- | set-union | function,
set × elem → set |
| -1 | nat-basic1 | function,
nat → nat |
| .elem | slot | function,
slot → elem |
| .elem:= | slot | function,
slot × elem → slot |
| < | nat-basic1 | predicate,
nat × nat |
| > | nat | predicate,
nat × nat |
| SIZE | abs | constant,
nat |
| T | table | variable,
table |
| T0 | table | variable,
table |
| T1 | table | variable,
table |
| T2 | table | variable,
table |
| \ | set-union | function,
set × set → set |
| ] | array | function,
array × nat × elem → array |
| ] | array | function,
array × nat → elem |
| ] | table | function,
table × nat × slot → table |
| ] | table | function,
table × nat → slot |
| a | elem | variable,
elem |
| a0 | slot | variable,
elem |
| abs | abs | function,
table × table × elem → nat × elem → nat → set |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| b | elem | variable,
elem |
| c | elem | variable,
elem |
| disj | abs | predicate,
table × table |
| elem | elem | sort,
|
| empty | slot | constant,
slot |
| found? | cuckoo | variable,
bool |
| full | slot | function,
elem → slot |
| h | cuckoo | variable,
elem → nat |
| h1 | cuckoo | variable,
elem → nat |
| h2 | cuckoo | variable,
elem → nat |
| insert | cuckoo | procedure,
elem, elem → nat, elem → nat : table, table |
| insert_rec | cuckoo | procedure,
elem, elem → nat, elem → nat : table, table |
| inv | abs | predicate,
table × elem → nat |
| lookup | cuckoo | procedure,
elem, table, table, elem → nat, elem → nat : bool |
| m | nat-basic2 | variable,
nat |
| mkarray | array | function,
nat → array |
| mkarray | table | function,
nat → table |
| n | nat-basic1 | variable,
nat |
| n0 | nat-basic1 | variable,
nat |
| n1 | nat-basic1 | variable,
nat |
| nat | nat-basic1 | sort,
|
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| set | set-basic | sort,
|
| slot | slot | variable,
slot |
| slot | slot | sort,
|
| slot0 | table | variable,
slot |
| slot1 | table | variable,
slot |
| table | table | sort,
|
| } | set-union | function,
elem → set |
| ∅ | set-basic | constant,
set |
| ∈ | set-basic | predicate,
elem × set |
| ∩ | set-union | function,
set × set → set |
| ∪ | set-union | function,
set × set → set |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | set-basic | predicate,
set × set |