| Symbol | Specification | Kind | Type |
|---|
| # . | set_of_nat | f | natset → nat |
| # . | array_of_nat | f | arrnat → nat |
| # . | list_of_nat | f | natlist → nat |
| # . | partition | f | partition → nat |
| # . | map_nat_nat | f | mapnatnat → nat |
| #oc | array_of_nat | f | nat × arrnat × nat → nat |
| . ' | list_of_nat | f | nat → natlist |
| . ' | partition | f | partelem → partition |
| . + . | nat-basic2 | f | nat × nat → nat |
| . + . | partition | f | partelem × partition → partition |
| . + . | list_of_nat | f | natlist × nat → natlist |
| . + . | partition | f | partition × partition → partition |
| . + . | list_of_nat | f | natlist × natlist → natlist |
| . + . | partition | f | partition × partelem → partition |
| . + . | list_of_nat | f | nat × natlist → natlist |
| . + . | partition | f | partelem × partelem → partition |
| . ++ . | set_of_nat | f | natset × nat → natset |
| . ++ . | partition | f | partition × partelem → partition |
| . ++ . | list_of_nat | f | natlist × nat → natlist |
| . +1 | nat-basic1 | f | nat → nat |
| . - . | nat | f | nat × nat → nat |
| . -- . | set_of_nat | f | natset × nat → natset |
| . -- . | map_nat_nat | f | mapnatnat × nat → mapnatnat |
| . -1 | nat-basic1 | f | nat → nat |
| . -1l . | list_of_nat | f | natlist × nat → natlist |
| . -1l . | partition | f | partition × partelem → partition |
| . -1l . | partition | f | partition × nat → partition |
| . -l . | partition | f | partition × partelem → partition |
| . -l . | list_of_nat | f | natlist × nat → natlist |
| . -p . | list_of_nat | f | natlist × nat → natlist |
| . .butlast | list_of_nat | f | natlist → natlist |
| . .butlast | partition | f | partition → partition |
| . .count | partelem | f | partelem → nat |
| . .count:= . | partelem | f | partelem × nat → partelem |
| . .first | partelem | f | partelem → nat |
| . .first:= . | partelem | f | partelem × nat → partelem |
| . .head | list_of_nat | f | natlist → nat |
| . .head | partition | f | partition → partelem |
| . .last | list_of_nat | f | natlist → nat |
| . .last | partelem | f | partelem → nat |
| . .last | partition | f | partition → partelem |
| . .last:= . | partelem | f | partelem × nat → partelem |
| . .tail | list_of_nat | f | natlist → natlist |
| . .tail | partition | f | partition → partition |
| . < . | list_of_nat | p | natlist × natlist |
| . < . | partition | p | partition × partition |
| . < . | nat-basic1 | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | array_of_nat | f | arrnat × nat → nat |
| . [ . ] | partition-refinement | f | mapnatnat × nat × nat × nat → mapnatnat |
| . [ . ] | array_of_nat | f | arrnat × nat × nat → arrnat |
| . [ . ] | map_nat_nat | f | mapnatnat × nat × nat → mapnatnat |
| . [ . ] | list_of_nat | f | natlist × nat × nat → natlist |
| . [ . ] | map_nat_nat | f | mapnatnat × nat → nat |
| . [ . ] | list_of_nat | f | natlist × nat → nat |
| . [ . ] | partition | f | partition × nat → partelem |
| . [ . ] | partition | f | partition × nat × partelem → partition |
| . \ . | set_of_nat | f | natset × natset → natset |
| . × . | map_nat_nat | f | nat × nat → natnat |
| . ∈ . | partition-refinement | p | nat × partelem |
| . ∈ . | set_of_nat | p | nat × natset |
| . ∈ . | list_of_nat | p | nat × natlist |
| . ∈ . | map_nat_nat | p | nat × mapnatnat |
| . ∈ . | partition | p | partelem × partition |
| . ∈ . | map_nat_nat | p | natnat × mapnatnat |
| . ∩ . | set_of_nat | f | natset × natset → natset |
| . ∪ . | set_of_nat | f | natset × natset → natset |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | set_of_nat | p | natset × natset |
| . ⊆ . | map_nat_nat | p | mapnatnat × mapnatnat |
| . ⊑ . | list_of_nat | p | natlist × natlist |
| . ⊑ . | partition | p | partition × partition |
| . ⊒ . | list_of_nat | p | natlist × natlist |
| . ⊒ . | partition | p | partition × partition |
| . mktwo . | list_of_nat | f | nat × nat → natlist |
| [] | partition | c | partition |
| [] | list_of_nat | c | natlist |
| { . } | set_of_nat | f | nat → natset |
| ∅ | map_nat_nat | c | mapnatnat |
| ∅ | set_of_nat | c | natset |
| ⟦ . ⟧ | partition-refinement | f | partelem → arrnat → natset |
| A | array_of_nat | v | arrnat |
| A0 | array_of_nat | v | arrnat |
| A1 | array_of_nat | v | arrnat |
| A2 | array_of_nat | v | arrnat |
| ADid | partition-refinement | p | arrnat × mapnatnat |
| D | map_nat_nat | v | mapnatnat |
| D0 | map_nat_nat | v | mapnatnat |
| D1 | map_nat_nat | v | mapnatnat |
| D2 | map_nat_nat | v | mapnatnat |
| DAid | partition-refinement | p | arrnat × mapnatnat |
| F | partition-refinement | v | mapnatnat |
| Fok | partition-refinement | p | mapnatnat × partition × nat |
| MAIN | partition-refinement | pr | natlist : arrnat, mapnatnat, partition, mapnatnat |
| NEWPARTS | partition-refinement | pr | : partition, mapnatnat |
| P | partition | v | partition |
| P0 | partition | v | partition |
| P1 | partition | v | partition |
| P10 | partition | v | partition |
| P2 | partition | v | partition |
| P3 | partition | v | partition |
| P4 | partition | v | partition |
| P5 | partition | v | partition |
| P6 | partition | v | partition |
| P7 | partition | v | partition |
| P8 | partition | v | partition |
| P9 | partition | v | partition |
| Pdone | partition-refinement | v | partition |
| Pnew | partition-refinement | v | partition |
| REFINE | partition-refinement | pr | natlist, mapnatnat : arrnat, mapnatnat, partition |
| REFINEONE | partition-refinement | pr | nat, mapnatnat : arrnat, mapnatnat, partition |
| S | set_of_nat | v | natset |
| S0 | set_of_nat | v | natset |
| S1 | set_of_nat | v | natset |
| S2 | set_of_nat | v | natset |
| X | list_of_nat | v | natlist |
| X0 | list_of_nat | v | natlist |
| X1 | list_of_nat | v | natlist |
| X10 | list_of_nat | v | natlist |
| X2 | list_of_nat | v | natlist |
| X3 | list_of_nat | v | natlist |
| X4 | list_of_nat | v | natlist |
| X5 | list_of_nat | v | natlist |
| X6 | list_of_nat | v | natlist |
| X7 | list_of_nat | v | natlist |
| X8 | list_of_nat | v | natlist |
| X9 | list_of_nat | v | natlist |
| XornoX | partition-refinement | p | partelem × natlist × arrnat |
| arrnat | array_of_nat | s | |
| butlastn | partition | f | nat × partition → partition |
| butlastn | list_of_nat | f | nat × natlist → natlist |
| disj | list_of_nat | p | natlist × natlist |
| disj | partition | p | partition × partition |
| divides | partition-refinement | p | partition × partition × natlist × arrnat |
| dups | partition | p | partition |
| dups | list_of_nat | p | natlist |
| fillfirst | partition | f | nat × partelem × partition → partition |
| fillfirst | list_of_nat | f | nat × nat × natlist → natlist |
| firstn | partition | f | nat × partition → partition |
| firstn | list_of_nat | f | nat × natlist → natlist |
| frome | partition | f | partition × partelem → partition |
| frome | list_of_nat | f | natlist × nat → natlist |
| i | partition-refinement | v | nat |
| lastn | partition | f | nat × partition → partition |
| lastn | list_of_nat | f | nat × natlist → natlist |
| length_of_P | partition-refinement | v | nat |
| list2set | partition-refinement | f | natlist → natset |
| m | nat-basic2 | v | nat |
| m0 | partelem | v | nat |
| m1 | partelem | v | nat |
| m2 | partelem | v | nat |
| m3 | partelem | v | nat |
| m4 | partelem | v | nat |
| mapnatnat | map_nat_nat | s | |
| mkarray | array_of_nat | f | nat → arrnat |
| mklist | partition | f | partelem × nat → partition |
| mklist | list_of_nat | f | nat × nat → natlist |
| n | nat-basic1 | v | nat |
| n0 | nat-basic1 | v | nat |
| n1 | nat-basic1 | v | nat |
| n2 | array_of_nat | v | nat |
| n3 | array_of_nat | v | nat |
| n4 | array_of_nat | v | nat |
| n5 | map_nat_nat | v | nat |
| n6 | map_nat_nat | v | nat |
| n7 | map_nat_nat | v | nat |
| n8 | map_nat_nat | v | nat |
| n9 | map_nat_nat | v | nat |
| nat | nat-basic1 | s | |
| natlist | list_of_nat | s | |
| natnat | map_nat_nat | s | |
| natset | set_of_nat | s | |
| nn | map_nat_nat | v | natnat |
| nodups | partition-refinement | p | arrnat |
| okp | partition-refinement | p | partelem × nat |
| p | partelem | v | partelem |
| p0 | partition | v | partelem |
| p1 | partition | v | partelem |
| p2 | partition | v | partelem |
| partelem | partelem | s | |
| partelem-sem | partition-refinement | v | arrnat → natset |
| partition | partition | s | |
| partitionRefinement | partition-refinement | p | partition × arrnat × partition × arrnat × natlist |
| partitions | partition-refinement | p | partition × nat |
| pe | partelem | f | nat × nat × nat → partelem |
| perm | array_of_nat | p | arrnat × arrnat |
| pos | partition | f | partelem × partition → nat |
| pos | list_of_nat | f | nat × natlist → nat |
| resetcnt | partition-refinement | f | partition → partition |
| restn | partition | f | nat × partition → partition |
| restn | list_of_nat | f | nat × natlist → natlist |
| rev | partition | f | partition → partition |
| rev | list_of_nat | f | natlist → natlist |
| rmdup | partition | f | partition → partition |
| rmdup | list_of_nat | f | natlist → natlist |
| samepartitions | partition-refinement | p | partition × arrnat × partition × arrnat |
| split | partition-refinement | p | partition × arrnat × natlist |
| splitone | partition-refinement | p | partelem × arrnat × natlist |
| startorfin | partition-refinement | p | partelem × partition |
| sublist | partition | f | nat × nat × partition → partition |
| sublist | list_of_nat | f | nat × nat × natlist → natlist |
| x | partition-refinement | v | nat |