[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
# .	bag-union	f	bag → nat
# .	array	f	array → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	bag-basic	f	bag × elem → bag
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	bag-union	f	bag × elem → bag
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. < .	oelem	p	elem × elem
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. [ . ]	array	pf	array × nat → elem with λ ar, n. n < # ar
. \ .	bag-union	f	bag × bag → bag
. ∈ .	bag-union	p	elem × bag
. ∈ .	array-copy	p	elem × array
. ∪ .	bag-union	f	bag × bag → bag
. ≤ .	oarray-sorted	p	elem × elem
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	bag-union	p	bag × bag
{ . }	bag-union	f	elem → bag
∅	bag-basic	c	bag
A	oarray-sorted	v	array
A0	oarray-sorted	v	array
Inv-end	sort-invariants	p	array × array × nat × nat × elem
Inv-first-inner	sort-invariants	p	array × array × elem × elem × nat × nat
Inv-last-inner	sort-invariants	p	array × array × elem × elem × nat × nat
Inv-main	sort-invariants	p	array × array × nat
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
bag	bag-basic	s
bag	bag-basic	v	bag
bag0	bag-basic	v	bag
bag1	bag-basic	v	bag
bag2	bag-basic	v	bag
c	elem	v	elem
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	p	array × elem
copy	array-copy	pf	array × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
count	bag-basic	f	elem × bag → nat
elem	elem	s
fill	array-copy	f	array × elem → array
fill	array-copy	pf	array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
i	oarray-sorted	v	nat
i0	oarray-sorted	v	nat
id○	array-copy	p	array × array × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
j	oarray-sorted	v	nat
m	nat-basic	v	nat
m0	array-copy	v	nat
mkarray	array	f	nat → array
mkbag	oarray-perm	pf	array × nat → bag with λ A, n. n ≤ # A
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
perm	oarray-perm	p	array × array
rev	array-copy	pf	array × nat → array with λ ar, n. n ≤ # ar
rev	array-copy	f	array → array
sorted	oarray-sorted	p	array × nat × nat
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar
x	oarray-sorted	v	elem
y	oarray-sorted	v	elem