| symbol | specification | entry |
|---|
| # | set-basic | function,
set → nat |
| # | array | function,
array → nat |
| # | key-index-array | function,
key-array → nat |
| % | nat-div | partial function,
nat × nat → nat |
| * | nat-mult | function,
nat × nat → nat |
| + | nat-basic | function,
nat × nat → nat |
| ++ | set-basic | function,
set × elem → set |
| ++ | keyindex-set | function,
set × keyindex → set |
| +1 | nat-basic | function,
nat → nat |
| - | nat | partial function,
nat × nat → nat |
| -- | set-union | function,
set × elem → set |
| -- | keyindex-set | function,
set × keyindex → set |
| -1 | nat-basic | partial function,
nat → nat |
| .ar | bin-min-heap | function,
binheap → key-array |
| .ar:= | bin-min-heap | function,
binheap × key-array → binheap |
| .elem | elem-index | function,
elem-index → elem |
| .elem:= | elem-index | function,
elem-index × elem → elem-index |
| .idx | elem-index | function,
elem-index → nat |
| .idx | key-index | function,
keyindex → nat |
| .idx:= | elem-index | function,
elem-index × nat → elem-index |
| .idx:= | key-index | function,
keyindex × nat → keyindex |
| .key | key-index | function,
keyindex → key |
| .key:= | key-index | function,
keyindex × key → keyindex |
| .size | bin-min-heap | function,
binheap → nat |
| .size:= | bin-min-heap | function,
binheap × nat → binheap |
| / | nat-div | partial function,
nat × nat → nat |
| 2^ | nat-pot | function,
nat → nat |
| 2exp-size | bin-min-heap-inv | predicate,
nat |
| < | oelem | predicate,
elem × elem |
| < | binheap-key | predicate,
key × key |
| < | nat-basic | predicate,
nat × nat |
| > | nat | predicate,
nat × nat |
| \ | set-union | function,
set × set → set |
| ] | array | partial function,
array × nat × elem → array |
| ] | array | partial function,
array × nat → elem |
| ] | key-index-array | partial function,
key-array × nat × keyindex → key-array |
| ] | key-index-array | partial function,
key-array × nat → keyindex |
| ] | index-array-base | partial function,
array × nat × elem-index → array |
| ] | index-array-base | partial function,
array × nat → elem-index |
| ^ | nat-pot | function,
nat × nat → nat |
| a | elem | variable,
elem |
| a0 | elem-index | variable,
elem |
| ar | array | variable,
array |
| ar0 | array | variable,
array |
| ar1 | array | variable,
array |
| ar2 | array | variable,
array |
| array | array | sort,
|
| b | elem | variable,
elem |
| bh | bin-min-heap | variable,
binheap |
| bh0 | bin-min-heap | variable,
binheap |
| bin-heap | bin-min-heap | function,
key-array × nat → binheap |
| bin-heap-inv | bin-min-heap-prepost | predicate,
binheap × array |
| bin_min_heap_bubble_down# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_bubble_up# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_empty# | bin-min-heap-ops | procedure,
: binheap |
| bin_min_heap_extract_min# | bin-min-heap-ops | procedure,
: binheap × array × nat |
| bin_min_heap_get_min# | bin-min-heap-ops | procedure,
binheap : nat |
| bin_min_heap_insert# | bin-min-heap-ops | procedure,
keyindex : binheap × array |
| bin_min_heap_is_empty# | bin-min-heap-ops | procedure,
binheap : bool |
| bin_min_heap_next_2pot | bin-min-heap-ops | procedure,
nat : nat |
| bin_min_heap_remove# | bin-min-heap-ops | procedure,
nat : binheap × array |
| bin_min_heap_resize# | bin-min-heap-ops | procedure,
nat : binheap |
| bin_min_heap_update# | bin-min-heap-ops | procedure,
nat × key : binheap × array |
| binheap | bin-min-heap | sort,
|
| bubble-down-inv | bin-min-heap-prepost | predicate,
nat × binheap × array × binheap × array |
| bubble-up-inv | bin-min-heap-prepost | predicate,
nat × binheap × array × binheap × array |
| c | elem | variable,
elem |
| cmp | key-index-array | partial predicate,
key-array × keyindex × nat × nat |
| cmp | key-index-array | partial predicate,
key-array × nat × key-array × nat × nat |
| cmp | index-array-base | partial predicate,
array × elem-index × nat × nat |
| cmp | array-copy | partial predicate,
array × elem × nat × nat |
| cmp | array-copy | partial predicate,
array × nat × array × nat × nat |
| copy | key-index-array | partial function,
key-array × nat × key-array × nat × nat → key-array |
| copy | array-copy | partial function,
array × nat × array × nat × nat → array |
| ei | elem-index | variable,
elem-index |
| ei0 | index-array-base | variable,
elem-index |
| ei1 | index-array-base | variable,
elem-index |
| elem | elem | sort,
|
| elem-index | elem-index | sort,
|
| elemindex | elem-index | function,
elem × nat → elem-index |
| fill | key-index-array | partial function,
key-array × keyindex × nat × nat → key-array |
| fill | key-index-array | function,
key-array × keyindex → key-array |
| fill | index-array-base | partial function,
array × elem-index × nat × nat → array |
| fill | index-array-base | function,
array × elem-index → array |
| fill | array-copy | partial function,
array × elem × nat × nat → array |
| fill | array-copy | function,
array × elem → array |
| heap-order | bin-min-heap-inv | predicate,
key-array × nat |
| id-idx | index-array | predicate,
array × array |
| idrange | key-index-array | partial predicate,
key-array × nat × nat |
| idrange | array-copy | partial predicate,
array × nat × nat |
| id○ | key-index-array | predicate,
key-array × key-array × nat |
| id○ | array-copy | predicate,
array × array × nat |
| isempty | bin-min-heap-ops | variable,
bool |
| kar | key-index-array | variable,
key-array |
| kar0 | key-index-array | variable,
key-array |
| kar1 | key-index-array | variable,
key-array |
| kar2 | key-index-array | variable,
key-array |
| key | binheap-key | variable,
key |
| key | binheap-key | sort,
|
| key-array | key-index-array | sort,
|
| key-index | key-index | function,
key × nat → keyindex |
| key0 | binheap-key | variable,
key |
| key1 | binheap-key | variable,
key |
| keyindex | key-index | sort,
|
| keyset | bin-min-heap-inv | function,
key-array × nat → set |
| keyset | bin-min-heap-prepost | function,
binheap → set |
| ki | key-index | variable,
keyindex |
| ki0 | keyindex-set | variable,
keyindex |
| ki0 | key-index-array | variable,
keyindex |
| ki1 | keyindex-set | variable,
keyindex |
| ki1 | key-index-array | variable,
keyindex |
| log | nat-pot | partial function,
nat × nat → nat |
| log2 | nat-pot | partial function,
nat → nat |
| m | nat-basic | variable,
nat |
| m0 | nat-pot | variable,
nat |
| m0 | elem-index | variable,
nat |
| m0 | key-index | variable,
nat |
| m0 | array-copy | variable,
nat |
| m1 | bin-min-heap-inv | variable,
nat |
| minsize | bin-min-heap-ops | variable,
nat |
| mkarray | array | function,
nat → array |
| mkkeyarray | key-index-array | function,
nat → key-array |
| n | nat-basic | variable,
nat |
| n0 | nat-basic | variable,
nat |
| n1 | nat-basic | variable,
nat |
| nat | nat-basic | sort,
|
| no-dups | bin-min-heap-inv | predicate,
key-array × nat |
| no-dups-idx | bin-min-heap-inv | predicate,
key-array × nat |
| rev | key-index-array | partial function,
key-array × nat → key-array |
| rev | key-index-array | function,
key-array → key-array |
| rev | array-copy | partial function,
array × nat → array |
| rev | array-copy | function,
array → array |
| s | set-basic | variable,
set |
| s0 | set-basic | variable,
set |
| s1 | set-basic | variable,
set |
| s2 | set-basic | variable,
set |
| set | set-basic | sort,
|
| subarray | key-index-array | partial function,
key-array × nat × nat → key-array |
| subarray | array-copy | partial function,
array × nat × nat → array |
| valid-idx | bin-min-heap-inv | predicate,
key-array × array × nat |
| } | set-union | function,
elem → set |
| } | keyindex-set | function,
keyindex → set |
| ∅ | set-basic | constant,
set |
| ∈ | set-basic | predicate,
elem × set |
| ∈ | keyindex-set | predicate,
keyindex × set |
| ∈ | key-index-array | predicate,
keyindex × key-array |
| ∈ | index-array-base | predicate,
elem-index × array |
| ∈ | array-copy | predicate,
elem × array |
| ∩ | 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 |