[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
# .	volumes	f	volumes → nat
# .	ebatbl	f	ebatbl → nat
. + .	nat-basic	f	nat × nat → nat
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	volumes	f	volumes × volid → volumes
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .pnum	ebaentry	pf	ebaentry → nat with λ ebae. ebae ≠ unmapped
. .pnum:= .	ebaentry	pf	ebaentry × nat → ebaentry with λ ebae, m. ebae ≠ unmapped
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	volumes	pf	volumes × volid → ebatbl with λ vols, v. v ∈ vols
. [ . ]	volumes	f	volumes × volid × ebatbl → volumes
. [ . ]	ebatbl	pf	ebatbl × nat × ebaentry → ebatbl with λ ebatbl, n, ebae. n < # ebatbl
. [ . ]	ebatbl	pf	ebatbl × nat → ebaentry with λ ebatbl, n. n < # ebatbl
. ∈ .	ebatbl	p	ebaentry × ebatbl
. ∈ .	volumes	p	volid × volumes
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. subseteq .	volumes	p	volumes × volumes
∅	volumes	c	volumes
⌜ . ⌝	ebaentry	f	nat → ebaentry
cmp	ebatbl	pp	ebatbl × ebaentry × nat × nat with λ ebatbl, ebae, m, n. m + n ≤ # ebatbl
cmp	ebatbl	pp	ebatbl × nat × ebatbl × nat × nat with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
copy	ebatbl	pf	ebatbl × nat × ebatbl × nat × nat → ebatbl with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
ebae	ebaentry	v	ebaentry
ebae0	ebaentry	v	ebaentry
ebae1	ebaentry	v	ebaentry
ebae2	ebaentry	v	ebaentry
ebaentry	ebaentry	s
ebatbl	ebatbl	s
ebatbl	ebatbl	v	ebatbl
ebatbl0	ebatbl	v	ebatbl
ebatbl1	ebatbl	v	ebatbl
ebatbl2	ebatbl	v	ebatbl
fill	ebatbl	pf	ebatbl × ebaentry × nat × nat → ebatbl with λ ebatbl, ebae, n, m. n + m ≤ # ebatbl
fill	ebatbl	f	ebatbl × ebaentry → ebatbl
id○	ebatbl	p	ebatbl × ebatbl × nat
idrange	ebatbl	pp	ebatbl × nat × nat with λ ebatbl, m, n. m + n ≤ # ebatbl
m	nat-basic	v	nat
m0	array-copy	v	nat
mkebatbl	ebatbl	f	nat → ebatbl
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
rev	ebatbl	pf	ebatbl × nat → ebatbl with λ ebatbl, n. n ≤ # ebatbl
rev	ebatbl	f	ebatbl → ebatbl
subarray	ebatbl	pf	ebatbl × nat × nat → ebatbl with λ ebatbl, m, n. m + n ≤ # ebatbl
unmapped	ebaentry	c	ebaentry
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
volid	volid	s
vols	volumes	v	volumes
vols0	volumes	v	volumes
vols1	volumes	v	volumes
vols2	volumes	v	volumes
volumes	volumes	s