[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
# .	dcache	f	key-set → nat
# .	dcache	f	dcache → nat
# .	string	f	string → nat
. '	string	f	char → string
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	string	f	string × char → string
. + .	string	f	string × string → string
. ++ .	dcache	f	key-set × key → key-set
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	dcache	f	dcache × key → dcache
. -- .	dcache	f	key-set × key → key-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -l .	string	f	string × char → string
. -p .	string	f	string × nat → string
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .data?	key	p	key
. .dentry?	dentry	p	dentry
. .dentry?	key	p	key
. .ino	dentry	pf	dentry → nat with λ dent. dent.dentry?
. .ino	key	f	key → nat
. .ino:= .	dentry	pf	dentry × nat → dentry with λ dent, m. dent.dentry?
. .ino:= .	key	f	key × nat → key
. .inode?	key	p	key
. .last	string	pf	string → char with λ str. str ≠ ""
. .name	key	pf	key → string with λ key. key.dentry?
. .name	dentry	f	dentry → string
. .name:= .	key	pf	key × string → key with λ key, str. key.dentry?
. .name:= .	dentry	f	dentry × string → dentry
. .negdentry?	dentry	p	dentry
. .part	key	pf	key → nat with λ key. key.data?
. .part:= .	key	pf	key × nat → key with λ key, m. key.data?
. .rstring	string	pf	string → string with λ str. str ≠ ""
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	dcache	pf	dcache × key → dentry with λ dcache, key. key ∈ dcache
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	dcache	f	dcache × key × dentry → dcache
. \ .	dcache	f	key-set × key-set → key-set
. \ .	dcache	f	dcache × key-set → dcache
. \| .	dcache	f	dcache × key-set → dcache
. ∈ .	dcache	p	dentry × dcache
. ∈ .	dcache	p	key × key-set
. ∈ .	dcache	p	key × dcache
. ∈ .	string	p	char × string
. ∩ .	dcache	f	key-set × key-set → key-set
. ∪ .	dcache	f	key-set × key-set → key-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	dcache	p	key-set × key-set
. ⊆ .	dcache	p	dcache × dcache
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
. ⊕ .	dcache	f	dcache × dcache → dcache
{ . }	dcache	f	key → key-set
∅	dcache	c	dcache
∅	dcache	c	key-set
⊏	string	p	string × string
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
datakey	key	f	nat × nat → key
dcache	dcache	s
dcache	dcache	v	dcache
dcache0	dcache	v	dcache
dcache1	dcache	v	dcache
dcache2	dcache	v	dcache
dent	dentry	v	dentry
dent0	dcache	v	dentry
dent1	dcache	v	dentry
dent2	dcache	v	dentry
dentry	dentry	s
dentrykey	key	f	nat × string → key
disj	string	p	string × string
dom .	dcache	f	dcache → key-set
dups	string	p	string
fillfirst	string	f	nat × char × string → string
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
inodekey	key	f	nat → key
key	key	s
key	key	v	key
key-set	dcache	s
key1	dcache	v	key
key2	dcache	v	key
ks	dcache	v	key-set
ks0	dcache	v	key-set
ks1	dcache	v	key-set
ks2	dcache	v	key-set
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	dentry	v	nat
m1	key	v	nat
m2	key	v	nat
mkdentry	dentry	f	string × nat → dentry
mklist	string	f	char × nat → string
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
negdentry	dentry	f	string → dentry
pos	string	f	char × string → nat
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	string	f	string → string
rmdup	string	f	string → string
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str