[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
#	recovery-entries	function, recoveryentries → nat
#	erasequeue-base	function, queue → nat
#	list-data	function, list → nat
#	nat-bag	function, nat-bag → nat
#	bag-union	function, bag → nat
#	nat-set	function, nat-set → nat
#	vtbl	function, vtbl → nat
#	buffer	function, buffer → nat
#	volumes	function, volumes → nat
#	store	function, store → nat
#	set-basic	function, set → nat
#	ebatbl	function, ebatbl → nat
#	wlarray-base	function, wlarray → nat
#	array	function, array → nat
#	apebs	function, apebs → nat
#	lebrefset	function, lebrefset → nat
#	nat-list-set	function, nat-set → nat
#	nat-list-set	function, nat-list → nat
#	abstract-volume	function, abstract-volume → nat
#	abstract-volumes	function, abstract-volumes → nat
#	string	function, string → nat
%	nat-div	partial function, nat × nat → nat
'	erasequeue-base	function, erasequeueentry → queue
'	list	function, elem → list
'	nat-list-set	function, nat → nat-list
'	string	function, char → string
*	nat-mult	function, nat × nat → nat
+	erasequeue-base	function, queue × erasequeueentry → queue
+	erasequeue-base	function, queue × queue → queue
+	erasequeue-base	function, erasequeueentry × queue → queue
+	list	function, list × elem → list
+	list	function, list × list → list
+	list-data	function, elem × list → list
+	buffer	function, buffer × buffer → buffer
+	array-splice	function, array × array → array
+	nat-list-set	function, nat-list × nat → nat-list
+	nat-list-set	function, nat-list × nat-list → nat-list
+	nat-list-set	function, nat × nat-list → nat-list
+	string	function, string × char → string
+	string	function, string × string → string
+	string	function, char × string → string
+	nat-basic	function, nat × nat → nat
++	list-dup	function, list × elem → list
++	erasequeue-base	function, queue × erasequeueentry → queue
++	nat-bag	function, nat-bag × nat → nat-bag
++	bag-basic	function, bag × elem → bag
++	nat-set	function, nat-set × nat → nat-set
++	set-basic	function, set × elem → set
++	lebrefset	function, lebrefset × lebref → lebrefset
++	nat-list-set	function, nat-set × nat → nat-set
++	nat-list-set	function, nat-list × nat → nat-list
++	string	function, string × char → string
+1	nat-basic	function, nat → nat
+2	erasequeue-base	function, erasequeueentry × erasequeueentry → queue
+2	list	function, elem × elem → list
+2	nat-list-set	function, nat × nat → nat-list
+2	string	function, char × char → string
-	erasequeue	function, queue × volid → queue
-	erasequeue	function, queue × lebref → queue
-	erasequeue	function, queue × nat → queue
-	nat	partial function, nat × nat → nat
--	recovery-entries	function, recoveryentries × lebadress → recoveryentries
--	nat-bag	function, nat-bag × nat → nat-bag
--	bag-union	function, bag × elem → bag
--	nat-set	function, nat-set × nat → nat-set
--	vtbl	function, vtbl × volid → vtbl
--	volumes	function, volumes × volid → volumes
--	store	function, store × elem → store
--	set-union	function, set × elem → set
--	lebrefset	function, lebrefset × lebref → lebrefset
--	nat-list-set	function, nat-set × nat → nat-set
--	abstract-volumes	function, abstract-volumes × volid → abstract-volumes
-1	nat-basic	partial function, nat → nat
-1l	list-del	function, list × elem → list
-1l	erasequeue-base	function, queue × erasequeueentry → queue
-1l	nat-list-set	function, nat-list × nat → nat-list
-1l	string	function, string × char → string
-l	list-del	function, list × elem → list
-l	erasequeue-base	function, queue × erasequeueentry → queue
-l	nat-list-set	function, nat-list × nat → nat-list
-l	string	function, string × char → string
-p	list-del	function, list × nat → list
-p	erasequeue-base	function, queue × nat → queue
-p	nat-list-set	function, nat-list × nat → nat-list
-p	string	function, string × nat → string
.bad	apeb	predicate, apeb
.bad:=	apeb	function, apeb × bool → apeb
.butlast	list-last	partial function, list → list
.butlast	erasequeue-base	partial function, queue → queue
.butlast	nat-list-set	partial function, nat-list → nat-list
.butlast	string	partial function, string → string
.butmax	nat-set	partial function, nat-set → nat-set
.butmax	oset	partial function, set → set
.butmin	nat-set	partial function, nat-set → nat-set
.butmin	oset	partial function, set → set
.char1	string	partial function, string → char
.checksum	avidheader	partial function, avidheader → nat
.checksum:=	avidheader	partial function, avidheader × nat → avidheader
.data	apeb	function, apeb → buffer
.data	leb	partial function, leb → buffer
.data:=	apeb	function, apeb × buffer → apeb
.data:=	leb	partial function, leb × buffer → leb
.ec	wlentry	function, wlentry → nat
.ec	aecheader	partial function, aecheader → nat
.ec:=	wlentry	function, wlentry × nat → wlentry
.ec:=	aecheader	partial function, aecheader × nat → aecheader
.echdr	apeb	function, apeb → aecheader
.echdr:=	apeb	function, apeb × aecheader → apeb
.fill	apeb	function, apeb → nat
.fill	leb	partial function, leb → nat
.fill:=	apeb	function, apeb × nat → apeb
.fill:=	leb	partial function, leb × nat → leb
.filter	array-indices	function, nat-set × nat → bool → nat-set
.head	erasequeue-base	partial function, queue → erasequeueentry
.head	list-data	partial function, list → elem
.head	nat-list-set	partial function, nat-list → nat
.indicesWhere	wlarray-base	function, wlarray × wlentry → bool × nat → nat-list
.indicesWhere	wlarray-base	function, wlarray × wlentry → bool → nat-list
.indicesWhere	array-indices	function, array × elem → bool × nat → nat-list
.indicesWhere	array-indices	function, array × elem → bool → nat-list
.last	list-last	partial function, list → elem
.last	erasequeue-base	partial function, queue → erasequeueentry
.last	nat-list-set	partial function, nat-list → nat
.last	string	partial function, string → char
.leb	lebadress	function, lebadress → nat
.leb	lebref	partial function, lebref → nat
.leb	avidheader	partial function, avidheader → nat
.leb:=	lebadress	function, lebadress × nat → lebadress
.leb:=	lebref	partial function, lebref × nat → lebref
.leb:=	avidheader	partial function, avidheader × nat → avidheader
.lebref	erasequeueentry	function, erasequeueentry → lebref
.lebref:=	erasequeueentry	function, erasequeueentry × lebref → erasequeueentry
.lebrefs	erasequeue	function, queue → lebrefset
.map	wlarray-base	function, wlarray × wlentry → wlentry → wlarray
.map	array-indices	function, array × elem → elem → array
.map	array-indices	function, nat-set × nat → nat → nat-set
.mapIf	wlarray-base	function, wlarray × wlentry → bool × wlentry → wlentry × nat → wlarray
.mapIf	wlarray-base	function, wlarray × wlentry → bool × wlentry → wlentry → wlarray
.mapIf	array-indices	function, array × elem → bool × elem → elem × nat → array
.mapIf	array-indices	function, array × elem → bool × elem → elem → array
.mapIndices	wlarray-base	function, wlarray × nat-set × wlentry → wlentry → wlarray
.mapIndices	wlarray-base	function, wlarray × nat-list × wlentry → wlentry → wlarray
.mapIndices	array-indices	function, array × nat-set × elem → elem → array
.mapIndices	array-indices	function, array × nat-list × elem → elem → array
.mapped?	leb	predicate, leb
.max	bag-max	function, nat-bag → nat
.max	nat-set	partial function, nat-set → nat
.max	oset	partial function, set → elem
.min	nat-set	partial function, nat-set → nat
.min	oset	partial function, set → elem
.pnum	erasequeueentry	function, erasequeueentry → nat
.pnum	ebaentry	partial function, ebaentry → nat
.pnum	recovery-entry	function, recoveryentry → nat
.pnum:=	erasequeueentry	function, erasequeueentry × nat → erasequeueentry
.pnum:=	ebaentry	partial function, ebaentry × nat → ebaentry
.pnum:=	recovery-entry	function, recoveryentry × nat → recoveryentry
.rstring	string	partial function, string → string
.size	avidheader	partial function, avidheader → nat
.size:=	avidheader	partial function, avidheader × nat → avidheader
.sqn	recovery-entry	function, recoveryentry → nat
.sqn	avidheader	partial function, avidheader → nat
.sqn:=	recovery-entry	function, recoveryentry × nat → recoveryentry
.sqn:=	avidheader	partial function, avidheader × nat → avidheader
.status	wlentry	function, wlentry → wlstatus
.status:=	wlentry	function, wlentry × wlstatus → wlentry
.tail	erasequeue-base	partial function, queue → queue
.tail	list-data	partial function, list → list
.tail	nat-list-set	partial function, nat-list → nat-list
.toSet	nat-list-set	function, nat-list → nat-set
.toSet	list+set	function, list → set
.toString	debug	function, nat → string
.valid?	avidheader	predicate, avidheader
.valid?	aecheader	predicate, aecheader
.vidhdr	apeb	function, apeb → avidheader
.vidhdr:=	apeb	function, apeb × avidheader → apeb
.vol	lebadress	function, lebadress → volid
.vol	lebref	partial function, lebref → volid
.vol	avidheader	partial function, avidheader → volid
.vol:=	lebadress	function, lebadress × volid → lebadress
.vol:=	lebref	partial function, lebref × volid → lebref
.vol:=	avidheader	partial function, avidheader × volid → avidheader
/	nat-div	partial function, nat × nat → nat
<	erasequeue-base	predicate, queue × queue
<	list-data	predicate, list × list
<	nat-set	predicate, nat-set × nat
<	nat-set	predicate, nat × nat-set
<	oset	predicate, set × elem
<	oset	predicate, elem × set
<	oelem	predicate, elem × elem
<	nat-list-set	predicate, nat-list × nat-list
<	nat-list-less	predicate, nat-list × nat
<	nat-basic	predicate, nat × nat
>	nat	predicate, nat × nat
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	aubi-io-asm	variable, avidheader,flexible
AVOLS	ebm-asm	variable, abstract-volumes,flexible
AVOLS0	ebm-asm	variable, abstract-volumes,flexible
BFLIPSET	ubi-asm	variable, nat-set,flexible
BITFLIPS	aubi-io-asm	variable, bool,flexible
BITFLIPS0	ubi-asm	variable, bool,flexible
BUF	aubi-io-asm	variable, buffer,flexible
BUF	encoding-vtbl	variable, buffer,flexible
BUF	ebm-asm	variable, buffer,flexible
BUF0	aubi-io-asm	variable, buffer,flexible
BUF0	ebm-asm	variable, buffer,flexible
Boolvar	encoding-volid	variable, bool,flexible
Boolvar	encoding-nat	variable, bool,flexible
CHKSM	ubi-asm	variable, nat,flexible
EACCESS	error	constant, error
EBADFD	error	constant, error
EBAENT	ubi-asm	variable, ebaentry,flexible
EBATBL	ubi-asm	variable, ebatbl,flexible
EB_PAGE_SIZE	eraseblock	constant, nat
EC	ubi-asm	variable, nat,flexible
ECOMMIT	error	constant, error
EEXISTS	error	constant, error
EFAIL	error	constant, error
EINVAL	error	constant, error
EIO	error	constant, error
EISDIR	error	constant, error
ENCODED_ELEM_SIZE	encoding-elem-size	constant, nat
ENCODED_NAT_SIZE	encoding-nat	constant, nat
ENCODED_VOLID_SIZE	encoding-volid	constant, nat
ENOENT	error	constant, error
ENOMEM	error	constant, error
ENOSPC	error	constant, error
ENOTDIR	error	constant, error
ENOTEMPTY	error	constant, error
EQENT	ubi-asm	variable, erasequeueentry,flexible
ERASEQ	ubi-asm	variable, queue,flexible
EROFS	error	constant, error
ERR	error-class	variable, error,flexible
ERR0	error-class	variable, error,flexible
ESUCCESS	error	constant, error
EUCLEAN	error	constant, error
FOUND	ubi-asm	variable, bool,flexible
FREEECS	ubi-asm	variable, nat-set,flexible
FROM	ubi-asm	variable, nat,flexible
INDEX	encoding-vtbl	variable, nat,flexible
INVALIDECS	ubi-asm	variable, nat-list,flexible
ISBAD	aubi-io-asm	variable, bool,flexible
LADR	ubi-asm	variable, lebadress,flexible
LEBSIZE	ubi-asm	variable, nat,flexible
LEB_SIZE	eraseblock	constant, nat
LNUM	ubi-asm	variable, nat,flexible
LNUM	ebm-asm	variable, nat,flexible
LREF	ubi-asm	variable, lebref,flexible
M	encoding-vtbl	variable, nat,flexible
N	aubi-io-asm	variable, nat,flexible
N	encoding-vtbl	variable, nat,flexible
N	ebm-asm	variable, nat,flexible
N0	aubi-io-asm	variable, nat,flexible
N0	ebm-asm	variable, nat,flexible
N1	aubi-io-asm	variable, nat,flexible
N1	ebm-asm	variable, nat,flexible
OFFSET	aubi-io-asm	variable, nat,flexible
OFFSET	ebm-asm	variable, nat,flexible
PAGESIZE	ubi-asm	variable, nat,flexible
PAGES_PER_LEB	eraseblock	constant, nat
PAGES_PER_PEB	eraseblock	constant, nat
PEB_SIZE	eraseblock	constant, nat
PNUM	aubi-io-asm	variable, nat,flexible
PNUM0	ubi-asm	variable, nat,flexible
RECS	ubi-asm	variable, recoveryentries,flexible
SIZE	encoding-vtbl	variable, nat,flexible
SQNUM	ubi-asm	variable, nat,flexible
TMPERASEQ	ubi-asm	variable, queue,flexible
TO	ubi-asm	variable, nat,flexible
TRIES	ubi-asm	variable, nat,flexible
UBI_ERASE_RETRIES	ubi-base	constant, nat
UBI_WRITE_RETRIES	ubi-base	constant, nat
USEDECS	ubi-asm	variable, nat-set,flexible
VALID	ubi-asm	variable, bool,flexible
VALIDCOUNT	ubi-asm	variable, nat,flexible
VALIDECSUM	ubi-asm	variable, nat,flexible
VOLID	encoding-vtbl	variable, volid,flexible
VOLID	ebm-asm	variable, volid,flexible
VOLID0	ubi-asm	variable, volid,flexible
VOLID0	ebm-asm	variable, volid,flexible
VOLS	ubi-asm	variable, volumes,flexible
VTBL	encoding-vtbl	variable, vtbl,flexible
VTBLPNUM	ubi-asm	variable, nat,flexible
VTBL_LNUM	vtbl-conv	constant, nat
VTBL_VOLID	vtbl-conv	constant, volid
WLARRAY	ubi-asm	variable, wlarray,flexible
WLFREE	ubi-asm	variable, wlentry,flexible
WLUSED	ubi-asm	variable, wlentry,flexible
WL_THRESHOLD	ubi-base	constant, nat
[]	erasequeue-base	constant, queue
[]	list-data	constant, list
[]	nat-list-set	constant, nat-list
\	list-set	function, list × list → list
\	erasequeue-base	function, queue × queue → queue
\	nat-bag	function, nat-bag × nat-bag → nat-bag
\	bag-union	function, bag × bag → bag
\	nat-set	function, nat-set × nat-set → nat-set
\	set-union	function, set × set → set
\	lebrefset	function, lebrefset × lebrefset → lebrefset
\	nat-list-set	function, nat-set × nat-set → nat-set
]	recovery-entries	partial function, recoveryentries × lebadress → recoveryentry
]	recovery-entries	function, recoveryentries × lebadress × recoveryentry → recoveryentries
]	list-del	partial function, list × nat × elem → list
]	list-del	partial function, list × nat → elem
]	erasequeue-base	partial function, queue × nat × erasequeueentry → queue
]	erasequeue-base	partial function, queue × nat → erasequeueentry
]	vtbl	partial function, vtbl × volid → nat
]	vtbl	function, vtbl × volid × nat → vtbl
]	buffer	partial function, buffer × nat × data → buffer
]	buffer	partial function, buffer × nat → data
]	volumes	partial function, volumes × volid → ebatbl
]	volumes	function, volumes × volid × ebatbl → volumes
]	store	partial function, store × elem → data
]	store	function, store × elem × data → store
]	ebatbl	partial function, ebatbl × nat × ebaentry → ebatbl
]	ebatbl	partial function, ebatbl × nat → ebaentry
]	wlarray-base	partial function, wlarray × nat × wlentry → wlarray
]	wlarray-base	partial function, wlarray × nat → wlentry
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	apebs	partial function, apebs × nat × apeb → apebs
]	apebs	partial function, apebs × nat → apeb
]	nat-list-set	partial function, nat-list × nat × nat → nat-list
]	nat-list-set	partial function, nat-list × nat → nat
]	abstract-volume	partial function, abstract-volume × nat × leb → abstract-volume
]	abstract-volume	partial function, abstract-volume × nat → leb
]	abstract-volumes	partial function, abstract-volumes × volid → abstract-volume
]	abstract-volumes	function, abstract-volumes × volid × abstract-volume → abstract-volumes
]	string	partial function, string × nat × char → string
]	string	partial function, string × nat → char
a	elem	variable, elem
a0	list-data	variable, elem
abs	ubi-abs	predicate, leb × apebs × ebaentry × queue
abs	ubi-abs	predicate, abstract-volumes × apebs × volumes × queue
absf	ubi-abs	function, volid × abstract-volume × apebs × ebatbl × queue × nat → abstract-volume
absf	ubi-abs	function, abstract-volumes × apebs × volumes × queue → abstract-volumes
abstract-volume	abstract-volume	sort,
abstract-volumes	abstract-volumes	sort,
abs○	ubi-abs	predicate, abstract-volumes × apebs × volumes × queue × volid
abs○	ubi-abs	predicate, abstract-volumes × apebs × volumes × queue × volid × nat
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,
avols	abstract-volumes	variable, abstract-volumes
avols0	abstract-volumes	variable, abstract-volumes
avols1	abstract-volumes	variable, abstract-volumes
avols2	abstract-volumes	variable, abstract-volumes
b	elem	variable, elem
bag	nat-bag	variable, nat-bag
bag	bag-basic	variable, bag
bag	bag-basic	sort,
bag0	nat-bag	variable, nat-bag
bag0	bag-basic	variable, bag
bag1	nat-bag	variable, nat-bag
bag1	bag-basic	variable, bag
bag2	nat-bag	variable, nat-bag
bag2	bag-basic	variable, bag
below	wlarray	function, nat-set × nat → nat-set
bflipset	ubi-base	variable, nat-set
bflipset-cons	ubi-base	predicate, nat-set × wlarray
bitflips	aubi-io-asm	variable, bool
bool	bool	sort,
boolvar	bool	variable, bool
boolvar	encoding-volid	variable, bool
boolvar	encoding-nat	variable, bool
boolvar0	bool	variable, bool
boolvar0	encoding-volid	variable, bool
boolvar0	encoding-nat	variable, bool
boolvar1	encoding-volid	variable, bool
boolvar1	encoding-nat	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	erasequeue-base	partial function, nat × queue → queue
butlastn	nat-list-set	partial function, nat × nat-list → nat-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	buffer	partial predicate, buffer × data × nat × nat
cmp	buffer	partial predicate, buffer × nat × buffer × nat × nat
cmp	ebatbl	partial predicate, ebatbl × ebaentry × nat × nat
cmp	ebatbl	partial predicate, ebatbl × nat × ebatbl × nat × nat
cmp	wlarray-base	partial predicate, wlarray × wlentry × nat × nat
cmp	wlarray-base	partial predicate, wlarray × nat × wlarray × nat × nat
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
cmp	apebs	partial predicate, apebs × apeb × nat × nat
cmp	apebs	partial predicate, apebs × nat × apebs × nat × nat
cmp	abstract-volume	partial predicate, abstract-volume × leb × nat × nat
cmp	abstract-volume	partial predicate, abstract-volume × nat × abstract-volume × nat × nat
copy	buffer	partial function, buffer × nat × buffer × nat × nat → buffer
copy	ebatbl	partial function, ebatbl × nat × ebatbl × nat × nat → ebatbl
copy	wlarray-base	partial function, wlarray × nat × wlarray × nat × nat → wlarray
copy	array-copy	partial function, array × nat × array × nat × nat → array
copy	apebs	partial function, apebs × nat × apebs × nat × nat → apebs
copy	abstract-volume	partial function, abstract-volume × nat × abstract-volume × nat × nat → abstract-volume
count	nat-bag	function, nat × nat-bag → nat
count	bag-basic	function, elem × bag → nat
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_nat#	encoding-nat	procedure, nat × buffer : nat × nat : error
decode_volid#	encoding-volid	procedure, nat × buffer : volid × nat : error
decode_vtbl#	encoding-vtbl	procedure, buffer : : vtbl × error
disj	list-dup	predicate, list × list
disj	erasequeue-base	predicate, queue × queue
disj	nat-list-set	predicate, nat-list × nat-list
disj	string	predicate, string × string
dropn	nat-list-set	function, nat × nat-list → nat-list
dropn	list-prefixn	function, nat × list → list
dups	list-dup	predicate, list
dups	erasequeue-base	predicate, queue
dups	nat-list-set	predicate, nat-list
dups	string	predicate, string
ebae	ebaentry	variable, ebaentry
ebae0	ebaentry	variable, ebaentry
ebae1	ebaentry	variable, ebaentry
ebae2	ebaentry	variable, ebaentry
ebaentry	ebaentry	sort,
ebatbl	ebatbl	variable, ebatbl
ebatbl	ebatbl	sort,
ebatbl0	ebatbl	variable, ebatbl
ebatbl1	ebatbl	variable, ebatbl
ebatbl2	ebatbl	variable, ebatbl
ebm-cons	ebm-base	predicate, abstract-volume
ebm-cons	ebm-base	predicate, abstract-volumes
ebm-initial	ebm-base	predicate, abstract-volumes
ebm_change#	ebm-asm	procedure, volid × nat × nat × buffer : abstract-volumes : error
ebm_create_volume#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_erase#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_format#	ebm-asm	procedure, : : abstract-volumes × error
ebm_get_leb_size#	ebm-asm	procedure, abstract-volumes : : nat
ebm_get_page_size#	ebm-asm	procedure, abstract-volumes : : nat
ebm_get_volume_size#	ebm-asm	procedure, volid × abstract-volumes : : nat
ebm_map#	ebm-asm	procedure, volid × nat : abstract-volumes : error
ebm_read#	ebm-asm	procedure, volid × nat × nat × nat × nat × abstract-volumes : buffer : error
ebm_recover#	ebm-asm	procedure, : abstract-volumes : error
ebm_sync_device#	ebm-asm	procedure, abstract-volumes : : error
ebm_unmap#	ebm-asm	procedure, volid × nat : abstract-volumes
ebm_write#	ebm-asm	procedure, volid × nat × nat × nat × nat × buffer : abstract-volumes : error
ecs	ubi-quality-base	function, wlarray × nat → nat-bag
ecs	ubi-quality-base	function, wlarray → nat-bag
elem	elem	sort,
empty	buffer	constant, data
empty	array-splice	constant, elem
empty	avidheader	constant, avidheader
empty	aecheader	constant, aecheader
emptyleb	eraseblock	constant, buffer
emptypage	eraseblock	constant, buffer
emptypeb	eraseblock	constant, buffer
encode#	encoding	procedure, elem × nat : buffer × nat : error
encode_nat#	encoding-nat	procedure, nat × nat : buffer × nat : error
encode_volid#	encoding-volid	procedure, volid × nat : buffer × nat : error
encode_vtbl#	encoding-vtbl	procedure, : vtbl × buffer : error
encoding-size	encoding	function, elem → nat
encoding-size	encoding-volid	function, volid → nat
encoding-size	encoding-nat	function, nat → nat
eq-entry	erasequeueentry	function, nat × lebref → erasequeueentry
eqent	erasequeueentry	variable, erasequeueentry
eqent0	erasequeueentry	variable, erasequeueentry
eqent1	erasequeue-base	variable, erasequeueentry
eqent2	erasequeue-base	variable, erasequeueentry
erase-worker-inv	ubi-base	predicate, apebs × wlarray × nat × error × apebs × volumes × wlarray × queue × erasequeueentry × queue × nat-set × nat × nat
erased	leb	constant, leb
erasequeueentry	erasequeueentry	sort,
erasing	wlstatus	constant, wlstatus
err	error	variable, error
err0	error	variable, error
err1	error	variable, error
erroneous	wlstatus	constant, wlstatus
error	error	sort,
evol	abstract-volume	variable, abstract-volume
evol0	abstract-volume	variable, abstract-volume
evol1	abstract-volume	variable, abstract-volume
evol2	abstract-volume	variable, abstract-volume
f	wlarray-base	variable, wlentry → wlentry
f	array-indices	variable, elem → elem
fail#	error-class	procedure, : : error
fail_or_success#	error-class	procedure, : : error
fill	buffer	partial function, buffer × data × nat × nat → buffer
fill	buffer	function, buffer × data → buffer
fill	ebatbl	partial function, ebatbl × ebaentry × nat × nat → ebatbl
fill	ebatbl	function, ebatbl × ebaentry → ebatbl
fill	wlarray-base	partial function, wlarray × wlentry × nat × nat → wlarray
fill	wlarray-base	function, wlarray × wlentry → wlarray
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
fill	apebs	partial function, apebs × apeb × nat × nat → apebs
fill	apebs	function, apebs × apeb → apebs
fill	abstract-volume	partial function, abstract-volume × leb × nat × nat → abstract-volume
fill	abstract-volume	function, abstract-volume × leb → abstract-volume
fillfirst	list-last	function, nat × elem × list → list
fillfirst	erasequeue-base	function, nat × erasequeueentry × queue → queue
fillfirst	nat-list-set	function, nat × nat × nat-list → nat-list
fillfirst	string	function, nat × char × string → string
filter	list-set	function, list × list → list
filter	erasequeue-base	function, queue × queue → queue
firstn	list-del	partial function, nat × list → list
firstn	erasequeue-base	partial function, nat × queue → queue
firstn	nat-list-set	partial function, nat × nat-list → nat-list
firstn	string	partial function, nat × string → string
fn	array-indices	variable, nat → nat
free	wlstatus	constant, wlstatus
free-ecs	wlarray	function, wlarray × nat → nat-set
free-ecs	wlarray	function, wlarray → nat-set
frome	list-del	function, list × elem → list
frome	erasequeue-base	function, queue × erasequeueentry → queue
frome	nat-list-set	function, nat-list × nat → nat-list
frome	string	function, string × char → string
garbage	avidheader	constant, avidheader
garbage	aecheader	constant, aecheader
id	ubi-base	predicate, apebs × apebs × nat-set
idrange	buffer	partial predicate, buffer × nat × nat
idrange	ebatbl	partial predicate, ebatbl × nat × nat
idrange	wlarray-base	partial predicate, wlarray × nat × nat
idrange	array-copy	partial predicate, array × nat × nat
idrange	apebs	partial predicate, apebs × nat × nat
idrange	abstract-volume	partial predicate, abstract-volume × nat × nat
id○	buffer	predicate, buffer × buffer × nat
id○	ebatbl	predicate, ebatbl × ebatbl × nat
id○	wlarray-base	predicate, wlarray × wlarray × nat
id○	array-copy	predicate, array × array × nat
id○	apebs	predicate, apebs × apebs × nat
id○	abstract-volume	predicate, abstract-volume × abstract-volume × nat
indices-erasing	ubi-crash-recovery-base	predicate, wlarray × nat-list
is-aligned	align	predicate, nat × nat
is-encoded	encoding	predicate, elem × buffer
is-encoded	encoding-volid	predicate, volid × buffer
is-encoded	encoding-nat	predicate, nat × buffer
is-encoded	encoding-vtbl	predicate, vtbl × buffer
is-encoded-rec	encoding-vtbl	predicate, vtbl × buffer
is-garbage	encoding	predicate, buffer
is-garbage-nat	encoding-nat	predicate, buffer
is-garbage-volid	encoding-volid	predicate, buffer
is-max	ubi-crash-recovery-base	predicate, apebs × volumes × wlarray × queue × nat-set × nat × nat
isbad	aubi-io-asm	variable, bool
isempty	eraseblock	predicate, buffer × nat × nat
isempty	eraseblock	predicate, buffer
ladr	lebadress	variable, lebadress
ladr1	recovery-entries	variable, lebadress
ladr2	recovery-entries	variable, lebadress
lastn	list-del	partial function, nat × list → list
lastn	erasequeue-base	partial function, nat × queue → queue
lastn	nat-list-set	partial function, nat × nat-list → nat-list
lastn	string	partial function, nat × string → string
leb	leb	variable, leb
leb	leb	sort,
leb0	abstract-volume	variable, leb
leb1	abstract-volume	variable, leb
lebadress	lebadress	sort,
lebref	lebref	sort,
lebrefset	lebrefset	sort,
list	list-data	sort,
lref	lebref	variable, lebref
lref0	erasequeueentry	variable, lebref
lref0	lebrefset	variable, lebref
lref1	lebrefset	variable, lebref
m	nat-basic	variable, nat
m0	lebadress	variable, nat
m0	lebref	variable, nat
m0	ebaentry	variable, nat
m0	wlentry	variable, nat
m0	array-copy	variable, nat
m0	recovery-entry	variable, nat
m0	aecheader	variable, nat
m1	recovery-entry	variable, nat
m1	avidheader	variable, nat
m2	recovery-entry	variable, nat
m2	avidheader	variable, nat
m3	avidheader	variable, nat
m4	avidheader	variable, nat
m5	avidheader	variable, nat
m6	avidheader	variable, nat
mapped	leb	function, buffer × nat → leb
mapped-pebs	ubi-base	function, volumes → nat-set
max	min-max	function, nat × nat → nat
max-avol	ubi-abs	function, apebs × ebatbl × volid × queue → abstract-volume
max-avols	ubi-abs	function, apebs × volumes × queue → abstract-volumes
min	min-max	function, nat × nat → nat
mkabstractvolume	abstract-volume	function, nat → abstract-volume
mkapebs	apebs	function, nat → apebs
mkarray	array	function, nat → array
mkbuf	buffer	function, nat → buffer
mkebatbl	ebatbl	function, nat → ebatbl
mkemparray	array-splice	function, nat → array
mkempbuf	buffer	function, nat → buffer
mklist	list-last	function, elem × nat → list
mklist	erasequeue-base	function, erasequeueentry × nat → queue
mklist	nat-list-set	function, nat × nat → nat-list
mklist	string	function, char × nat → string
mkpeb	apeb	function, aecheader × avidheader × buffer × nat × bool → apeb
mkwlarray	wlarray-base	function, nat → wlarray
mkzarray	array-splice	function, nat → array
mkzbuf	buffer	function, nat → buffer
n	nat-basic	variable, nat
n0	nat-basic	variable, nat
n1	nat-basic	variable, nat
n2	nat-bag	variable, nat
n2	nat-set	variable, nat
n2	vtbl	variable, nat
n2	ubi-io-pre	variable, nat
n2	nat-list-set	variable, nat
n3	nat-bag	variable, nat
n3	nat-set	variable, nat
n3	vtbl	variable, nat
n3	nat-list-set	variable, nat
n4	nat-bag	variable, nat
n4	nat-set	variable, nat
n4	vtbl	variable, nat
n4	nat-list-set	variable, nat
n5	vtbl	variable, nat
n5	nat-list-set	variable, nat
nat	nat-basic	sort,
nat-bag	nat-bag	sort,
nat-list	nat-list-set	sort,
nat-set	nat-set	sort,
nat-set	nat-list-set	sort,
none	lebref	constant, lebref
ns	nat-set	variable, nat-set
ns	nat-list-set	variable, nat-set
ns0	nat-set	variable, nat-set
ns0	nat-list-set	variable, nat-set
ns1	nat-set	variable, nat-set
ns1	nat-list-set	variable, nat-set
ns2	nat-set	variable, nat-set
ns2	nat-list-set	variable, nat-set
nx	nat-list-set	variable, nat-list
nx0	nat-list-set	variable, nat-list
nx1	nat-list-set	variable, nat-list
ny	nat-list-set	variable, nat-list
nz	nat-list-set	variable, nat-list
pos	list-del	function, elem × list → nat
pos	erasequeue-base	function, erasequeueentry × queue → nat
pos	nat-list-set	function, nat × nat-list → nat
pos	string	function, char × string → nat
prefixn	nat-list-set	function, nat × nat-list → nat-list
prefixn	list-prefixn	function, nat × list → list
q	erasequeue-base	variable, queue
q0	erasequeue-base	variable, queue
q1	erasequeue-base	variable, queue
q2	erasequeue-base	variable, queue
q5	erasequeue-base	variable, queue
queue	erasequeue-base	sort,
range=	buffer	predicate, buffer × nat × buffer × nat × nat
range=	array-splice	predicate, array × nat × array × nat × nat
rec	recovery-entry	variable, recoveryentry
rec0	recovery-entries	variable, recoveryentry
rec1	recovery-entries	variable, recoveryentry
rec2	recovery-entries	variable, recoveryentry
recovery-entry	recovery-entry	function, nat × nat → recoveryentry
recoveryentries	recovery-entries	sort,
recoveryentry	recovery-entry	sort,
recs	recovery-entries	variable, recoveryentries
recs0	recovery-entries	variable, recoveryentries
recs1	recovery-entries	variable, recoveryentries
recs2	recovery-entries	variable, recoveryentries
resize	buffer	function, buffer × nat → buffer
resize	array-splice	function, array × nat → array
restn	list-del	partial function, nat × list → list
restn	erasequeue-base	partial function, nat × queue → queue
restn	nat-list-set	partial function, nat × nat-list → nat-list
restn	string	partial function, nat × string → string
rev	list-last	function, list → list
rev	erasequeue-base	function, queue → queue
rev	buffer	partial function, buffer × nat → buffer
rev	buffer	function, buffer → buffer
rev	ebatbl	partial function, ebatbl × nat → ebatbl
rev	ebatbl	function, ebatbl → ebatbl
rev	wlarray-base	partial function, wlarray × nat → wlarray
rev	wlarray-base	function, wlarray → wlarray
rev	array-copy	partial function, array × nat → array
rev	array-copy	function, array → array
rev	apebs	partial function, apebs × nat → apebs
rev	apebs	function, apebs → apebs
rev	nat-list-set	function, nat-list → nat-list
rev	abstract-volume	partial function, abstract-volume × nat → abstract-volume
rev	abstract-volume	function, abstract-volume → abstract-volume
rev	string	function, string → string
rmdup	list-dup	function, list → list
rmdup	erasequeue-base	function, queue → queue
rmdup	nat-list-set	function, nat-list → nat-list
rmdup	string	function, string → string
s	set-basic	variable, set
s	lebrefset	variable, lebrefset
s0	set-basic	variable, set
s0	lebrefset	variable, lebrefset
s1	set-basic	variable, set
s1	lebrefset	variable, lebrefset
s2	set-basic	variable, set
s2	lebrefset	variable, lebrefset
same-used	wlarray	predicate, wlarray × wlarray
scan-all-inv	ubi-crash-recovery-base	predicate, nat × apebs × recoveryentries × wlarray × queue × nat-set × nat-list × nat × error
set	set-basic	sort,
slice	nat-list-set	function, nat × nat × nat-list → nat-list
slice	list-prefixn	function, nat × nat × list → list
splice	buffer	function, buffer × nat × buffer × nat × nat → buffer
splice	array-splice	function, array × nat × array × nat × nat → array
sqnum	ubi-asm	variable, nat
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
stat	wlstatus	variable, wlstatus
stat0	wlentry	variable, wlstatus
store	store	sort,
str	string	variable, string
str0	string	variable, string
str1	string	variable, string
str2	string	variable, string
str3	string	variable, string
string	string	sort,
subarray	buffer	partial function, buffer × nat × nat → buffer
subarray	ebatbl	partial function, ebatbl × nat × nat → ebatbl
subarray	wlarray-base	partial function, wlarray × nat × nat → wlarray
subarray	array-copy	partial function, array × nat × nat → array
subarray	apebs	partial function, apebs × nat × nat → apebs
subarray	abstract-volume	partial function, abstract-volume × nat × nat → abstract-volume
sublist	list-del	partial function, nat × nat × list → list
sublist	erasequeue-base	partial function, nat × nat × queue → queue
sublist	nat-list-set	partial function, nat × nat × nat-list → nat-list
sublist	string	partial function, nat × nat × string → string
subseteq	recovery-entries	predicate, recoveryentries × recoveryentries
subseteq	volumes	predicate, volumes × volumes
subseteq	abstract-volumes	predicate, abstract-volumes × abstract-volumes
sum-of-differences	ubi-quality-base	function, nat × nat-bag → nat
to-vtbl	vtbl-conv	function, volumes → vtbl
ubi-cons	ubi-base	predicate, apebs × volumes × wlarray × queue × nat-set × nat × nat
ubi-io-erase-pre	ubi-io-pre	predicate, nat × apebs
ubi-io-initial	ubi-io-inv	predicate, apebs
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-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_atomic_leb_change#	ubi-asm	procedure, volid × nat × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_change#	ubi-asm	procedure, volid × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_create_volume#	ubi-asm	procedure, volid × nat × nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_erase#	ubi-asm	procedure, volid × nat × nat × nat : volumes × wlarray × queue × nat-set × apebs : error
ubi_erase_all#	ubi-asm	procedure, volumes × nat-set × nat × nat : wlarray × queue × apebs : error
ubi_erase_worker#	ubi-asm	procedure, : wlarray × queue × apebs
ubi_erase_worker_helper#	ubi-asm	procedure, nat : wlarray × apebs : error
ubi_fix_ecs#	ubi-asm	procedure, nat : nat-list × wlarray
ubi_format#	ubi-asm	procedure, : wlarray × nat × nat × apebs × volumes × queue × nat-set × nat : nat × error
ubi_get_leb_size#	ubi-asm	procedure, nat : : nat
ubi_get_page_size#	ubi-asm	procedure, nat : : nat
ubi_get_pebs_for_wl#	ubi-asm	procedure, wlarray : nat × nat × nat-set : bool
ubi_get_volume_size#	ubi-asm	procedure, volid × volumes : : nat
ubi_init_vols_mappings#	ubi-asm	procedure, nat × apebs : recoveryentries × volumes × wlarray × queue × nat-set
ubi_init_vols_sizes#	ubi-asm	procedure, recoveryentries × wlarray × apebs : vtbl × volumes
ubi_map#	ubi-asm	procedure, volid × nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_next_sqnum#	ubi-asm	procedure, : nat : nat
ubi_read#	ubi-asm	procedure, volid × nat × nat × nat × nat × volumes × nat × apebs : buffer × nat-set : error
ubi_recover#	ubi-asm	procedure, apebs : volumes × wlarray × queue × nat-set × nat × nat × nat : nat × error
ubi_scan_all#	ubi-asm	procedure, nat × apebs : recoveryentries × wlarray × queue × nat-set × nat : nat × nat × nat-list × error
ubi_sync_device#	ubi-asm	procedure, volumes × nat-set × nat × nat : wlarray × queue × apebs : error
ubi_unmap#	ubi-asm	procedure, volid × nat : volumes × wlarray × queue × nat-set
ubi_wear_leveling_worker#	ubi-asm	procedure, nat × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_wl_find_free_max_below#	ubi-asm	procedure, nat × wlarray : nat
ubi_wl_get_free_min#	ubi-asm	procedure, wlarray : nat : bool
ubi_wl_get_peb#	ubi-asm	procedure, : nat × wlarray × queue × apebs : error
ubi_wl_get_used_min#	ubi-asm	procedure, wlarray : nat : bool
ubi_wl_put_peb#	ubi-asm	procedure, lebref × nat : wlarray × queue
ubi_write#	ubi-asm	procedure, volid × nat × nat × nat × nat × buffer × nat : volumes × wlarray × queue × nat-set × nat × nat × apebs : error
ubi_write_multiple#	ubi-asm	procedure, volid × nat × nat × nat × nat × buffer × nat-set × nat : volumes × wlarray × queue × nat × apebs : error
ubi_write_once#	ubi-asm	procedure, volid × nat × nat × nat × nat × buffer : volumes × wlarray × queue × nat × apebs : error
unique-elems	bag-max	predicate, nat-bag
unique-sqns	ubi-base	predicate, apebs
unmapped	ebaentry	constant, ebaentry
unmapped	leb	constant, leb
unmapped-vols	ubi-crash-recovery-base	predicate, volumes
used	wlstatus	constant, wlstatus
used-ecs	wlarray	function, wlarray × nat → nat-set
used-ecs	wlarray	function, wlarray → nat-set
v	volid	variable, volid
v0	volid	variable, volid
v1	volid	variable, volid
v2	volid	variable, volid
valid-ebatbl	ubi-base	predicate, apebs × wlarray × volumes × nat
valid-eraseq	ubi-base	predicate, apebs × queue
valid-eraseq	ubi-base	predicate, wlarray × queue
valid-eraseq	ubi-base	predicate, queue
valid-eraseq-strong	ubi-crash-recovery-base	predicate, apebs × vtbl × queue
valid-eraseq-stronger	ubi-crash-recovery-base	predicate, apebs × queue
valid-global-sqn	ubi-base	predicate, apebs × nat
valid-indices	wlarray-base	predicate, wlarray × nat-list
valid-indices	array-indices	predicate, array × nat-list
valid-leb	ebm-base	predicate, leb
valid-peb	valid-peb	predicate, apeb
valid-peb	valid-peb	predicate, volid × nat × apeb
valid-recs	ubi-crash-recovery-base	predicate, apebs × wlarray × recoveryentries
valid-recs-sqns	ubi-crash-recovery-base	predicate, apebs × recoveryentries
valid-sqns	sqns	function, volid × nat × apebs × nat → nat-bag
valid-sqns	sqns	function, volid × nat × apebs → nat-bag
valid-vtbl	ubi-base	predicate, apebs × volumes × wlarray × nat
valid-vtbl-weak	ubi-crash-recovery-base	predicate, apebs × nat
valid-wl	ubi-base	predicate, apebs × wlarray
valid-wl-entry	ubi-base	predicate, apeb × wlentry
volid	volid	sort,
vols	volumes	variable, volumes
vols0	volumes	variable, volumes
vols1	volumes	variable, volumes
vols2	volumes	variable, volumes
volumes	volumes	sort,
vtbl	vtbl	variable, vtbl
vtbl	vtbl	sort,
vtbl0	vtbl	variable, vtbl
vtbl1	vtbl	variable, vtbl
vtbl2	vtbl	variable, vtbl
vtblpnum	ubi-asm	variable, nat
wl-entry	wlentry	function, nat × wlstatus → wlentry
wlar	wlarray-base	variable, wlarray
wlar0	wlarray-base	variable, wlarray
wlar1	wlarray-base	variable, wlarray
wlar2	wlarray-base	variable, wlarray
wlarray	wlarray-base	sort,
wle	wlentry	variable, wlentry
wle0	wlarray-base	variable, wlentry
wle1	wlarray-base	variable, wlentry
wlentry	wlentry	sort,
wlstatus	wlstatus	sort,
write-once-inv	ubi-base	predicate, apebs × volumes × wlarray × queue × nat-set × nat × nat × volid × nat × nat × nat × buffer × error
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	buffer	constant, data
zero	array-splice	constant, elem
}	nat-bag	function, nat → nat-bag
}	bag-union	function, elem → bag
}	nat-set	function, nat → nat-set
}	set-union	function, elem → set
}	lebrefset	function, lebref → lebrefset
}	nat-list-set	function, nat → nat-set
×	lebadress	function, volid × nat → lebadress
×	lebref	function, volid × nat → lebref
Δ	ubi-quality-base	function, wlarray → nat
φ	array-indices	variable, elem → bool
φn	array-indices	variable, nat → bool
φwlentry	wlarray-base	variable, wlentry → bool
∅	recovery-entries	constant, recoveryentries
∅	nat-bag	constant, nat-bag
∅	bag-basic	constant, bag
∅	nat-set	constant, nat-set
∅	vtbl	constant, vtbl
∅	volumes	constant, volumes
∅	store	constant, store
∅	set-basic	constant, set
∅	lebrefset	constant, lebrefset
∅	nat-list-set	constant, nat-set
∅	abstract-volumes	constant, abstract-volumes
∈	recovery-entries	predicate, lebadress × recoveryentries
∈	erasequeue	predicate, volid × queue
∈	erasequeue	predicate, lebref × queue
∈	erasequeue	predicate, nat × queue
∈	erasequeue-base	predicate, erasequeueentry × queue
∈	list	predicate, elem × list
∈	nat-bag	predicate, nat × nat-bag
∈	bag-union	predicate, elem × bag
∈	nat-set	predicate, nat × nat-set
∈	vtbl	predicate, volid × vtbl
∈	buffer	predicate, data × buffer
∈	volumes	predicate, volid × volumes
∈	store	predicate, elem × store
∈	set-basic	predicate, elem × set
∈	ebatbl	predicate, ebaentry × ebatbl
∈	wlarray-base	predicate, wlentry × wlarray
∈	array-copy	predicate, elem × array
∈	apebs	predicate, apeb × apebs
∈	lebrefset	predicate, lebref × lebrefset
∈	nat-list-set	predicate, nat × nat-set
∈	nat-list-set	predicate, nat × nat-list
∈	abstract-volume	predicate, leb × abstract-volume
∈	abstract-volumes	predicate, volid × abstract-volumes
∈	string	predicate, char × string
∩	nat-set	function, nat-set × nat-set → nat-set
∩	set-union	function, set × set → set
∩	lebrefset	function, lebrefset × lebrefset → lebrefset
∩	nat-list-set	function, nat-set × nat-set → nat-set
∪	list-set	function, list × list → list
∪	erasequeue-base	function, queue × queue → queue
∪	nat-bag	function, nat-bag × nat-bag → nat-bag
∪	bag-union	function, bag × bag → bag
∪	nat-set	function, nat-set × nat-set → nat-set
∪	vtbl	function, vtbl × vtbl → vtbl
∪	set-union	function, set × set → set
∪	store-union	function, store × store → store
∪	lebrefset	function, lebrefset × lebrefset → lebrefset
∪	nat-list-set	function, nat-set × nat-set → nat-set
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⊆	list-set	predicate, list × list
⊆	erasequeue-base	predicate, queue × queue
⊆	nat-bag	predicate, nat-bag × nat-bag
⊆	bag-union	predicate, bag × bag
⊆	ubi-crash-recovery-base	predicate, volumes × volumes
⊆	nat-set	predicate, nat-set × nat-set
⊆	vtbl	predicate, vtbl × vtbl
⊆	store	predicate, store × store
⊆	set-basic	predicate, set × set
⊆	lebrefset	predicate, lebrefset × lebrefset
⊆	nat-list-set	predicate, nat-set × nat-set
⊆	ebm-base	predicate, abstract-volumes × abstract-volumes
⊏	string	predicate, string × string
⊑	list-last	predicate, list × list
⊑	erasequeue-base	predicate, queue × queue
⊑	nat-list-set	predicate, nat-list × nat-list
⊑	string	predicate, string × string
⊒	list-last	predicate, list × list
⊒	erasequeue-base	predicate, queue × queue
⊒	nat-list-set	predicate, nat-list × nat-list
⊒	string	predicate, string × string
⊥	ubi-crash-recovery-base	predicate, recoveryentries × volumes
⊥	vtbl	predicate, vtbl × vtbl
⊥	store-union	predicate, store × store
⌉	ubi-crash-recovery-base	predicate, volumes × volumes × queue
⌋	error-class	predicate, error
⌝	ebaentry	function, nat → ebaentry