[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	array	function, array → nat
#	buffer	function, buffer → nat
#	apebs	function, apebs → nat
#	pebs	function, pebs → nat
#	list-data	function, list → nat
#	string	function, string → nat
%	nat-div	partial function, nat × nat → nat
'	list	function, elem → list
'	string	function, char → string
*	nat-mult	function, nat × nat → nat
+	array-splice	function, array × array → array
+	buffer	function, buffer × buffer → buffer
+	nat-basic	function, nat × nat → nat
+	list-data	function, elem × list → list
+	list	function, list × elem → list
+	list	function, list × list → list
+	string	function, string × char → string
+	string	function, string × string → string
+	string	function, char × string → string
++	list-dup	function, list × elem → list
++	string	function, string × char → string
+1	nat-basic	function, nat → nat
+2	list	function, elem × elem → list
+2	string	function, char × char → string
-	nat	partial function, nat × nat → nat
-1	nat-basic	partial function, nat → nat
-1l	list-del	function, list × elem → list
-1l	string	function, string × char → string
-l	list-del	function, list × elem → list
-l	string	function, string × char → string
-p	list-del	function, list × nat → list
-p	string	function, string × nat → string
.bad	peb	predicate, peb
.bad	apeb	predicate, apeb
.bad:=	peb	function, peb × bool → peb
.bad:=	apeb	function, apeb × bool → apeb
.butlast	list-last	partial function, list → list
.butlast	string	partial function, string → string
.char1	string	partial function, string → char
.checksum	vidheader	function, vidheader → nat
.checksum	avidheader	partial function, avidheader → nat
.checksum:=	vidheader	function, vidheader × nat → vidheader
.checksum:=	avidheader	partial function, avidheader × nat → avidheader
.data	peb	function, peb → buffer
.data	apeb	function, apeb → buffer
.data:=	peb	function, peb × buffer → peb
.data:=	apeb	function, apeb × buffer → apeb
.ec	echeader	function, echeader → nat
.ec	aecheader	partial function, aecheader → nat
.ec:=	echeader	function, echeader × nat → echeader
.ec:=	aecheader	partial function, aecheader × nat → aecheader
.echdr	apeb	function, apeb → aecheader
.echdr:=	apeb	function, apeb × aecheader → apeb
.fill	peb	function, peb → nat
.fill	apeb	function, apeb → nat
.fill:=	peb	function, peb × nat → peb
.fill:=	apeb	function, apeb × nat → apeb
.head	list-data	partial function, list → elem
.last	list-last	partial function, list → elem
.last	string	partial function, string → char
.leb	vidheader	function, vidheader → nat
.leb	avidheader	partial function, avidheader → nat
.leb:=	vidheader	function, vidheader × nat → vidheader
.leb:=	avidheader	partial function, avidheader × nat → avidheader
.rstring	string	partial function, string → string
.size	vidheader	function, vidheader → nat
.size	avidheader	partial function, avidheader → nat
.size:=	vidheader	function, vidheader × nat → vidheader
.size:=	avidheader	partial function, avidheader × nat → avidheader
.sqn	vidheader	function, vidheader → nat
.sqn	avidheader	partial function, avidheader → nat
.sqn:=	vidheader	function, vidheader × nat → vidheader
.sqn:=	avidheader	partial function, avidheader × nat → avidheader
.tail	list-data	partial function, list → list
.toString	debug	function, nat → string
.valid?	aecheader	predicate, aecheader
.valid?	avidheader	predicate, avidheader
.vidhdr	apeb	function, apeb → avidheader
.vidhdr:=	apeb	function, apeb × avidheader → apeb
.vol	vidheader	function, vidheader → volid
.vol	avidheader	partial function, avidheader → volid
.vol:=	vidheader	function, vidheader × volid → vidheader
.vol:=	avidheader	partial function, avidheader × volid → avidheader
/	nat-div	partial function, nat × nat → nat
<	nat-basic	predicate, nat × nat
<	list-data	predicate, list × list
>	nat	predicate, nat × nat
AEHDR	ubi-io-asm	variable, aecheader,flexible
AEHDR	aubi-io-asm	variable, aecheader,flexible
APEB	aubi-io-asm	variable, apeb,flexible
APEBS	aubi-io-asm	variable, apebs,flexible
APEBS0	aubi-io-asm	variable, apebs,flexible
AVHDR	ubi-io-asm	variable, avidheader,flexible
AVHDR	aubi-io-asm	variable, avidheader,flexible
BITFLIPS	mtd-asm	variable, bool,flexible
BITFLIPS	aubi-io-asm	variable, bool,flexible
BUF	mtd-asm	variable, buffer,flexible
BUF	aubi-io-asm	variable, buffer,flexible
BUF0	mtd-asm	variable, buffer,flexible
BUF0	aubi-io-asm	variable, buffer,flexible
Boolvar	encoding-echeader	variable, bool,flexible
Boolvar	encoding-vidheader	variable, bool,flexible
EACCESS	error	constant, error
EBADFD	error	constant, error
EB_PAGE_SIZE	eraseblock	constant, nat
ECOMMIT	error	constant, error
EEXISTS	error	constant, error
EFAIL	error	constant, error
EHDR	ubi-io-asm	variable, echeader,flexible
EINVAL	error	constant, error
EIO	error	constant, error
EISDIR	error	constant, error
ENCODED_EC_HEADER_SIZE	encoding-echeader	constant, nat
ENCODED_ELEM_SIZE	encoding-elem-size	constant, nat
ENCODED_VIDHEADER_SIZE	encoding-vidheader	constant, nat
ENOENT	error	constant, error
ENOMEM	error	constant, error
ENOSPC	error	constant, error
ENOTDIR	error	constant, error
ENOTEMPTY	error	constant, error
EROFS	error	constant, error
ERR	error-class	variable, error,flexible
ERR0	error-class	variable, error,flexible
ESUCCESS	error	constant, error
EUCLEAN	error	constant, error
ISBAD	mtd-asm	variable, bool,flexible
ISBAD	aubi-io-asm	variable, bool,flexible
LEB_SIZE	eraseblock	constant, nat
M	ubi-io-asm	variable, nat,flexible
N	mtd-asm	variable, nat,flexible
N	aubi-io-asm	variable, nat,flexible
N0	mtd-asm	variable, nat,flexible
N0	aubi-io-asm	variable, nat,flexible
N1	mtd-asm	variable, nat,flexible
N1	aubi-io-asm	variable, nat,flexible
OFFSET	mtd-asm	variable, nat,flexible
OFFSET	aubi-io-asm	variable, nat,flexible
PAGESIZE	ubi-io-asm	variable, nat,flexible
PAGES_PER_LEB	eraseblock	constant, nat
PAGES_PER_PEB	eraseblock	constant, nat
PEB	mtd-asm	variable, peb,flexible
PEBS	mtd-asm	variable, pebs,flexible
PEB_SIZE	eraseblock	constant, nat
PNUM	mtd-asm	variable, nat,flexible
PNUM	aubi-io-asm	variable, nat,flexible
PNUM0	mtd-asm	variable, nat,flexible
TRIES	ubi-io-asm	variable, nat,flexible
UBI_READ_RETRIES	ubi-io-asm	constant, nat
VHDR	ubi-io-asm	variable, vidheader,flexible
[]	list-data	constant, list
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	buffer	partial function, buffer × nat × data → buffer
]	buffer	partial function, buffer × nat → data
]	apebs	partial function, apebs × nat × apeb → apebs
]	apebs	partial function, apebs × nat → apeb
]	pebs	partial function, pebs × nat × peb → pebs
]	pebs	partial function, pebs × nat → peb
]	list-del	partial function, list × nat × elem → list
]	list-del	partial function, list × nat → elem
]	string	partial function, string × nat × char → string
]	string	partial function, string × nat → char
a	elem	variable, elem
a0	list-data	variable, elem
abs	ubi-io-abs	predicate, pebs × apebs
abs-echdr	ubi-io-abs	predicate, buffer × aecheader
abs-peb	ubi-io-abs	predicate, peb × apeb
abs-vidhdr	ubi-io-abs	predicate, buffer × avidheader
aechdr	aecheader	function, nat → aecheader
aecheader	aecheader	sort,
aehdr	aecheader	variable, aecheader
aehdr0	aecheader	variable, aecheader
aehdr1	aecheader	variable, aecheader
align↑	align	function, nat × nat → nat
align↓	align	function, nat × nat → nat
apeb	apeb	variable, apeb
apeb	apeb	sort,
apeb0	apebs	variable, apeb
apeb1	apebs	variable, apeb
apebs	apebs	variable, apebs
apebs	apebs	sort,
apebs0	apebs	variable, apebs
apebs1	apebs	variable, apebs
apebs2	apebs	variable, apebs
ar	array	variable, array
ar0	array	variable, array
ar1	array	variable, array
ar2	array	variable, array
array	array	sort,
aubi_io_format#	aubi-io-asm	procedure, : : apebs × error
aubi_io_get_blockcount#	aubi-io-asm	procedure, apebs : : nat
aubi_io_get_leb_size#	aubi-io-asm	procedure, apebs : : nat
aubi_io_get_page_size#	aubi-io-asm	procedure, apebs : : nat
aubi_io_isbad#	aubi-io-asm	procedure, nat × apebs : : bool × error
aubi_io_markbad#	aubi-io-asm	procedure, nat : apebs : error
aubi_io_read_data#	aubi-io-asm	procedure, nat × nat × nat × nat × apebs : buffer : bool × error
aubi_io_read_echdr#	aubi-io-asm	procedure, nat × apebs : aecheader : bool × error
aubi_io_read_vidhdr#	aubi-io-asm	procedure, nat × apebs : avidheader : bool × error
aubi_io_recovery#	aubi-io-asm	procedure, apebs :
aubi_io_sync_erase#	aubi-io-asm	procedure, nat : apebs : error
aubi_io_write_data#	aubi-io-asm	procedure, nat × nat × nat × nat × buffer : apebs : error
aubi_io_write_data_wl#	aubi-io-asm	procedure, nat × nat × buffer : apebs : error
aubi_io_write_echdr#	aubi-io-asm	procedure, nat × aecheader : apebs : error
aubi_io_write_vidhdr#	aubi-io-asm	procedure, nat × avidheader : apebs : error
avhdr	avidheader	variable, avidheader
avhdr0	avidheader	variable, avidheader
avhdr1	avidheader	variable, avidheader
avidhdr	avidheader	function, volid × nat × nat × nat × nat → avidheader
avidheader	avidheader	sort,
b	elem	variable, elem
bitflips	mtd-asm	variable, bool
bitflips	aubi-io-asm	variable, bool
bool	bool	sort,
boolvar	bool	variable, bool
boolvar	encoding-echeader	variable, bool
boolvar	encoding-vidheader	variable, bool
boolvar0	bool	variable, bool
boolvar0	encoding-echeader	variable, bool
boolvar0	encoding-vidheader	variable, bool
boolvar1	encoding-echeader	variable, bool
boolvar1	encoding-vidheader	variable, bool
buf	buffer	variable, buffer
buf0	buffer	variable, buffer
buf1	buffer	variable, buffer
buf2	buffer	variable, buffer
buffer	buffer	sort,
butlastn	list-last	partial function, nat × list → list
butlastn	string	partial function, nat × string → string
c	elem	variable, elem
char	char	variable, char
char	char	sort,
char0	char	variable, char
char1	char	variable, char
char2	char	variable, char
checksum	checksum	function, buffer × nat → nat
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
cmp	buffer	partial predicate, buffer × data × nat × nat
cmp	buffer	partial predicate, buffer × nat × buffer × nat × nat
cmp	apebs	partial predicate, apebs × apeb × nat × nat
cmp	apebs	partial predicate, apebs × nat × apebs × nat × nat
cmp	pebs	partial predicate, pebs × peb × nat × nat
cmp	pebs	partial predicate, pebs × nat × pebs × nat × nat
copy	array-copy	partial function, array × nat × array × nat × nat → array
copy	buffer	partial function, buffer × nat × buffer × nat × nat → buffer
copy	apebs	partial function, apebs × nat × apebs × nat × nat → apebs
copy	pebs	partial function, pebs × nat × pebs × nat × nat → pebs
d	data	variable, data
d0	data	variable, data
d1	data	variable, data
d2	data	variable, data
data	data	sort,
datasize	datasize	function, buffer × nat → nat
datasize	datasize	function, buffer → nat
debug#	debug	procedure, string :
decode#	encoding	procedure, nat × buffer : elem × nat : error
decode_echeader#	encoding-echeader	procedure, nat × buffer : echeader : error
decode_echeader_empty#	encoding-echeader	procedure, nat × buffer : echeader × nat : error
decode_echeader_nonempty#	encoding-echeader	procedure, nat × buffer : echeader : error
decode_nonempty#	encoding-fixed-size-nonempty	procedure, nat × buffer : elem : error
decode_pagesize#	encoding-page-size-nonempty	procedure, nat × buffer : elem : error
decode_vidheader#	encoding-vidheader	procedure, nat × buffer : vidheader : error
decode_vidheader_empty#	encoding-vidheader	procedure, nat × buffer : vidheader × nat : error
decode_vidheader_nonempty#	encoding-vidheader	procedure, nat × buffer : vidheader : error
disj	list-dup	predicate, list × list
disj	string	predicate, string × string
dups	list-dup	predicate, list
dups	string	predicate, string
echdr	echeader	function, nat → echeader
echeader	echeader	sort,
ehdr	echeader	variable, echeader
ehdr0	encoding-echeader	variable, echeader
ehdr1	encoding-echeader	variable, echeader
elem	elem	sort,
empty	array-splice	constant, elem
empty	buffer	constant, data
empty	aecheader	constant, aecheader
empty	avidheader	constant, avidheader
emptyleb	eraseblock	constant, buffer
emptypage	eraseblock	constant, buffer
emptypeb	eraseblock	constant, buffer
encode#	encoding	procedure, elem × nat : buffer × nat : error
encode_echeader#	encoding-echeader	procedure, nat × echeader : buffer : error
encode_echeader_empty#	encoding-echeader	procedure, echeader × nat : buffer × nat : error
encode_echeader_nonempty#	encoding-echeader	procedure, echeader × nat : buffer : error
encode_nonempty#	encoding-fixed-size-nonempty	procedure, elem × nat : buffer : error
encode_pagesize#	encoding-page-size-nonempty	procedure, nat × elem : buffer : error
encode_vidheader#	encoding-vidheader	procedure, nat × vidheader : buffer : error
encode_vidheader_empty#	encoding-vidheader	procedure, vidheader × nat : buffer × nat : error
encode_vidheader_nonempty#	encoding-vidheader	procedure, vidheader × nat : buffer : error
encoding-size	encoding-echeader	function, echeader → nat
encoding-size	encoding-vidheader	function, vidheader → nat
encoding-size	encoding	function, elem → nat
err	error	variable, error
err0	error	variable, error
err1	error	variable, error
error	error	sort,
fail#	error-class	procedure, : : error
fail_or_success#	error-class	procedure, : : error
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
fill	buffer	partial function, buffer × data × nat × nat → buffer
fill	buffer	function, buffer × data → buffer
fill	apebs	partial function, apebs × apeb × nat × nat → apebs
fill	apebs	function, apebs × apeb → apebs
fill	pebs	partial function, pebs × peb × nat × nat → pebs
fill	pebs	function, pebs × peb → pebs
fillfirst	list-last	function, nat × elem × list → list
fillfirst	string	function, nat × char × string → string
firstn	list-del	partial function, nat × list → list
firstn	string	partial function, nat × string → string
frome	list-del	function, list × elem → list
frome	string	function, string × char → string
garbage	aecheader	constant, aecheader
garbage	avidheader	constant, avidheader
idrange	array-copy	partial predicate, array × nat × nat
idrange	buffer	partial predicate, buffer × nat × nat
idrange	apebs	partial predicate, apebs × nat × nat
idrange	pebs	partial predicate, pebs × nat × nat
id○	array-copy	predicate, array × array × nat
id○	buffer	predicate, buffer × buffer × nat
id○	apebs	predicate, apebs × apebs × nat
id○	pebs	predicate, pebs × pebs × nat
initial-apebs	ubi-io-abs	function, pebs → apebs
is-aligned	align	predicate, nat × nat
is-encoded	encoding-echeader	predicate, echeader × buffer
is-encoded	encoding-vidheader	predicate, vidheader × buffer
is-encoded	encoding	predicate, elem × buffer
is-encoded-empty	encoding-echeader	predicate, echeader × buffer
is-encoded-empty	encoding-vidheader	predicate, vidheader × buffer
is-encoded-nonempty	encoding-echeader	predicate, echeader × buffer
is-encoded-nonempty	encoding-vidheader	predicate, vidheader × buffer
is-encoded-nonempty	encoding-fixed-size-nonempty	predicate, elem × buffer
is-encoded-pagesize	encoding-page-size-nonempty	predicate, elem × buffer
is-garbage	encoding	predicate, buffer
is-garbage-ec	encoding-echeader	predicate, buffer
is-garbage-empty-ec	encoding-echeader	predicate, buffer
is-garbage-empty-vid	encoding-vidheader	predicate, buffer
is-garbage-nonempty	encoding-fixed-size-nonempty	predicate, buffer
is-garbage-nonempty-ec	encoding-echeader	predicate, buffer
is-garbage-nonempty-vid	encoding-vidheader	predicate, buffer
is-garbage-pagesize	encoding-page-size-nonempty	predicate, buffer
is-garbage-vid	encoding-vidheader	predicate, buffer
isbad	mtd-asm	variable, bool
isbad	aubi-io-asm	variable, bool
isempty	eraseblock	predicate, buffer × nat × nat
isempty	eraseblock	predicate, buffer
lastn	list-del	partial function, nat × list → list
lastn	string	partial function, nat × string → string
list	list-data	sort,
m	nat-basic	variable, nat
m0	array-copy	variable, nat
m0	echeader	variable, nat
m0	aecheader	variable, nat
m1	vidheader	variable, nat
m1	avidheader	variable, nat
m1	mtd-base	variable, nat
m2	vidheader	variable, nat
m2	avidheader	variable, nat
m2	mtd-base	variable, nat
m3	vidheader	variable, nat
m3	avidheader	variable, nat
m4	vidheader	variable, nat
m4	avidheader	variable, nat
m5	vidheader	variable, nat
m5	avidheader	variable, nat
m6	vidheader	variable, nat
m6	avidheader	variable, nat
max	min-max	function, nat × nat → nat
min	min-max	function, nat × nat → nat
mkapebs	apebs	function, nat → apebs
mkarray	array	function, nat → array
mkbuf	buffer	function, nat → buffer
mkemparray	array-splice	function, nat → array
mkempbuf	buffer	function, nat → buffer
mklist	list-last	function, elem × nat → list
mklist	string	function, char × nat → string
mkpeb	peb	function, buffer × nat × bool → peb
mkpeb	apeb	function, aecheader × avidheader × buffer × nat × bool → apeb
mkpebs	pebs	function, nat → pebs
mkzarray	array-splice	function, nat → array
mkzbuf	buffer	function, nat → buffer
mtd-cons	mtd-base	predicate, pebs
mtd-valid-peb	mtd-base	predicate, peb
mtd_asm_erase#	mtd-asm	procedure, nat : pebs : error
mtd_asm_get_blockcount#	mtd-asm	procedure, pebs : : nat
mtd_asm_get_page_size#	mtd-asm	procedure, pebs : : nat
mtd_asm_get_peb_size#	mtd-asm	procedure, pebs : : nat
mtd_asm_init#	mtd-asm	procedure, : : pebs × error
mtd_asm_isbad#	mtd-asm	procedure, nat × pebs : : bool × error
mtd_asm_markbad#	mtd-asm	procedure, nat : pebs : error
mtd_asm_read#	mtd-asm	procedure, nat × nat × nat × nat × pebs : buffer : bool × error
mtd_asm_write#	mtd-asm	procedure, nat × nat × nat × nat × buffer : pebs : error
n	nat-basic	variable, nat
n0	nat-basic	variable, nat
n1	nat-basic	variable, nat
n2	ubi-io-pre	variable, nat
nat	nat-basic	sort,
peb	peb	variable, peb
peb	peb	sort,
peb0	pebs	variable, peb
peb1	pebs	variable, peb
pebs	pebs	variable, pebs
pebs	pebs	sort,
pebs0	pebs	variable, pebs
pebs1	pebs	variable, pebs
pebs2	pebs	variable, pebs
pos	list-del	function, elem × list → nat
pos	string	function, char × string → nat
range=	array-splice	predicate, array × nat × array × nat × nat
range=	buffer	predicate, buffer × nat × buffer × nat × nat
resize	array-splice	function, array × nat → array
resize	buffer	function, buffer × nat → buffer
restn	list-del	partial function, nat × list → list
restn	string	partial function, nat × string → string
rev	array-copy	partial function, array × nat → array
rev	array-copy	function, array → array
rev	buffer	partial function, buffer × nat → buffer
rev	buffer	function, buffer → buffer
rev	apebs	partial function, apebs × nat → apebs
rev	apebs	function, apebs → apebs
rev	pebs	partial function, pebs × nat → pebs
rev	pebs	function, pebs → pebs
rev	list-last	function, list → list
rev	string	function, string → string
rmdup	list-dup	function, list → list
rmdup	string	function, string → string
splice	array-splice	function, array × nat × array × nat × nat → array
splice	buffer	function, buffer × nat × buffer × nat × nat → buffer
str	string	variable, string
str0	string	variable, string
str1	string	variable, string
str2	string	variable, string
str3	string	variable, string
string	string	sort,
subarray	array-copy	partial function, array × nat × nat → array
subarray	buffer	partial function, buffer × nat × nat → buffer
subarray	apebs	partial function, apebs × nat × nat → apebs
subarray	pebs	partial function, pebs × nat × nat → pebs
sublist	list-del	partial function, nat × nat × list → list
sublist	string	partial function, nat × nat × string → string
ubi-io-erase-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-initial	ubi-io-inv	predicate, apebs
ubi-io-initial	ubi-io-base	predicate, pebs
ubi-io-inv	ubi-io-inv	predicate, apebs
ubi-io-isbad-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-markbad-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-peb-initial	ubi-io-inv	predicate, apeb
ubi-io-peb-initial	ubi-io-base	predicate, peb
ubi-io-peb-inv	ubi-io-inv	predicate, apeb
ubi-io-read-data-pre	ubi-io-pre	predicate, nat × nat × nat × nat × buffer × apebs
ubi-io-read-echdr-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-read-vidhdr-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-write-data-pre	ubi-io-pre	predicate, nat × nat × nat × nat × buffer × apebs
ubi-io-write-data-wl-pre	ubi-io-pre	predicate, nat × nat × buffer × apebs
ubi-io-write-echdr-pre	ubi-io-pre	predicate, nat × aecheader × apebs
ubi-io-write-vidhdr-pre	ubi-io-pre	predicate, nat × avidheader × apebs
ubi_io_format#	ubi-io-asm	procedure, : nat × pebs : error
ubi_io_get_blockcount#	ubi-io-asm	procedure, pebs : : nat
ubi_io_get_leb_size#	ubi-io-asm	procedure, nat × pebs : : nat
ubi_io_get_page_size#	ubi-io-asm	procedure, nat : : nat
ubi_io_isbad#	ubi-io-asm	procedure, nat × pebs : : bool × error
ubi_io_markbad#	ubi-io-asm	procedure, nat : pebs : error
ubi_io_read#	ubi-io-asm	procedure, nat × nat × nat × nat × pebs : buffer : bool × error
ubi_io_read_data#	ubi-io-asm	procedure, nat × nat × nat × nat × nat × pebs : buffer : bool × error
ubi_io_read_echdr#	ubi-io-asm	procedure, nat × nat × pebs : aecheader : bool × error
ubi_io_read_vidhdr#	ubi-io-asm	procedure, nat × nat × pebs : avidheader : bool × error
ubi_io_recovery#	ubi-io-asm	procedure, pebs : : nat
ubi_io_sync_erase#	ubi-io-asm	procedure, nat : pebs : error
ubi_io_write_data#	ubi-io-asm	procedure, nat × nat × nat × nat × buffer × nat : pebs : error
ubi_io_write_data_wl#	ubi-io-asm	procedure, nat × nat × buffer × nat : pebs : error
ubi_io_write_echdr#	ubi-io-asm	procedure, nat × aecheader × nat : pebs : error
ubi_io_write_vidhdr#	ubi-io-asm	procedure, nat × avidheader × nat : pebs : error
v	volid	variable, volid
v0	volid	variable, volid
v1	volid	variable, volid
v2	volid	variable, volid
vhdr	vidheader	variable, vidheader
vhdr0	encoding-vidheader	variable, vidheader
vhdr1	encoding-vidheader	variable, vidheader
vidhdr	vidheader	function, volid × nat × nat × nat × nat → vidheader
vidheader	vidheader	sort,
volid	volid	sort,
x	list-data	variable, list
x0	list-data	variable, list
x1	list-data	variable, list
y	list-data	variable, list
z	list-data	variable, list
zero	array-splice	constant, elem
zero	buffer	constant, data
∈	array-copy	predicate, elem × array
∈	buffer	predicate, data × buffer
∈	apebs	predicate, apeb × apebs
∈	pebs	predicate, peb × pebs
∈	list	predicate, elem × list
∈	string	predicate, char × string
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⊏	string	predicate, string × string
⊑	list-last	predicate, list × list
⊑	string	predicate, string × string
⊒	list-last	predicate, list × list
⊒	string	predicate, string × string
⌋	error-class	predicate, error