[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
# .	array	f	array → nat
#c .	matrix	f	matrix → nat
#clean0rows	ShearSort	f	matrix × elem → nat
#clean1rows	ShearSort	f	matrix × elem → nat
#dirtyrows	ShearSort	f	matrix × elem → nat
#oc	list-as-arrayinstance	f	elem × array → nat
#r .	matrix	f	matrix → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	list-as-arrayinstance	f	elem → array
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	list-as-arrayinstance	f	array × array → array
. + .	list-as-arrayinstance	f	array × elem → array
. + .	array-listops	f	elem × array → array
. ++ .	list-as-arrayinstance	f	array × elem → array
. +1	nat-basic	f	nat → nat
. +2 .	list-as-arrayinstance	f	elem × elem → array
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	list-as-arrayinstance	f	array × elem → array
. -l .	list-as-arrayinstance	f	array × elem → array
. -p .	list-as-arrayinstance	f	array × nat → array
. .butlast	list-as-arrayinstance	pf	array → array with λ x. x ≠ []
. .dirtyrows≤ ( . )	ShearSort	p	matrix × nat
. .first	array-listops	pf	array → elem with λ ar. ar ≠ []
. .last	list-as-arrayinstance	pf	array → elem with λ x. x ≠ []
. .rest	array-listops	pf	array → array with λ ar. ar ≠ []
. .toArc	rowcol-upd	f	matrix → array
. .toArr	rowcol-upd	f	matrix → array
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. /↑ .	ShearSort	pf	nat × nat → nat with λ m, n. n ≠ 0
. < .	nat-basic	p	nat × nat
. < .	array-listops	p	array × array
. < .	oelem	p	elem × elem
. > .	nat	p	nat × nat
. [ . ]	matrix	pf	matrix × nat × nat → elem with λ mx, r, c. r < #r mx ∧ c < #c mx
. [ . ]	matrix	pf	matrix × nat × nat × elem → matrix with λ mx, r, c, a. r < #r mx ∧ c < #c mx
. [ . ]	array	pf	array × nat → elem with λ ar, n. n < # ar
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. [ . ]c	matrix+array	pf	matrix × nat → array with λ mx, c. c < #c mx
. [ . ]c	rowcol-upd	pf	matrix × nat × array → matrix with λ mx, c, a. c < #c mx ∧ # a = #r mx
. [ . ]r	matrix+array	pf	matrix × nat → array with λ mx, r. r < #r mx
. [ . ]r	rowcol-upd	pf	matrix × nat × array → matrix with λ mx, r, a. r < #r mx ∧ # a = #c mx
. \ .	list-as-arrayinstance	f	array × array → array
. ^ .	nat-pot	f	nat × nat → nat
. ∈ .	list-as-arrayinstance	p	elem × array
. ∪ .	list-as-arrayinstance	f	array × array → array
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	list-as-arrayinstance	p	array × array
. ⊆m .	list-as-arrayinstance	p	array × array
. ⊑ .	list-as-arrayinstance	p	array × array
. ⊒ .	list-as-arrayinstance	p	array × array
[]	array-listops	c	array
2^ .	nat-pot	f	nat → nat
a	ShearSort	v	array
array	array	s
asc	ShearSort	v	bool
bound	ShearSort	v	nat
butlastn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
c	ShearSort	v	nat
cmp	array-copy	p	array × elem
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
copy	array-copy	pf	array × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
count	oarray-sort	f	array × (elem → bool) → nat
count	oarray-sort	pf	array × nat × nat × (elem → bool) → nat with λ x, m, n, p. m ≤ n ∧ n ≤ # x
countevn	ShearSort	f	array × (elem → bool) → nat
countevn	ShearSort	pf	array × nat × nat × (elem → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a
countodd	ShearSort	f	array × (elem → bool) → nat
countodd	ShearSort	pf	array × nat × nat × (elem → bool) → nat with λ a, m, n, p. m ≤ n ∧ n ≤ # a
disj	list-as-arrayinstance	p	array × array
dups	list-as-arrayinstance	p	array
elem	elem	s
even	nat-even	p	nat
fill	array-copy	f	array × elem → array
fill	array-copy	pf	array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fillfirst	list-as-arrayinstance	f	nat × elem × array → array
filter	list-as-arrayinstance	f	array × array → array
filter	oarray-sort	f	array × (elem → bool) → array
firstn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
frome	list-as-arrayinstance	f	array × elem → array
i	ShearSort	v	elem
id○	array-copy	p	array × array × nat
id○	array-copy	p	array × array × nat × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
ins≤	oarray-sort	f	elem × array → array
j	ShearSort	v	elem
lastn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
log	nat-pot	pf	nat × nat → nat with λ m, m0. m0 ≠ 0
log2 .	nat-pot	pf	nat → nat with λ m0. m0 ≠ 0
log2↑	ShearSort	f	nat → nat
m	ShearSort	v	nat
matrix	matrix	s
max	nat-even	f	nat × nat → nat
max	oelem-min-max	f	elem × elem → elem
max	oarray-sort	pf	array → elem with λ x. x ≠ []
merge	oarray-sort	f	array × array → array
min	nat-even	f	nat × nat → nat
min	oelem-min-max	f	elem × elem → elem
min	oarray-sort	pf	array → elem with λ x. x ≠ []
mkarray	array	f	nat → array
mklist	list-as-arrayinstance	f	elem × nat → array
mkmatrix	matrix	f	nat × nat × elem → matrix
mx	ShearSort	v	matrix
n	ShearSort	v	nat
nat	nat-basic	s
odd	nat-even	p	nat
ordered<	oarray-sort	p	array
ordered≤	oarray-sort	p	array
p	ShearSort	v	elem → bool
perm	list-as-arrayinstance	p	array × array
pos	list-as-arrayinstance	f	elem × array → nat
r	ShearSort	v	nat
restn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
rev	list-as-arrayinstance	f	array → array
rmdup	list-as-arrayinstance	f	array → array
rowsincreasing	ShearSort	p	matrix × nat
scolsorted	ShearSort	p	matrix × nat × matrix
shearsort#	ShearSort	pr	: matrix (nondeterministic)
sort	oarray-sort	f	array → array
sortcol#	ShearSort	pr	nat : matrix (nondeterministic)
sortcols#	ShearSort	pr	: matrix (nondeterministic)
sortrow#	ShearSort	pr	nat × bool : matrix (nondeterministic)
sortrows#	ShearSort	pr	: matrix (nondeterministic)
sortrowssnake#	ShearSort	pr	: matrix (nondeterministic)
srowsorted	ShearSort	p	matrix × nat × matrix
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar
sublist	list-as-arrayinstance	pf	nat × nat × array → array with λ n, m, x. n + m ≤ # x
toArc	rowcol-upd	f	matrix × nat → array
toArr	rowcol-upd	f	matrix × nat → array