[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol Specification Kind Type
# .key-index-arrayfkey-array → nat
# .set-basicfset → nat
# .arrayfarray → nat
. % .nat-divpfnat × nat → nat with λ n, m. m ≠ 0
. * .nat-multfnat × nat → nat
. + .nat-basicfnat × nat → nat
. ++ .keyindex-setfset × keyindex → set
. +1nat-basicfnat → nat
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -- .keyindex-setfset × keyindex → set
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. .arbin-min-heapfbinheap → key-array
. .ar:= .bin-min-heapfbinheap × key-array → binheap
. .elemelem-indexfelem-index → elem
. .elem:= .elem-indexfelem-index × elem → elem-index
. .idxkey-indexfkeyindex → nat
. .idxelem-indexfelem-index → nat
. .idx:= .elem-indexfelem-index × nat → elem-index
. .idx:= .key-indexfkeyindex × nat → keyindex
. .keykey-indexfkeyindex → key
. .key:= .key-indexfkeyindex × key → keyindex
. .sizebin-min-heapfbinheap → nat
. .size:= .bin-min-heapfbinheap × nat → binheap
. / .nat-divpfnat × nat → nat with λ n, m. m ≠ 0
. < .binheap-keypkey × key
. < .nat-basicpnat × nat
. > .natpnat × nat
. [ . ]index-array-basepfarray × nat × elem-index → array with λ ar, n, ei. n < # ar
. [ . ]index-array-basepfarray × nat → elem-index with λ ar, n. n < # ar
. [ . ]key-index-arraypfkey-array × nat × keyindex → key-array with λ kar, n, ki. n < # kar
. [ . ]key-index-arraypfkey-array × nat → keyindex with λ kar, n. n < # kar
. \ .set-unionfset × set → set
. ^ .nat-potfnat × nat → nat
. ∈ .keyindex-setpkeyindex × set
. ∈ .index-array-basepelem-index × array
. ∈ .key-index-arraypkeyindex × key-array
. ∩ .set-unionfset × set → set
. ∪ .set-unionfset × set → set
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .set-basicpset × set
{ . }keyindex-setfkeyindex → set
∅set-basiccset
2^ .nat-potfnat → nat
2exp-sizebin-min-heap-invpnat
aelemvelem
a0elem-indexvelem
ararrayvarray
ar0arrayvarray
ar1arrayvarray
ar2arrayvarray
arrayarrays
belemvelem
bhbin-min-heapvbinheap
bh0bin-min-heapvbinheap
bin-heapbin-min-heapfkey-array × nat → binheap
bin-heap-invbin-min-heap-prepostpbinheap × array
bin_min_heap_bubble_down#bin-min-heap-opsprnat : binheap × array (nonfunctional)
bin_min_heap_bubble_up#bin-min-heap-opsprnat : binheap × array (nonfunctional)
bin_min_heap_empty#bin-min-heap-opspr : binheap
bin_min_heap_extract_min#bin-min-heap-opspr : binheap × array × nat (nondeterministic nonfunctional)
bin_min_heap_get_min#bin-min-heap-opsprbinheap : nat (nondeterministic)
bin_min_heap_insert#bin-min-heap-opsprkeyindex : binheap × array (nonfunctional)
bin_min_heap_is_empty#bin-min-heap-opsprbinheap : bool
bin_min_heap_next_2potbin-min-heap-opsprnat : nat (nonfunctional)
bin_min_heap_remove#bin-min-heap-opsprnat : binheap × array (nonfunctional)
bin_min_heap_resize#bin-min-heap-opsprnat : binheap (nonfunctional)
bin_min_heap_update#bin-min-heap-opsprnat × key : binheap × array (nonfunctional)
binheapbin-min-heaps
bubble-down-invbin-min-heap-prepostpnat × binheap × array × binheap × array
bubble-up-invbin-min-heap-prepostpnat × binheap × array × binheap × array
celemvelem
cmpindex-array-basepparray × elem-index × nat × nat with λ ar, ei, m, n. m + n ≤ # ar
cmparray-copypparray × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmpkey-index-arrayppkey-array × keyindex × nat × nat with λ kar, ki, m, n. m + n ≤ # kar
cmpkey-index-arrayppkey-array × nat × key-array × nat × nat with λ kar, m, kar0, m0, n. m + n ≤ # kar ∧ m0 + n ≤ # kar0
copykey-index-arraypfkey-array × nat × key-array × nat × nat → key-array with λ kar, m, kar0, m0, n. m + n ≤ # kar ∧ m0 + n ≤ # kar0
copyarray-copypfarray × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
eielem-indexvelem-index
ei0index-array-basevelem-index
ei1index-array-basevelem-index
elemelems
elem-indexelem-indexs
elemindexelem-indexfelem × nat → elem-index
fillindex-array-basepfarray × elem-index × nat × nat → array with λ ar, ei, n, m. n + m ≤ # ar
fillkey-index-arrayfkey-array × keyindex → key-array
fillkey-index-arraypfkey-array × keyindex × nat × nat → key-array with λ kar, ki, n, m. n + m ≤ # kar
fillindex-array-basefarray × elem-index → array
heap-orderbin-min-heap-invpkey-array × nat
id-idxindex-arrayparray × array
id○key-index-arraypkey-array × key-array × nat
id○array-copyparray × array × nat
idrangearray-copypparray × nat × nat with λ ar, m, n. m + n ≤ # ar
idrangekey-index-arrayppkey-array × nat × nat with λ kar, m, n. m + n ≤ # kar
isemptybin-min-heap-opsvbool
karkey-index-arrayvkey-array
kar0key-index-arrayvkey-array
kar1key-index-arrayvkey-array
kar2key-index-arrayvkey-array
keybinheap-keys
keybinheap-keyvkey
key-arraykey-index-arrays
key-indexkey-indexfkey × nat → keyindex
key0binheap-keyvkey
key1binheap-keyvkey
keyindexkey-indexs
keysetbin-min-heap-invfkey-array × nat → set
keysetbin-min-heap-prepostfbinheap → set
kikey-indexvkeyindex
ki0keyindex-setvkeyindex
ki1keyindex-setvkeyindex
lognat-potpfnat × nat → nat with λ m, m0. m0 ≠ 0
log2 .nat-potpfnat → nat with λ m0. m0 ≠ 0
mnat-basicvnat
m0nat-potvnat
m1bin-min-heap-invvnat
minsizebin-min-heap-opsvnat
mkarrayarrayfnat → array
mkkeyarraykey-index-arrayfnat → key-array
nnat-basicvnat
n0nat-basicvnat
n1nat-basicvnat
natnat-basics
no-dupsbin-min-heap-invpkey-array × nat
no-dups-idxbin-min-heap-invpkey-array × nat
revarray-copypfarray × nat → array with λ ar, n. n ≤ # ar
revkey-index-arraypfkey-array × nat → key-array with λ kar, n. n ≤ # kar
revkey-index-arrayfkey-array → key-array
revarray-copyfarray → array
sset-basicvset
s0set-basicvset
s1set-basicvset
s2set-basicvset
setset-basics
subarrayarray-copypfarray × nat × nat → array with λ ar, m, n. m + n ≤ # ar
subarraykey-index-arraypfkey-array × nat × nat → key-array with λ kar, m, n. m + n ≤ # kar
valid-idxbin-min-heap-invpkey-array × array × nat