[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
# .	icache	f	nat-set → nat
# .	icache	f	icache → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	icache	f	nat-set × nat → nat-set
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	icache	f	icache × nat → icache
. -- .	icache	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .directory	inode	p	inode
. .directory:= .	inode	f	inode × bool → inode
. .dirty	icache-entry	p	icache-entry
. .dirty:= .	icache-entry	f	icache-entry × bool → icache-entry
. .ino	inode	f	inode → nat
. .ino:= .	inode	f	inode × nat → inode
. .inode	icache-entry	f	icache-entry → inode
. .inode:= .	icache-entry	f	icache-entry × inode → icache-entry
. .meta	inode	f	inode → metadata
. .meta:= .	inode	f	inode × metadata → inode
. .nlink	inode	f	inode → nat
. .nlink:= .	inode	f	inode × nat → inode
. .nsubdirs	inode	f	inode → nat
. .nsubdirs:= .	inode	f	inode × nat → inode
. .size	inode	f	inode → nat
. .size:= .	inode	f	inode × nat → inode
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	icache	pf	icache × nat → icache-entry with λ icache, ino. ino ∈ icache
. [ . ]	icache	f	icache × nat × icache-entry → icache
. \ .	icache	f	nat-set × nat-set → nat-set
. \ .	icache	f	icache × nat-set → icache
. \| .	icache	f	icache × nat-set → icache
. ∈ .	icache	p	icache-entry × icache
. ∈ .	icache	p	nat × nat-set
. ∈ .	icache	p	nat × icache
. ∩ .	icache	f	nat-set × nat-set → nat-set
. ∪ .	icache	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	icache	p	nat-set × nat-set
. ⊆ .	icache	p	icache × icache
. ⊕ .	icache	f	icache × icache → icache
{ . }	icache	f	nat → nat-set
∅	icache	c	icache
∅	icache	c	nat-set
boolvar	inode	v	bool
boolvar0	inode	v	bool
dom .	icache	f	icache → nat-set
icache	icache	v	icache
icache	icache	s
icache-entry	icache-entry	s
icache0	icache	v	icache
icache1	icache	v	icache
icache2	icache	v	icache
ie	icache-entry	v	icache-entry
ie0	icache	v	icache-entry
ie1	icache	v	icache-entry
ie2	icache	v	icache-entry
ino	icache	v	nat
ino1	icache	v	nat
ino2	icache	v	nat
inode	inode	s
inode	inode	v	inode
inode0	icache-entry	v	inode
m	nat-basic	v	nat
m0	inode	v	nat
m1	inode	v	nat
m2	inode	v	nat
m3	inode	v	nat
m4	inode	v	nat
m5	inode	v	nat
m6	inode	v	nat
md	metadata	v	metadata
md0	inode	v	metadata
metadata	metadata	s
mkientry	icache-entry	f	bool × inode → icache-entry
mkinode	inode	f	nat × metadata × bool × nat × nat × nat → inode
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
nat-set	icache	s
ns	icache	v	nat-set
ns0	icache	v	nat-set
ns1	icache	v	nat-set
ns2	icache	v	nat-set