[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
# .	buffer	f	buffer → nat
# .	lp-array	f	lp-array → nat
# .	nat-list-set	f	nat-list → nat
# .	nat-list-set	f	nat-set → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	nat-list-set	f	nat → nat-list
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	nat-list-set	f	nat-list × nat → nat-list
. + .	nat-list-set	f	nat × nat-list → 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 ≠ []
. .filter ( . )	array-indices	f	nat-set × (nat → bool) → nat-set
. .flags	lprops	f	lprops → lpropflags
. .flags:= .	lprops	f	lprops × lpropflags → lprops
. .gcheapidx	lprops	f	lprops → nat
. .gcheapidx:= .	lprops	f	lprops × nat → lprops
. .head	nat-list-set	pf	nat-list → nat with λ nx. nx ≠ []
. .indicesWhere ( . )	lp-array	f	lp-array × (lprops → bool) → nat-list
. .indicesWhere ( . )	lp-array	f	lp-array × (lprops → bool) × nat → nat-list
. .last	nat-list-set	pf	nat-list → nat with λ nx. nx ≠ []
. .map ( . )	lp-array	f	lp-array × (lprops → lprops) → lp-array
. .map ( . )	array-indices	f	nat-set × (nat → nat) → nat-set
. .mapIf ( . )	lp-array	f	lp-array × (lprops → bool) × (lprops → lprops) → lp-array
. .mapIf ( . )	lp-array	f	lp-array × (lprops → bool) × (lprops → lprops) × nat → lp-array
. .mapIndices ( . )	lp-array	f	lp-array × nat-list × (lprops → lprops) → lp-array
. .mapIndices ( . )	lp-array	f	lp-array × nat-set × (lprops → lprops) → lp-array
. .ref-size	lprops	f	lprops → nat
. .ref-size:= .	lprops	f	lprops × nat → lprops
. .size	lprops	f	lprops → nat
. .size:= .	lprops	f	lprops × nat → lprops
. .tail	nat-list-set	pf	nat-list → nat-list with λ nx. nx ≠ []
. .toSet	nat-list-set	f	nat-list → nat-set
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	nat-list-less	p	nat-list × nat
. < .	nat-list-set	p	nat-list × nat-list
. > .	nat	p	nat × nat
. [ . ]	lp-array	pf	lp-array × nat × lprops → lp-array with λ lpt, n, lp. n < # lpt
. [ . ]	lp-array	pf	lp-array × nat → lprops with λ lpt, n. n < # lpt
. [ . ]	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
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. \ .	nat-list-set	f	nat-set × nat-set → nat-set
. ∈ .	lp-array	p	lprops × lp-array
. ∈ .	buffer	p	data × buffer
. ∈ .	nat-list-set	p	nat × nat-set
. ∈ .	nat-list-set	p	nat × nat-list
. ∩ .	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
φ	lp-array	v	lprops → bool
φn	array-indices	v	nat → bool
∅	nat-list-set	c	nat-set
⌊ . ⌋	error-class	p	error
Boolvar	encoding-lprops	v	bool,flexible
EACCESS	error	c	error
EB_PAGE_SIZE	eraseblock	c	nat
EBADFD	error	c	error
ECOMMIT	error	c	error
EEXISTS	error	c	error
EFAIL	error	c	error
EINVAL	error	c	error
EIO	error	c	error
EISDIR	error	c	error
ENCODED_LPROPS_SIZE	encoding-lprops	c	nat
ENOENT	error	c	error
ENOMEM	error	c	error
ENOSPC	error	c	error
ENOTDIR	error	c	error
ENOTEMPTY	error	c	error
EROFS	error	c	error
ERR	error-class	v	error,flexible
ERR0	error-class	v	error,flexible
ESUCCESS	error	c	error
EUCLEAN	error	c	error
LEB_SIZE	eraseblock	c	nat
LP_FREE	lprops	c	lpropflags
LP_GROUP_NODES	lprops	c	lpropflags
LP_INDEX_NODES	lprops	c	lpropflags
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
boolvar	encoding-lprops	v	bool
boolvar0	encoding-lprops	v	bool
boolvar1	encoding-lprops	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
cmp	lp-array	pp	lp-array × lprops × nat × nat with λ lpt, lp, m, n. m + n ≤ # lpt
cmp	lp-array	pp	lp-array × nat × lp-array × nat × nat with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	buffer	pf	buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
copy	lp-array	pf	lp-array × nat × lp-array × nat × nat → lp-array with λ lpt, m, lpt0, m0, n. m + n ≤ # lpt ∧ m0 + n ≤ # lpt0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
decode_lprops#	encoding-lprops	pr	nat × buffer : lprops × nat : error (nondeterministic)
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
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
encode_lprops#	encoding-lprops	pr	lprops × nat : buffer × nat : error (nondeterministic)
encoding-size	encoding-lprops	f	lprops → nat
err	error	v	error
err0	error	v	error
err1	error	v	error
error	error	s
fail#	error-class	pr	: : error (nondeterministic)
fail_or_success#	error-class	pr	: : error (nondeterministic)
fill	lp-array	pf	lp-array × lprops × nat × nat → lp-array with λ lpt, lp, n, m. n + m ≤ # lpt
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	lp-array	f	lp-array × lprops → lp-array
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
frome	nat-list-set	f	nat-list × nat → nat-list
id○	lp-array	p	lp-array × lp-array × nat
id○	buffer	p	buffer × buffer × nat
idrange	lp-array	pp	lp-array × nat × nat with λ lpt, m, n. m + n ≤ # lpt
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
is-aligned	align	p	nat × nat
is-encoded	encoding-lprops	p	lprops × buffer
is-encoded	encoding-lpt	p	lp-array × buffer
is-encoded	encoding-lpt	p	lp-array × buffer × nat
is-garbage-lprops	encoding-lprops	p	buffer
isempty	eraseblock	p	buffer × nat × nat
isempty	eraseblock	p	buffer
lastn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
lp	lprops	v	lprops
lp-array	lp-array	s
lp0	lprops	v	lprops
lp1	encoding-lprops	v	lprops
lpf	lprops	v	lpropflags
lpf0	lprops	v	lpropflags
lpropflags	lprops	s
lprops	lprops	s
lpt	lp-array	v	lp-array
lpt0	lp-array	v	lp-array
lpt1	lp-array	v	lp-array
lpt2	lp-array	v	lp-array
lptfun	lp-array	v	lprops → lprops
lptlebs	encoding-lpt	f	nat × nat → nat
lptsize	encoding-lpt	f	nat × nat → nat
m	nat-basic	v	nat
m0	lprops	v	nat
m1	lprops	v	nat
m2	lprops	v	nat
m3	lprops	v	nat
m4	lprops	v	nat
mainareasize	encoding-lpt	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	nat-list-set	f	nat × nat → nat-list
mklp	lprops	f	nat × nat × lpropflags × nat → lprops
mklparray	lp-array	f	nat → lp-array
mkzbuf	buffer	f	nat → buffer
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
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	nat-list-set	pf	nat × nat-list → nat-list with λ n, nx. n ≤ # nx
rev	lp-array	pf	lp-array × nat → lp-array with λ lpt, n. n ≤ # lpt
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	lp-array	f	lp-array → lp-array
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
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	lp-array	pf	lp-array × nat × nat → lp-array with λ lpt, m, n. m + n ≤ # lpt
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
sublist	nat-list-set	pf	nat × nat × nat-list → nat-list with λ n, m, nx. n + m ≤ # nx
valid-indices	lp-array	p	lp-array × nat-list
zero	buffer	c	data