[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
# .bufferfbuffer → nat
# .file-heapffile-heap → nat
# .file-contentffile-content → nat
# .file-heapfnat-set → nat
. * .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. + .nat-basicfnat × nat → nat
. + .bufferfbuffer × buffer → buffer
. ++ .file-heapffile-heap × nat → file-heap
. ++ .file-heapfnat-set × nat → nat-set
. +1nat-basicfnat → nat
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -* .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -- .file-contentffile-content × nat → file-content
. -- .file-heapfnat-set × nat → nat-set
. -- .file-heapffile-heap × nat → file-heap
. -> .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -⊗ .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. .contentabstract-filefabstract-file → file-content
. .content:= .abstract-filefabstract-file × file-content → abstract-file
. .metaabstract-filefabstract-file → metadata
. .meta:= .abstract-filefabstract-file × metadata → abstract-file
. .nlinkabstract-filefabstract-file → nat
. .nlink:= .abstract-filefabstract-file × nat → abstract-file
. .sizeabstract-filefabstract-file → nat
. .size:= .abstract-filefabstract-file × nat → abstract-file
. < .nat-basicpnat × nat
. => .file-heapfnat × abstract-file → file-heap → bool
. =>affile-heapfnat → file-heap → bool
. =>af?file-heapfnat → file-heap → bool
. > .natpnat × nat
. [ . ]file-contentpffile-content × nat → buffer with λ content, n. n ∈ content
. [ . ]bufferpfbuffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]bufferpfbuffer × nat → data with λ buf, n. n < # buf
. [ . ]file-contentffile-content × nat × buffer → file-content
. [ . ]file-heapffile-heap × nat × abstract-file → file-heap
. [ . ]file-heapffile-heap × nat → abstract-file
. \ .file-heapfnat-set × nat-set → nat-set
. \ .file-heapffile-heap × file-heap → file-heap
. \ .file-heapffile-heap × nat-set → file-heap
. ∈ .file-heappnat × file-heap
. ∈ .file-heappnat × nat-set
. ∈ .file-contentpnat × file-content
. ∈ .bufferpdata × buffer
. ∩ .file-heapfnat-set × nat-set → nat-set
. ∪ .file-heapfnat-set × nat-set → nat-set
. ∪ .file-heapffile-heap × file-heap → file-heap
. ≡ .file-heappfile-heap × file-heap
. ≤ .natpnat × nat
. ≥ .natpnat × nat
. ⊆ .file-heapp(file-heap → bool) × (file-heap → bool)
. ⊆ .file-heappfile-heap × file-heap
. ⊆ .file-contentpfile-content × file-content
. ⊆ .file-heappnat-set × nat-set
. ⊗ .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. ⊥ .file-heappfile-heap × file-heap
. and .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
. or .file-heapf(file-heap → bool) × (file-heap → bool) → file-heap → bool
_∃ .file-heapf(abstract-file → file-heap → bool) → file-heap → bool
_∃ .file-heapf(nat → file-heap → bool) → file-heap → bool
_∃ .file-heapf(nat × nat → file-heap → bool) → file-heap → bool
{ . }file-heapfnat → nat-set
{ . }file-heapffile-heap → file-heap → bool
∅file-contentcfile-content
∅file-heapcnat-set
∅file-heapcfile-heap
⌜ . ⌝file-heapfbool → file-heap → bool
Ffile-heapvfile-heap → bool
F0file-heapvfile-heap → bool
F1file-heapvfile-heap → bool
F2file-heapvfile-heap → bool
Trueseparationpbool
VFS_PAGE_SIZEpagecnat
abstract-fileabstract-files
adFfile-heapvabstract-file → file-heap → bool
afabstract-filevabstract-file
af0file-heapvabstract-file
af1file-heapvabstract-file
bufbuffervbuffer
buf0buffervbuffer
buf1buffervbuffer
buf2buffervbuffer
bufferbuffers
bvheap-sepvbool
cmpbufferppbuffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmpbufferppbuffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
contentfile-contentvfile-content
content0file-contentvfile-content
content1file-contentvfile-content
content2file-contentvfile-content
copybufferpfbuffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
ddatavdata
d0datavdata
d1datavdata
d2datavdata
datadatas
empfile-heappfile-heap
emptybuffercdata
falsefile-heappfile-heap
file-contentfile-contents
file-heapfile-heaps
filesfile-heapvfile-heap
files0file-heapvfile-heap
files1file-heapvfile-heap
files2file-heapvfile-heap
fillbufferpfbuffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fillbufferfbuffer × data → buffer
id○bufferpbuffer × buffer × nat
idrangebufferppbuffer × nat × nat with λ buf, m, n. m + n ≤ # buf
inofile-heapvnat
ino0file-heapvnat
ino1file-heapvnat
itefile-heapfbool × (file-heap → bool) × (file-heap → bool) → file-heap → bool
mnat-basicvnat
m0array-copyvnat
m1abstract-filevnat
m2abstract-filevnat
maxmin-maxfnat × nat → nat
mdmetadatavmetadata
md0abstract-filevmetadata
metadatametadatas
minmin-maxfnat × nat → nat
mkbufbufferfnat → buffer
mkempbufbufferfnat → buffer
mkfileabstract-filefnat × metadata × nat × file-content → abstract-file
mkzbufbufferfnat → buffer
nnat-basicvnat
n0nat-basicvnat
n1nat-basicvnat
n2file-contentvnat
n3file-contentvnat
n4file-contentvnat
nFfile-heapvnat → file-heap → bool
natnat-basics
nat-setfile-heaps
nnFfile-heapvnat × nat → file-heap → bool
not .file-heapf(file-heap → bool) → file-heap → bool
nsfile-heapvnat-set
ns0file-heapvnat-set
ns1file-heapvnat-set
ns2file-heapvnat-set
precisefile-heapp(file-heap → bool)
range=bufferpbuffer × nat × buffer × nat × nat
resizebufferfbuffer × nat → buffer
revbufferpfbuffer × nat → buffer with λ buf, n. n ≤ # buf
revbufferfbuffer → buffer
splicebufferfbuffer × nat × buffer × nat × nat → buffer
subarraybufferpfbuffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
truefile-heappfile-heap
zerobuffercdata
zeropagepagecbuffer