| Symbol | Specification | Kind | Type |
|---|
| # . | key-index-array | f | key-array → nat |
| . % . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . * . | nat-mult | f | nat × nat → nat |
| . + . | nat-basic | f | nat × nat → nat |
| . +1 | nat-basic | f | nat → nat |
| . - . | nat | pf | nat × nat → nat with λ n, m. n ≥ m |
| . -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 |
| . .idx | key-index | f | keyindex → nat |
| . .idx:= . | key-index | f | keyindex × nat → keyindex |
| . .key | key-index | f | keyindex → key |
| . .key:= . | key-index | f | keyindex × key → keyindex |
| . .size | bin-min-heap | f | binheap → nat |
| . .size:= . | bin-min-heap | f | binheap × nat → binheap |
| . / . | nat-div | pf | nat × nat → nat with λ n, m. m ≠ 0 |
| . < . | binheap-key | p | key × key |
| . < . | nat-basic | p | nat × nat |
| . > . | nat | p | nat × nat |
| . [ . ] | 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 |
| . ^ . | nat-pot | f | nat × nat → nat |
| . ∈ . | key-index-array | p | keyindex × key-array |
| . ≤ . | nat | p | nat × nat |
| . ≥ . | nat | p | nat × nat |
| 2^ . | nat-pot | f | nat → nat |
| bh | bin-min-heap | v | binheap |
| bh0 | bin-min-heap | v | binheap |
| bin-heap | bin-min-heap | f | key-array × nat → binheap |
| binheap | bin-min-heap | s | |
| 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 |
| fill | key-index-array | f | key-array × keyindex → key-array |
| fill | key-index-array | pf | key-array × keyindex × nat × nat → key-array with λ kar, ki, n, m. n + m ≤ # kar |
| id○ | key-index-array | p | key-array × key-array × nat |
| 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 | binheap-key | s | |
| key | binheap-key | v | key |
| key-array | key-index-array | s | |
| key-index | key-index | f | key × nat → keyindex |
| key0 | binheap-key | v | key |
| key1 | binheap-key | v | key |
| keyindex | key-index | s | |
| ki | key-index | v | keyindex |
| ki0 | key-index-array | v | keyindex |
| ki1 | key-index-array | v | keyindex |
| log | nat-pot | pf | nat × nat → nat with λ m, m0. m0 ≠ 0 |
| log2 . | nat-pot | pf | nat → nat with λ m0. m0 ≠ 0 |
| m | nat-basic | v | nat |
| m0 | nat-pot | v | nat |
| mkkeyarray | key-index-array | f | nat → key-array |
| n | nat-basic | v | nat |
| n0 | nat-basic | v | nat |
| n1 | nat-basic | v | nat |
| nat | nat-basic | s | |
| rev | key-index-array | pf | key-array × nat → key-array with λ kar, n. n ≤ # kar |
| rev | key-index-array | f | key-array → key-array |
| subarray | key-index-array | pf | key-array × nat × nat → key-array with λ kar, m, n. m + n ≤ # kar |