[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
# .	wlarray-base	f	wlarray → nat
# .	nat-list-set	f	nat-set → nat
# .	nat-list-set	f	nat-list → nat
. '	nat-list-set	f	nat → nat-list
. + .	nat-basic	f	nat × nat → nat
. + .	nat-list-set	f	nat × nat-list → nat-list
. + .	nat-list-set	f	nat-list × nat → nat-list
. + .	nat-list-set	f	nat-list × nat-list → nat-list
. ++ .	nat-list-set	f	nat-set × nat → nat-set
. ++ .	nat-list-set	f	nat-list × nat → nat-list
. +1	nat-basic	f	nat → nat
. +2 .	nat-list-set	f	nat × nat → nat-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	nat-list-set	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	nat-list-set	f	nat-list × nat → nat-list
. -l .	nat-list-set	f	nat-list × nat → nat-list
. -p .	nat-list-set	f	nat-list × nat → nat-list
. .butlast	nat-list-set	pf	nat-list → nat-list with λ nx. nx ≠ []
. .ec	wlentry	f	wlentry → nat
. .ec:= .	wlentry	f	wlentry × nat → wlentry
. .filter ( . )	array-indices	f	nat-set × (nat → bool) → nat-set
. .head	nat-list-set	pf	nat-list → nat with λ nx. nx ≠ []
. .indicesWhere ( . )	wlarray-base	f	wlarray × (wlentry → bool) → nat-list
. .indicesWhere ( . )	wlarray-base	f	wlarray × (wlentry → bool) × nat → nat-list
. .last	nat-list-set	pf	nat-list → nat with λ nx. nx ≠ []
. .map ( . )	wlarray-base	f	wlarray × (wlentry → wlentry) → wlarray
. .map ( . )	array-indices	f	nat-set × (nat → nat) → nat-set
. .mapIf ( . )	wlarray-base	f	wlarray × (wlentry → bool) × (wlentry → wlentry) → wlarray
. .mapIf ( . )	wlarray-base	f	wlarray × (wlentry → bool) × (wlentry → wlentry) × nat → wlarray
. .mapIndices ( . )	wlarray-base	f	wlarray × nat-list × (wlentry → wlentry) → wlarray
. .mapIndices ( . )	wlarray-base	f	wlarray × nat-set × (wlentry → wlentry) → wlarray
. .status	wlentry	f	wlentry → wlstatus
. .status:= .	wlentry	f	wlentry × wlstatus → wlentry
. .tail	nat-list-set	pf	nat-list → nat-list with λ nx. nx ≠ []
. .toSet	nat-list-set	f	nat-list → nat-set
. < .	nat-list-less	p	nat-list × nat
. < .	nat-basic	p	nat × nat
. < .	nat-list-set	p	nat-list × nat-list
. > .	nat	p	nat × nat
. [ . ]	wlarray-base	pf	wlarray × nat × wlentry → wlarray with λ wlar, n, wle. n < # wlar
. [ . ]	wlarray-base	pf	wlarray × nat → wlentry with λ wlar, n. n < # wlar
. [ . ]	nat-list-set	pf	nat-list × nat × nat → nat-list with λ nx, n, n0. n < # nx
. [ . ]	nat-list-set	pf	nat-list × nat → nat with λ nx, n. n < # nx
. \ .	nat-list-set	f	nat-set × nat-set → nat-set
. ∈ .	wlarray-base	p	wlentry × wlarray
. ∈ .	nat-list-set	p	nat × nat-list
. ∈ .	nat-list-set	p	nat × nat-set
. ∩ .	nat-list-set	f	nat-set × nat-set → nat-set
. ∪ .	nat-list-set	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	nat-list-set	p	nat-set × nat-set
. ⊑ .	nat-list-set	p	nat-list × nat-list
. ⊒ .	nat-list-set	p	nat-list × nat-list
[]	nat-list-set	c	nat-list
{ . }	nat-list-set	f	nat → nat-set
φn	array-indices	v	nat → bool
φwlentry	wlarray-base	v	wlentry → bool
∅	nat-list-set	c	nat-set
butlastn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
cmp	wlarray-base	pp	wlarray × wlentry × nat × nat with λ wlar, wle, m, n. m + n ≤ # wlar
cmp	wlarray-base	pp	wlarray × nat × wlarray × nat × nat with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0
copy	wlarray-base	pf	wlarray × nat × wlarray × nat × nat → wlarray with λ wlar, m, wlar0, m0, n. m + n ≤ # wlar ∧ m0 + n ≤ # wlar0
disj	nat-list-set	p	nat-list × nat-list
dropn	nat-list-set	f	nat × nat-list → nat-list
dups	nat-list-set	p	nat-list
erasing	wlstatus	c	wlstatus
erroneous	wlstatus	c	wlstatus
f	wlarray-base	v	wlentry → wlentry
fill	wlarray-base	pf	wlarray × wlentry × nat × nat → wlarray with λ wlar, wle, n, m. n + m ≤ # wlar
fill	wlarray-base	f	wlarray × wlentry → wlarray
fillfirst	nat-list-set	f	nat × nat × nat-list → nat-list
firstn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
fn	array-indices	v	nat → nat
free	wlstatus	c	wlstatus
frome	nat-list-set	f	nat-list × nat → nat-list
id○	wlarray-base	p	wlarray × wlarray × nat
idrange	wlarray-base	pp	wlarray × nat × nat with λ wlar, m, n. m + n ≤ # wlar
lastn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
m	nat-basic	v	nat
m0	wlentry	v	nat
mklist	nat-list-set	f	nat × nat → nat-list
mkwlarray	wlarray-base	f	nat → wlarray
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	nat-list-set	v	nat
n3	nat-list-set	v	nat
n4	nat-list-set	v	nat
n5	nat-list-set	v	nat
nat	nat-basic	s
nat-list	nat-list-set	s
nat-set	nat-list-set	s
ns	nat-list-set	v	nat-set
ns0	nat-list-set	v	nat-set
ns1	nat-list-set	v	nat-set
ns2	nat-list-set	v	nat-set
nx	nat-list-set	v	nat-list
nx0	nat-list-set	v	nat-list
nx1	nat-list-set	v	nat-list
ny	nat-list-set	v	nat-list
nz	nat-list-set	v	nat-list
pos	nat-list-set	f	nat × nat-list → nat
prefixn	nat-list-set	f	nat × nat-list → nat-list
restn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
rev	wlarray-base	pf	wlarray × nat → wlarray with λ wlar, n. n ≤ # wlar
rev	wlarray-base	f	wlarray → wlarray
rev	nat-list-set	f	nat-list → nat-list
rmdup	nat-list-set	f	nat-list → nat-list
slice	nat-list-set	f	nat × nat × nat-list → nat-list
stat	wlstatus	v	wlstatus
stat0	wlentry	v	wlstatus
subarray	wlarray-base	pf	wlarray × nat × nat → wlarray with λ wlar, m, n. m + n ≤ # wlar
sublist	nat-list-set	pf	nat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx
used	wlstatus	c	wlstatus
valid-indices	wlarray-base	p	wlarray × nat-list
wl-entry	wlentry	f	nat × wlstatus → wlentry
wlar	wlarray-base	v	wlarray
wlar0	wlarray-base	v	wlarray
wlar1	wlarray-base	v	wlarray
wlar2	wlarray-base	v	wlarray
wlarray	wlarray-base	s
wle	wlentry	v	wlentry
wle0	wlarray-base	v	wlentry
wle1	wlarray-base	v	wlentry
wlentry	wlentry	s
wlstatus	wlstatus	s