| Symbol | Specification | Kind | Type |
|---|
| # . | key-index-array | f | key-array → nat |
| # . | gc-heap-base | f | lp-array → nat |
| # . | gc-heap-rename | f | gc-heap-set → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . ++ . | gc-heap-rename | f | gc-heap-set × keyindex → gc-heap-set |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -- . | gc-heap-rename | f | gc-heap-set × keyindex → gc-heap-set |
| . -1 | nat-basic | pf | nat → nat with λ n. n ≠ 0 |
| . .ar | bin-min-heap | f | binheap → key-array |
| . .ar:= . | bin-min-heap | f | binheap × key-array → binheap |
| . .flags | lprops | f | lprops → lpropflags |
| . .flags:= . | lprops | f | lprops × lpropflags → lprops |
| . .gcheapidx | lprops | f | lprops → nat |
| . .gcheapidx:= . | lprops | f | lprops × nat → lprops |
| . .idx | key-index | f | keyindex → nat |
| . .idx:= . | key-index | f | keyindex × nat → keyindex |
| . .key | gc-heap-base | f | keyindex → nat |
| . .key:= . | gc-heap-base | f | keyindex × nat → keyindex |
| . .ref-size | lprops | f | lprops → nat |
| . .ref-size:= . | lprops | f | lprops × nat → lprops |
| . .size | bin-min-heap | f | binheap → nat |
| . .size | lprops | f | lprops → nat |
| . .size:= . | lprops | f | lprops × nat → lprops |
| . .size:= . | bin-min-heap | f | binheap × nat → binheap |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | gc-heap-base | pf | lp-array × nat × lprops → lp-array with λ lpt, n, lp. n < # lpt |
| . [ . ] | gc-heap-base | pf | lp-array × nat → lprops with λ lpt, n. n < # lpt |
| . [ . ] | key-index-array | pf | key-array × nat × keyindex → key-array with λ kar, n, ki. n < # kar |
| . [ . ] | key-index-array | pf | key-array × nat → keyindex with λ kar, n. n < # kar |
| . \ . | gc-heap-rename | f | gc-heap-set × gc-heap-set → gc-heap-set |
| . ^ . | nat-pot | f | nat × nat → nat |
| . ∈ . | gc-heap-rename | p | keyindex × gc-heap-set |
| . ∈ . | gc-heap-base | p | lprops × lp-array |
| . ∈ . | key-index-array | p | keyindex × key-array |
| . ∩ . | gc-heap-rename | f | gc-heap-set × gc-heap-set → gc-heap-set |
| . ∪ . | gc-heap-rename | f | gc-heap-set × gc-heap-set → gc-heap-set |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| . ⊆ . | gc-heap-rename | p | gc-heap-set × gc-heap-set |
| { . } | gc-heap-rename | f | keyindex → gc-heap-set |
| ∅ | gc-heap-rename | c | gc-heap-set |
| 2^ . | nat-pot | f | nat → nat |
| 2exp-size | bin-min-heap-inv | p | nat |
| Boolvar | gc-heap-base | v | bool,flexible |
| LP_FREE | lprops | c | lpropflags |
| LP_GROUP_NODES | lprops | c | lpropflags |
| LP_INDEX_NODES | lprops | c | lpropflags |
| Plprops | gc-heap-base | v | lprops → bool |
| bh | bin-min-heap | v | binheap |
| bh0 | bin-min-heap | v | binheap |
| bin-heap | bin-min-heap | f | key-array × nat → binheap |
| bin-heap-inv | gc-heap-base | p | binheap × lp-array |
| bin_min_heap_bubble_down# | gc-heap-base | pr | nat : binheap × lp-array (nonfunctional) |
| bin_min_heap_bubble_up# | gc-heap-base | pr | nat : binheap × lp-array (nonfunctional) |
| bin_min_heap_next_2pot | bin-min-heap-ops | pr | nat : nat (nonfunctional) |
| bin_min_heap_resize# | bin-min-heap-ops | pr | nat : binheap (nonfunctional) |
| binheap | bin-min-heap | s | |
| boolvar | gc-heap-base | v | bool |
| boolvar0 | gc-heap-base | v | bool |
| boolvar1 | gc-heap-base | v | bool |
| bubble-down-inv | gc-heap-base | p | nat × binheap × lp-array × binheap × lp-array |
| bubble-up-inv | gc-heap-base | p | nat × binheap × lp-array × binheap × lp-array |
| cmp | gc-heap-base | pp | lp-array × lprops × nat × nat with λ lpt, lp, m, n. m + n ≤ # lpt |
| cmp | gc-heap-base | pp | lp-array × nat × lp-array × nat × nat with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0 |
| cmp | key-index-array | pp | key-array × keyindex × nat × nat with λ kar, ki, m, n. m + n ≤ # kar |
| cmp | key-index-array | pp | key-array × nat × key-array × nat × nat with λ kar, m, kar0, m0, n. m + n ≤ # kar ∧ m0 + n ≤ # kar0 |
| copy | key-index-array | pf | key-array × nat × key-array × nat × nat → key-array with λ kar, m, kar0, m0, n. m + n ≤ # kar ∧ m0 + n ≤ # kar0 |
| copy | gc-heap-base | pf | lp-array × nat × lp-array × nat × nat → lp-array with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0 |
| empty? | gc-heap-rename | v | bool |
| fill | key-index-array | f | key-array × keyindex → key-array |
| fill | gc-heap-base | pf | lp-array × lprops × nat × nat → lp-array with λ lpt, lp, n, m. n + m ≤ # lpt |
| fill | gc-heap-base | f | lp-array × lprops → lp-array |
| fill | key-index-array | pf | key-array × keyindex × nat × nat → key-array with λ kar, ki, n, m. n + m ≤ # kar |
| gc-heap-set | gc-heap-rename | s | |
| gc_heap_empty# | gc-heap-rename | pr | : binheap |
| gc_heap_extract_min# | gc-heap-rename | pr | : binheap × lp-array × nat (nondeterministic nonfunctional) |
| gc_heap_get_min# | gc-heap-rename | pr | binheap : nat (nondeterministic) |
| gc_heap_insert# | gc-heap-rename | pr | keyindex : binheap × lp-array (nonfunctional) |
| gc_heap_is_empty# | gc-heap-rename | pr | binheap : bool |
| gc_heap_remove# | gc-heap-rename | pr | nat : binheap × lp-array (nonfunctional) |
| gc_heap_update# | gc-heap-rename | pr | nat × nat : binheap × lp-array (nonfunctional) |
| gchs | gc-heap-rename | v | gc-heap-set |
| gchs0 | gc-heap-rename | v | gc-heap-set |
| gchs1 | gc-heap-rename | v | gc-heap-set |
| gchs2 | gc-heap-rename | v | gc-heap-set |
| heap-order | bin-min-heap-inv | p | key-array × nat |
| id-idx | gc-heap-base | p | lp-array × lp-array |
| id○ | key-index-array | p | key-array × key-array × nat |
| id○ | gc-heap-base | p | lp-array × lp-array × nat |
| idrange | gc-heap-base | pp | lp-array × nat × nat with λ lpt, m, n. m + n ≤ # lpt |
| idrange | key-index-array | pp | key-array × nat × nat with λ kar, m, n. m + n ≤ # kar |
| kar | key-index-array | v | key-array |
| kar0 | key-index-array | v | key-array |
| kar1 | key-index-array | v | key-array |
| kar2 | key-index-array | v | key-array |
| key-array | key-index-array | s | |
| key-index | gc-heap-base | f | nat × nat → keyindex |
| keyindex | key-index | s | |
| keyset | gc-heap-rename | f | key-array × nat → gc-heap-set |
| keyset | gc-heap-rename | f | binheap → gc-heap-set |
| ki | key-index | v | keyindex |
| ki0 | keyindex-set | v | keyindex |
| ki1 | keyindex-set | v | keyindex |
| logarithm | gc-heap-rename | pf | nat × nat → nat with λ m, m0. m0 ≠ 0 |
| logarithm2 . | gc-heap-rename | pf | nat → nat with λ m0. m0 ≠ 0 |
| lp | lprops | v | lprops |
| lp-array | gc-heap-base | s | |
| lp0 | lprops | v | lprops |
| lp2 | gc-heap-base | v | lprops |
| lp3 | gc-heap-base | v | lprops |
| lpf | lprops | v | lpropflags |
| lpf0 | lprops | v | lpropflags |
| lpf1 | gc-heap-base | v | lpropflags |
| lpf2 | gc-heap-base | v | lpropflags |
| lpropflags | lprops | s | |
| lprops | lprops | s | |
| lpt | gc-heap-base | v | lp-array |
| lpt0 | gc-heap-base | v | lp-array |
| lpt1 | gc-heap-base | v | lp-array |
| lpt2 | gc-heap-base | v | lp-array |
| m | nat-basic | v | nat |
| m0 | elem-index | v | nat |
| m1 | lprops | v | nat |
| m2 | lprops | v | nat |
| m3 | lprops | v | nat |
| m4 | lprops | v | nat |
| minsize | bin-min-heap-ops | v | nat |
| mkkeyarray | key-index-array | f | nat → key-array |
| mklp | lprops | f | nat × nat × lpropflags × nat → lprops |
| mklparray | gc-heap-base | f | nat → lp-array |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| n2 | gc-heap-base | v | nat |
| n3 | gc-heap-base | v | nat |
| n4 | gc-heap-base | v | nat |
| n5 | gc-heap-base | v | nat |
| n6 | gc-heap-base | v | nat |
| n7 | gc-heap-base | v | nat |
| n8 | gc-heap-base | v | nat |
| n9 | gc-heap-base | v | nat |
| nat | nat-basic | s | |
| natkey | gc-heap-rename | v | nat |
| natkey0 | gc-heap-rename | v | nat |
| natkey1 | gc-heap-rename | v | nat |
| no-dups | bin-min-heap-inv | p | key-array × nat |
| no-dups-idx | bin-min-heap-inv | p | key-array × nat |
| rev | gc-heap-base | pf | lp-array × nat → lp-array with λ lpt, n. n ≤ # lpt |
| rev | key-index-array | f | key-array → key-array |
| rev | gc-heap-base | f | lp-array → lp-array |
| rev | key-index-array | pf | key-array × nat → key-array with λ kar, n. n ≤ # kar |
| subarray | gc-heap-base | pf | lp-array × nat × nat → lp-array with λ lpt, m, n. m + n ≤ # lpt |
| subarray | key-index-array | pf | key-array × nat × nat → key-array with λ kar, m, n. m + n ≤ # kar |
| valid-idx | gc-heap-base | p | key-array × lp-array × nat |