| symbol | specification | entry |
|---|
| # | list-data | function,
list → nat |
| # | store | function,
store → nat |
| # | array | function,
array → nat |
| # | array_of_nat | function,
arrnat → nat |
| # | list_of_nat | function,
natlist → nat |
| # | partition | function,
partition → nat |
| # | map_nat_nat | function,
mapnatnat → nat |
| # | set-basic | function,
set → nat |
| # | set_of_nat | function,
natset → nat |
| #oc | array_of_nat | function,
nat × arrnat × nat → nat |
| #oc | array-perm | function,
elem × array × nat → nat |
| ' | list | function,
elem → list |
| ' | list_of_nat | function,
nat → natlist |
| ' | partition | function,
partelem → partition |
| + | nat-basic2 | function,
nat × nat → nat |
| + | list-data | function,
elem × list → list |
| + | list | function,
elem × elem → list |
| + | list | function,
list × elem → list |
| + | list | function,
list × list → list |
| + | list_of_nat | function,
natlist × nat → natlist |
| + | list_of_nat | function,
natlist × natlist → natlist |
| + | list_of_nat | function,
nat × natlist → natlist |
| + | partition | function,
partelem × partelem → partition |
| + | partition | function,
partition × partelem → partition |
| + | partition | function,
partition × partition → partition |
| + | partition | function,
partelem × partition → partition |
| ++ | list-dup | function,
list × elem → list |
| ++ | list_of_nat | function,
natlist × nat → natlist |
| ++ | partition | function,
partition × partelem → partition |
| ++ | set-basic | function,
set × elem → set |
| ++ | set_of_nat | function,
natset × nat → natset |
| +1 | nat-basic1 | function,
nat → nat |
| - | nat | function,
nat × nat → nat |
| -- | store | function,
store × elem → store |
| -- | map_nat_nat | function,
mapnatnat × nat → mapnatnat |
| -- | set-union | function,
set × elem → set |
| -- | set_of_nat | function,
natset × nat → natset |
| -1 | nat-basic1 | function,
nat → nat |
| -1l | list-del | function,
list × nat → list |
| -1l | list-del | function,
list × elem → list |
| -1l | list_of_nat | function,
natlist × nat → natlist |
| -1l | partition | function,
partition × nat → partition |
| -1l | partition | function,
partition × partelem → partition |
| -l | list-del | function,
list × elem → list |
| -l | list_of_nat | function,
natlist × nat → natlist |
| -l | partition | function,
partition × partelem → partition |
| -p | list_of_nat | function,
natlist × nat → natlist |
| .butlast | list-last | function,
list → list |
| .butlast | list_of_nat | function,
natlist → natlist |
| .butlast | partition | function,
partition → partition |
| .count | partelem | function,
partelem → nat |
| .count:= | partelem | function,
partelem × nat → partelem |
| .first | list-data | function,
list → elem |
| .first | partelem | function,
partelem → nat |
| .first:= | partelem | function,
partelem × nat → partelem |
| .head | list_of_nat | function,
natlist → nat |
| .head | partition | function,
partition → partelem |
| .last | list-last | function,
list → elem |
| .last | list_of_nat | function,
natlist → nat |
| .last | partelem | function,
partelem → nat |
| .last | partition | function,
partition → partelem |
| .last:= | partelem | function,
partelem × nat → partelem |
| .rest | list-data | function,
list → list |
| .tail | list_of_nat | function,
natlist → natlist |
| .tail | partition | function,
partition → partition |
| < | nat-basic1 | predicate,
nat × nat |
| < | list-data | predicate,
list × list |
| < | list_of_nat | predicate,
natlist × natlist |
| < | partition | predicate,
partition × partition |
| > | nat | predicate,
nat × nat |
| A | array_of_nat | variable,
arrnat |
| A0 | array_of_nat | variable,
arrnat |
| A1 | array_of_nat | variable,
arrnat |
| A2 | array_of_nat | variable,
arrnat |
| ADid | partition-refinement | predicate,
arrnat × mapnatnat |
| D | map_nat_nat | variable,
mapnatnat |
| D0 | map_nat_nat | variable,
mapnatnat |
| D1 | map_nat_nat | variable,
mapnatnat |
| D2 | map_nat_nat | variable,
mapnatnat |
| DAid | partition-refinement | predicate,
arrnat × mapnatnat |
| F | partition-refinement | variable,
mapnatnat |
| Fok | partition-refinement | predicate,
mapnatnat × partition × nat |
| MAIN | partition-refinement | procedure,
natlist : arrnat, mapnatnat, partition, mapnatnat |
| NEWPARTS | partition-refinement | procedure,
: partition, mapnatnat |
| P | partition | variable,
partition |
| P0 | partition | variable,
partition |
| P1 | partition | variable,
partition |
| P10 | partition | variable,
partition |
| P2 | partition | variable,
partition |
| P3 | partition | variable,
partition |
| P4 | partition | variable,
partition |
| P5 | partition | variable,
partition |
| P6 | partition | variable,
partition |
| P7 | partition | variable,
partition |
| P8 | partition | variable,
partition |
| P9 | partition | variable,
partition |
| Pdone | partition-refinement | variable,
partition |
| Pnew | partition-refinement | variable,
partition |
| REFINE | partition-refinement | procedure,
natlist, mapnatnat : arrnat, mapnatnat, partition |
| REFINEONE | partition-refinement | procedure,
nat, mapnatnat : arrnat, mapnatnat, partition |
| S | set_of_nat | variable,
natset |
| S0 | set_of_nat | variable,
natset |
| S1 | set_of_nat | variable,
natset |
| S2 | set_of_nat | variable,
natset |
| X | list_of_nat | variable,
natlist |
| X0 | list_of_nat | variable,
natlist |
| X1 | list_of_nat | variable,
natlist |
| X10 | list_of_nat | variable,
natlist |
| X2 | list_of_nat | variable,
natlist |
| X3 | list_of_nat | variable,
natlist |
| X4 | list_of_nat | variable,
natlist |
| X5 | list_of_nat | variable,
natlist |
| X6 | list_of_nat | variable,
natlist |
| X7 | list_of_nat | variable,
natlist |
| X8 | list_of_nat | variable,
natlist |
| X9 | list_of_nat | variable,
natlist |
| XornoX | partition-refinement | predicate,
partelem × natlist × arrnat |
| [] | list-data | constant,
list |
| [] | list_of_nat | constant,
natlist |
| [] | partition | constant,
partition |
| \ | set-union | function,
set × set → set |
| \ | set_of_nat | function,
natset × natset → natset |
| ] | list-del | function,
list × nat × elem → list |
| ] | list-del | function,
list × nat → elem |
| ] | store | function,
store × elem → data |
| ] | store | function,
store × elem × data → store |
| ] | array | function,
array × nat × elem → array |
| ] | array | function,
array × nat → elem |
| ] | array_of_nat | function,
arrnat × nat × nat → arrnat |
| ] | array_of_nat | function,
arrnat × nat → nat |
| ] | list_of_nat | function,
natlist × nat × nat → natlist |
| ] | list_of_nat | function,
natlist × nat → nat |
| ] | partition | function,
partition × nat × partelem → partition |
| ] | partition | function,
partition × nat → partelem |
| ] | map_nat_nat | function,
mapnatnat × nat → nat |
| ] | map_nat_nat | function,
mapnatnat × nat × nat → mapnatnat |
| ] | partition-refinement | function,
mapnatnat × nat × nat × nat → mapnatnat |
| a | elem | variable,
elem |
| a0 | list-data | variable,
elem |
| a0 | store | variable,
elem |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| arrnat | array_of_nat | sort,
|
| b | elem | variable,
elem |
| butlastn | list-last | function,
nat × list → list |
| butlastn | list_of_nat | function,
nat × natlist → natlist |
| butlastn | partition | function,
nat × partition → partition |
| c | elem | variable,
elem |
| d | data | variable,
data |
| d0 | data | variable,
data |
| d1 | data | variable,
data |
| d2 | data | variable,
data |
| data | data | sort,
|
| disj | list-dup | predicate,
list × list |
| disj | list_of_nat | predicate,
natlist × natlist |
| disj | partition | predicate,
partition × partition |
| divides | partition-refinement | predicate,
partition × partition × natlist × arrnat |
| dups | list-dup | predicate,
list |
| dups | list_of_nat | predicate,
natlist |
| dups | partition | predicate,
partition |
| elem | elem | sort,
|
| elemdata | store | sort,
|
| elemdatavar | store | variable,
elemdata |
| fillfirst | list-last | function,
nat × elem × list → list |
| fillfirst | list_of_nat | function,
nat × nat × natlist → natlist |
| fillfirst | partition | function,
nat × partelem × partition → partition |
| firstn | list-del | function,
nat × list → list |
| firstn | list_of_nat | function,
nat × natlist → natlist |
| firstn | partition | function,
nat × partition → partition |
| frome | list-del | function,
list × elem → list |
| frome | list_of_nat | function,
natlist × nat → natlist |
| frome | partition | function,
partition × partelem → partition |
| i | partition-refinement | variable,
nat |
| lastn | list-del | function,
nat × list → list |
| lastn | list_of_nat | function,
nat × natlist → natlist |
| lastn | partition | function,
nat × partition → partition |
| length_of_P | partition-refinement | variable,
nat |
| list | list-data | sort,
|
| list2set | partition-refinement | function,
natlist → natset |
| m | nat-basic2 | variable,
nat |
| m0 | partelem | variable,
nat |
| m1 | partelem | variable,
nat |
| m2 | partelem | variable,
nat |
| m3 | partelem | variable,
nat |
| m4 | partelem | variable,
nat |
| mapnatnat | map_nat_nat | sort,
|
| mkarray | array | function,
nat → array |
| mkarray | array_of_nat | function,
nat → arrnat |
| mklist | list-last | function,
elem × nat → list |
| mklist | list_of_nat | function,
nat × nat → natlist |
| mklist | partition | function,
partelem × nat → partition |
| mktwo | list_of_nat | function,
nat × nat → natlist |
| n | nat-basic1 | variable,
nat |
| n0 | nat-basic1 | variable,
nat |
| n1 | nat-basic1 | variable,
nat |
| n2 | array_of_nat | variable,
nat |
| n2 | list_of_nat | variable,
nat |
| n2 | map_nat_nat | variable,
nat |
| n2 | set_of_nat | variable,
nat |
| n3 | array_of_nat | variable,
nat |
| n3 | list_of_nat | variable,
nat |
| n3 | map_nat_nat | variable,
nat |
| n3 | set_of_nat | variable,
nat |
| n4 | array_of_nat | variable,
nat |
| n4 | list_of_nat | variable,
nat |
| n4 | map_nat_nat | variable,
nat |
| n4 | set_of_nat | variable,
nat |
| n5 | list_of_nat | variable,
nat |
| n5 | map_nat_nat | variable,
nat |
| n6 | map_nat_nat | variable,
nat |
| n7 | map_nat_nat | variable,
nat |
| n8 | map_nat_nat | variable,
nat |
| n9 | map_nat_nat | variable,
nat |
| nat | nat-basic1 | sort,
|
| natlist | list_of_nat | sort,
|
| natnat | map_nat_nat | sort,
|
| natset | set_of_nat | sort,
|
| nn | map_nat_nat | variable,
natnat |
| nodups | partition-refinement | predicate,
arrnat |
| okp | partition-refinement | predicate,
partelem × nat |
| p | partelem | variable,
partelem |
| p0 | partition | variable,
partelem |
| p1 | partition | variable,
partelem |
| p2 | partition | variable,
partelem |
| partelem | partelem | sort,
|
| partelem-sem | partition-refinement | variable,
arrnat → natset |
| partition | partition | sort,
|
| partitionRefinement | partition-refinement | predicate,
partition × arrnat × partition × arrnat × natlist |
| partitions | partition-refinement | predicate,
partition × nat |
| pe | partelem | function,
nat × nat × nat → partelem |
| perm | array_of_nat | predicate,
arrnat × arrnat |
| perm | array-perm | predicate,
array × array |
| pos | list-del | function,
elem × list → nat |
| pos | list_of_nat | function,
nat × natlist → nat |
| pos | partition | function,
partelem × partition → nat |
| resetcnt | partition-refinement | function,
partition → partition |
| restn | list-del | function,
nat × list → list |
| restn | list_of_nat | function,
nat × natlist → natlist |
| restn | partition | function,
nat × partition → partition |
| rev | list-last | function,
list → list |
| rev | list_of_nat | function,
natlist → natlist |
| rev | partition | function,
partition → partition |
| rmdup | list-dup | function,
list → list |
| rmdup | list_of_nat | function,
natlist → natlist |
| rmdup | partition | function,
partition → partition |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| samepartitions | partition-refinement | predicate,
partition × arrnat × partition × arrnat |
| set | set-basic | sort,
|
| split | partition-refinement | predicate,
partition × arrnat × natlist |
| splitone | partition-refinement | predicate,
partelem × arrnat × natlist |
| st | store | variable,
store |
| st0 | store | variable,
store |
| st1 | store | variable,
store |
| st2 | store | variable,
store |
| startorfin | partition-refinement | predicate,
partelem × partition |
| store | store | sort,
|
| sublist | list-del | function,
nat × nat × list → list |
| sublist | list_of_nat | function,
nat × nat × natlist → natlist |
| sublist | partition | function,
nat × nat × partition → partition |
| x | list-data | variable,
list |
| x | partition-refinement | variable,
nat |
| x0 | list-data | variable,
list |
| x1 | list-data | variable,
list |
| x2 | list-data | variable,
list |
| y | list-data | variable,
list |
| y0 | list-data | variable,
list |
| y1 | list-data | variable,
list |
| y2 | list-data | variable,
list |
| z | list-data | variable,
list |
| z0 | list-data | variable,
list |
| z1 | list-data | variable,
list |
| z2 | list-data | variable,
list |
| } | set-union | function,
elem → set |
| } | set_of_nat | function,
nat → natset |
| × | store | function,
elem × data → elemdata |
| × | map_nat_nat | function,
nat × nat → natnat |
| ∅ | store | constant,
store |
| ∅ | map_nat_nat | constant,
mapnatnat |
| ∅ | set-basic | constant,
set |
| ∅ | set_of_nat | constant,
natset |
| ∈ | list | predicate,
elem × list |
| ∈ | store | predicate,
elemdata × store |
| ∈ | store | predicate,
elem × store |
| ∈ | list_of_nat | predicate,
nat × natlist |
| ∈ | partition | predicate,
partelem × partition |
| ∈ | map_nat_nat | predicate,
natnat × mapnatnat |
| ∈ | map_nat_nat | predicate,
nat × mapnatnat |
| ∈ | partition-refinement | predicate,
nat × partelem |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | set_of_nat | predicate,
nat × natset |
| ∩ | set-union | function,
set × set → set |
| ∩ | set_of_nat | function,
natset × natset → natset |
| ∪ | set-union | function,
set × set → set |
| ∪ | set_of_nat | function,
natset × natset → natset |
| ≤ | nat | predicate,
nat × nat |
| ≥ | nat | predicate,
nat × nat |
| ⊆ | store | predicate,
store × store |
| ⊆ | map_nat_nat | predicate,
mapnatnat × mapnatnat |
| ⊆ | set-basic | predicate,
set × set |
| ⊆ | set_of_nat | predicate,
natset × natset |
| ⊑ | list-last | predicate,
list × list |
| ⊑ | list_of_nat | predicate,
natlist × natlist |
| ⊑ | partition | predicate,
partition × partition |
| ⊒ | list-last | predicate,
list × list |
| ⊒ | list_of_nat | predicate,
natlist × natlist |
| ⊒ | partition | predicate,
partition × partition |
| ⟧ | partition-refinement | function,
partelem → arrnat → natset |