[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
# .ebatblfebatbl → nat
. + .nat-basicfnat × nat → nat
. +1nat-basicfnat → nat
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. .pnumebaentrypfebaentry → nat with λ ebae. ebae ≠ unmapped
. .pnum:= .ebaentrypfebaentry × nat → ebaentry with λ ebae, m. ebae ≠ unmapped
. < .nat-basicpnat × nat
. > .natpnat × nat
. [ . ]ebatblpfebatbl × nat × ebaentry → ebatbl with λ ebatbl, n, ebae. n < # ebatbl
. [ . ]ebatblpfebatbl × nat → ebaentry with λ ebatbl, n. n < # ebatbl
. ∈ .ebatblpebaentry × ebatbl
. ≤ .natpnat × nat
. ≥ .natpnat × nat
⌜ . ⌝ebaentryfnat → ebaentry
cmpebatblppebatbl × ebaentry × nat × nat with λ ebatbl, ebae, m, n. m + n ≤ # ebatbl
cmpebatblppebatbl × nat × ebatbl × nat × nat with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
copyebatblpfebatbl × nat × ebatbl × nat × nat → ebatbl with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
ebaeebaentryvebaentry
ebae0ebaentryvebaentry
ebae1ebaentryvebaentry
ebae2ebaentryvebaentry
ebaentryebaentrys
ebatblebatbls
ebatblebatblvebatbl
ebatbl0ebatblvebatbl
ebatbl1ebatblvebatbl
ebatbl2ebatblvebatbl
fillebatblpfebatbl × ebaentry × nat × nat → ebatbl with λ ebatbl, ebae, n, m. n + m ≤ # ebatbl
fillebatblfebatbl × ebaentry → ebatbl
id○ebatblpebatbl × ebatbl × nat
idrangeebatblppebatbl × nat × nat with λ ebatbl, m, n. m + n ≤ # ebatbl
mnat-basicvnat
m0array-copyvnat
mkebatblebatblfnat → ebatbl
nnat-basicvnat
n0nat-basicvnat
n1nat-basicvnat
natnat-basics
revebatblpfebatbl × nat → ebatbl with λ ebatbl, n. n ≤ # ebatbl
revebatblfebatbl → ebatbl
subarrayebatblpfebatbl × nat × nat → ebatbl with λ ebatbl, m, n. m + n ≤ # ebatbl
unmappedebaentrycebaentry