[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
# .	string	f	string → nat
# .	dir-heap	f	dir-heap → nat
# .	dir-heap	f	nat-set → nat
# .	dir-entries	f	dir-entries → nat
# .	dir-entries	f	stringset → nat
. '	string	f	char → string
. * .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	string	f	string × char → string
. + .	string	f	string × string → string
. ++ .	dir-heap	f	dir-heap × nat → dir-heap
. ++ .	string	f	string × char → string
. ++ .	dir-heap	f	nat-set × nat → nat-set
. ++ .	dir-entries	f	stringset × string → stringset
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -* .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -- .	dir-entries	f	dir-entries × string → dir-entries
. -- .	dir-entries	f	stringset × string → stringset
. -- .	dir-heap	f	dir-heap × nat → dir-heap
. -- .	dir-heap	f	nat-set × nat → nat-set
. -> .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -⊗ .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -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 ≠ ""
. .entries	abstract-dir	f	abstract-dir → dir-entries
. .entries:= .	abstract-dir	f	abstract-dir × dir-entries → abstract-dir
. .last	string	pf	string → char with λ str. str ≠ ""
. .meta	abstract-dir	f	abstract-dir → metadata
. .meta:= .	abstract-dir	f	abstract-dir × metadata → abstract-dir
. .nlink	abstract-dir	f	abstract-dir → nat
. .nlink:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. .nsubdirs	abstract-dir	f	abstract-dir → nat
. .nsubdirs:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	abstract-dir	f	abstract-dir → nat
. .size:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. < .	nat-basic	p	nat × nat
. => .	dir-heap	f	nat × abstract-dir → dir-heap → bool
. =>ad	dir-heap	f	nat → dir-heap → bool
. =>ad?	dir-heap	f	nat → dir-heap → bool
. > .	nat	p	nat × nat
. [ . ]	dir-entries	pf	dir-entries × string → nat with λ entries, str. str ∈ entries
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	dir-entries	f	dir-entries × string × nat → dir-entries
. [ . ]	dir-heap	f	dir-heap × nat × abstract-dir → dir-heap
. [ . ]	dir-heap	f	dir-heap × nat → abstract-dir
. \ .	dir-entries	f	stringset × stringset → stringset
. \ .	dir-heap	f	dir-heap × dir-heap → dir-heap
. \ .	dir-entries	f	dir-entries × stringset → dir-entries
. \ .	dir-heap	f	dir-heap × nat-set → dir-heap
. \ .	dir-heap	f	nat-set × nat-set → nat-set
. \| .	dir-entries	f	dir-entries × stringset → dir-entries
. ∈ .	dir-heap	p	nat × dir-heap
. ∈ .	dir-heap	p	nat × nat-set
. ∈ .	dir-entries	p	nat × dir-entries
. ∈ .	string	p	char × string
. ∈ .	dir-entries	p	string × stringset
. ∈ .	dir-entries	p	string × dir-entries
. ∩ .	dir-entries	f	stringset × stringset → stringset
. ∩ .	dir-heap	f	nat-set × nat-set → nat-set
. ∪ .	dir-entries	f	stringset × stringset → stringset
. ∪ .	dir-heap	f	dir-heap × dir-heap → dir-heap
. ∪ .	dir-heap	f	nat-set × nat-set → nat-set
. ≡ .	dir-heap	p	dir-heap × dir-heap
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	dir-heap	p	(dir-heap → bool) × (dir-heap → bool)
. ⊆ .	dir-heap	p	dir-heap × dir-heap
. ⊆ .	dir-heap	p	nat-set × nat-set
. ⊆ .	dir-entries	p	dir-entries × dir-entries
. ⊆ .	dir-entries	p	stringset × stringset
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
. ⊕ .	dir-entries	f	dir-entries × dir-entries → dir-entries
. ⊗ .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. ⊥ .	dir-heap	p	dir-heap × dir-heap
. and .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. or .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
_∃ .	dir-heap	f	(abstract-dir → dir-heap → bool) → dir-heap → bool
_∃ .	dir-heap	f	(nat → dir-heap → bool) → dir-heap → bool
_∃ .	dir-heap	f	(nat × nat → dir-heap → bool) → dir-heap → bool
{ . }	dir-entries	f	string → stringset
{ . }	dir-heap	f	dir-heap → dir-heap → bool
{ . }	dir-heap	f	nat → nat-set
∅	dir-entries	c	dir-entries
∅	dir-entries	c	stringset
∅	dir-heap	c	nat-set
∅	dir-heap	c	dir-heap
⊏	string	p	string × string
⌜ . ⌝	dir-heap	f	bool → dir-heap → bool
D	dir-heap	v	dir-heap → bool
D0	dir-heap	v	dir-heap → bool
D1	dir-heap	v	dir-heap → bool
D2	dir-heap	v	dir-heap → bool
True	separation	p	bool
abstract-dir	abstract-dir	s
ad	abstract-dir	v	abstract-dir
ad0	dir-heap	v	abstract-dir
ad1	dir-heap	v	abstract-dir
adD	dir-heap	v	abstract-dir → dir-heap → bool
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
bv	heap-sep	v	bool
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
dir-entries	dir-entries	s
dir-heap	dir-heap	s
dirs	dir-heap	v	dir-heap
dirs0	dir-heap	v	dir-heap
dirs1	dir-heap	v	dir-heap
dirs2	dir-heap	v	dir-heap
disj	string	p	string × string
dom .	dir-entries	f	dir-entries → stringset
dups	string	p	string
emp	dir-heap	p	dir-heap
entries	dir-entries	v	dir-entries
entries0	dir-entries	v	dir-entries
entries1	dir-entries	v	dir-entries
entries2	dir-entries	v	dir-entries
false	dir-heap	p	dir-heap
fillfirst	string	f	nat × char × string → string
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
ino	dir-entries	v	nat
ino0	dir-entries	v	nat
ino1	dir-entries	v	nat
ino2	dir-entries	v	nat
ite	dir-heap	f	bool × (dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	abstract-dir	v	nat
m1	abstract-dir	v	nat
m2	abstract-dir	v	nat
m3	abstract-dir	v	nat
m4	abstract-dir	v	nat
md	metadata	v	metadata
md0	abstract-dir	v	metadata
metadata	metadata	s
mkdir	abstract-dir	f	nat × metadata × nat × nat × dir-entries → abstract-dir
mklist	string	f	char × nat → string
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nD	dir-heap	v	nat → dir-heap → bool
nat	nat-basic	s
nat-set	dir-heap	s
nnD	dir-heap	v	nat × nat → dir-heap → bool
not .	dir-heap	f	(dir-heap → bool) → dir-heap → bool
ns	dir-heap	v	nat-set
ns0	dir-heap	v	nat-set
ns1	dir-heap	v	nat-set
ns2	dir-heap	v	nat-set
pos	string	f	char × string → nat
precise	dir-heap	p	(dir-heap → bool)
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
strings	dir-entries	v	stringset
strings0	dir-entries	v	stringset
strings1	dir-entries	v	stringset
strings2	dir-entries	v	stringset
stringset	dir-entries	s
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
true	dir-heap	p	dir-heap