[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
# .	list-of-natarray	f	list-of-natarray → nat
# .	array-set	f	array-set → nat
#oc	natarray	f	nat × array → nat
. '	natarray	f	nat → array
. '	list-of-natarray	f	array → list-of-natarray
. + .	nat-basic	f	nat × nat → nat
. + .	list-as-arrayinstance	f	array × array → array
. + .	natarray	f	array × nat → array
. + .	natarray	f	nat × array → array
. + .	list-of-natarray	f	array × list-of-natarray → list-of-natarray
. + .	list-of-natarray	f	list-of-natarray × list-of-natarray → list-of-natarray
. + .	list-of-natarray	f	list-of-natarray × array → list-of-natarray
. ++ .	natarray	f	array × nat → array
. ++ .	list-of-natarray	f	list-of-natarray × array → list-of-natarray
. ++ .	array-set	f	array-set × array → array-set
. +1	nat-basic	f	nat → nat
. +2 .	natarray	f	nat × nat → array
. +2 .	list-of-natarray	f	array × array → list-of-natarray
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	array-set	f	array-set × array → array-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	natarray	f	array × nat → array
. -l .	natarray	f	array × nat → array
. -p .	list-as-arrayinstance	f	array × nat → array
. .butlast	list-as-arrayinstance	pf	array → array with λ x. x ≠ []
. .butlast	list-of-natarray	pf	list-of-natarray → list-of-natarray with λ x. x ≠ []
. .first	natarray	pf	array → nat with λ ar. ar ≠ []
. .head	list-of-natarray	pf	list-of-natarray → array with λ x. x ≠ []
. .last	natarray	pf	array → nat with λ x. x ≠ []
. .last	list-of-natarray	pf	list-of-natarray → array with λ x. x ≠ []
. .rest	array-listops	pf	array → array with λ ar. ar ≠ []
. .tail	list-of-natarray	pf	list-of-natarray → list-of-natarray with λ x. x ≠ []
. .toSet	challenge1	f	list-of-natarray → array-set
. < .	nat-basic	p	nat × nat
. < .	array-listops	p	array × array
. < .	list-of-natarray	p	list-of-natarray × list-of-natarray
. > .	nat	p	nat × nat
. [ . ]	natarray	pf	array × nat → nat with λ ar, n. n < # ar
. [ . ]	natarray	pf	array × nat × nat → array with λ ar, n, a. n < # ar
. \ .	list-as-arrayinstance	f	array × array → array
. \ .	array-set	f	array-set × array-set → array-set
. ∈ .	natarray	p	nat × array
. ∈ .	list-of-natarray	p	array × list-of-natarray
. ∈ .	array-set	p	array × array-set
. ∩ .	array-set	f	array-set × array-set → array-set
. ∪ .	list-as-arrayinstance	f	array × array → array
. ∪ .	array-set	f	array-set × array-set → array-set
. ≤ .	nat	p	nat × nat
. ≤ .	challenge1	p	array × array
. ≥ .	nat	p	nat × nat
. ⊆ .	list-as-arrayinstance	p	array × array
. ⊆ .	array-set	p	array-set × array-set
. ⊆m .	list-as-arrayinstance	p	array × array
. ⊑ .	list-as-arrayinstance	p	array × array
. ⊑ .	list-of-natarray	p	list-of-natarray × list-of-natarray
. ⊒ .	list-as-arrayinstance	p	array × array
. ⊒ .	list-of-natarray	p	list-of-natarray × list-of-natarray
[]	array-listops	c	array
[]	list-of-natarray	c	list-of-natarray
{ . }	array-set	f	array → array-set
∅	array-set	c	array-set
EndIncreasingPart	challenge1	pf	array → nat with λ ar. ordered≤(ar)
PosNextGreaterElem	challenge1	pf	nat × array → nat with λ m, ar. hasGreaterElem(ar, m)
allPerms	challenge1	f	array → array-set
ar	challenge1	v	array
array	array	s
array-set	array-set	s
arx	challenge1	v	list-of-natarray
butlastn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
butlastn	list-of-natarray	pf	nat × list-of-natarray → list-of-natarray with λ n, x. n ≤ # x
cmp	natarray	p	array × nat
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	natarray	pp	array × nat × 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
disj	list-as-arrayinstance	p	array × array
disj	list-of-natarray	p	list-of-natarray × list-of-natarray
dups	list-as-arrayinstance	p	array
dups	list-of-natarray	p	list-of-natarray
fill	natarray	f	array × nat → array
fill	natarray	pf	array × nat × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fillfirst	natarray	f	nat × nat × array → array
fillfirst	list-of-natarray	f	nat × array × list-of-natarray → list-of-natarray
filter	list-as-arrayinstance	f	array × array → array
firstn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
frome	natarray	f	array × nat → array
greaterPerms	challenge1	f	array → array-set
hasGreaterElem	challenge1	p	array × nat
hasNext	challenge1	v	bool
i	challenge1	v	nat
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≤	natarray	f	nat × array → array
j	challenge1	v	nat
lastn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
list-of-natarray	list-of-natarray	s
listofar	challenge1	v	list-of-natarray
m	challenge1	v	nat
max	challenge1	p	array
merge	oarray-sort	f	array × array → array
min	challenge1	p	array
mkarray	array	f	nat → array
mklist	natarray	f	nat × nat → array
mklist	list-of-natarray	f	array × nat → list-of-natarray
n	challenge1	v	nat
nat	nat-basic	s
next#	challenge1	pr	: array : bool
nextperm	challenge1	p	array × array
ordered<	oarray-sort	p	array
ordered≤	oarray-sort	p	array
ordered≤	challenge1	p	list-of-natarray
perm	list-as-arrayinstance	p	array × array
permut#	challenge1	pr	: array × list-of-natarray
pos	natarray	f	nat × array → nat
restn	list-as-arrayinstance	pf	nat × array → array with λ n, x. n ≤ # x
rev	list-as-arrayinstance	f	array → array
rev	list-of-natarray	f	list-of-natarray → list-of-natarray
rmdup	list-as-arrayinstance	f	array → array
rmdup	list-of-natarray	f	list-of-natarray → list-of-natarray
smallerPerms	challenge1	f	array → array-set
sort#	challenge1	pr	: array
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
temp	challenge1	v	nat