[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
# .	directory-tree-inst	f	stringset → nat
# .	fidset	f	fidset → nat
# .	string	f	string → nat
# .	path	f	path → nat
# .	directory-tree-base	f	entries-tree → nat
#n .	directory-tree	f	entries-tree → nat
#n .	directory-tree	f	directory-tree → nat
. '	string	f	char → string
. '	path	f	string → path
. + .	nat-basic	f	nat × nat → nat
. + .	path	f	path × string → path
. + .	string	f	char × string → string
. + .	path	f	path × path → path
. + .	string	f	string × string → string
. + .	path	f	string × path → path
. + .	string	f	string × char → string
. ++ .	directory-tree-inst	f	stringset × string → stringset
. ++ .	fidset	f	fidset × fid → fidset
. ++ .	string	f	string × char → string
. ++ .	path	f	path × string → path
. +1	nat-basic	f	nat → nat
. +2 .	path	f	string × string → path
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	directory-tree-inst	f	stringset × string → stringset
. -- .	directory-tree-base	f	entries-tree × string → entries-tree
. -- .	directory-tree	f	directory-tree × path → directory-tree
. -- .	fidset	f	fidset × fid → fidset
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	path	f	path × string → path
. -l .	string	f	string × char → string
. -l .	path	f	path × string → path
. -p .	string	f	string × nat → string
. -p .	path	f	path × nat → path
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .dir?	directory-tree	p	directory-tree
. .entries	directory-tree	f	directory-tree → entries-tree
. .entries:= .	directory-tree	f	directory-tree × entries-tree → directory-tree
. .fid	directory-tree	f	directory-tree → fid
. .fid:= .	directory-tree	f	directory-tree × fid → directory-tree
. .head	path	pf	path → string with λ p. p ≠ ε
. .last	path	pf	path → string with λ p. p ≠ ε
. .last	string	pf	string → char with λ str. str ≠ ""
. .meta	directory-tree	f	directory-tree → metadata
. .meta:= .	directory-tree	f	directory-tree × metadata → directory-tree
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .subdirs	directory-tree	f	directory-tree → stringset
. .tail	path	pf	path → path with λ p. p ≠ ε
. < .	nat-basic	p	nat × nat
. < .	path	p	path × path
. > .	nat	p	nat × nat
. [ . ]	path	pf	path × nat × string → path with λ p, n, str. n < # p
. [ . ]	path	pf	path × nat → string with λ p, n. n < # p
. [ . ]	directory-tree-base	pf	entries-tree × string → directory-tree with λ sdt, str. str ∈ sdt
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	directory-tree	f	directory-tree × path × directory-tree → directory-tree
. [ . ]	directory-tree-base	f	entries-tree × string × directory-tree → entries-tree
. [ . ]	directory-tree	f	directory-tree × path → directory-tree
. \ .	directory-tree-inst	f	stringset × stringset → stringset
. \ .	fidset	f	fidset × fidset → fidset
. \ .	directory-tree-inst	f	entries-tree × stringset → entries-tree
. \| .	directory-tree-inst	f	entries-tree × stringset → entries-tree
. × .	directory-tree-base	f	string × directory-tree → stringdirectorytree
. ∈ .	directory-tree	p	path × directory-tree
. ∈ .	fidset	p	fid × fidset
. ∈ .	directory-tree-inst	p	string × stringset
. ∈ .	path	p	string × path
. ∈ .	directory-tree-inst	p	directory-tree × entries-tree
. ∈ .	directory-tree-base	p	stringdirectorytree × entries-tree
. ∈ .	string	p	char × string
. ∈ .	directory-tree-base	p	string × entries-tree
. ∩ .	directory-tree-inst	f	stringset × stringset → stringset
. ∩ .	fidset	f	fidset × fidset → fidset
. ∪ .	directory-tree-inst	f	stringset × stringset → stringset
. ∪ .	fidset	f	fidset × fidset → fidset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	fidset	p	fidset × fidset
. ⊆ .	directory-tree-inst	p	stringset × stringset
. ⊆ .	directory-tree-base	p	entries-tree × entries-tree
. ⊑ .	path	p	path × path
. ⊑ .	string	p	string × string
. ⊒ .	path	p	path × path
. ⊒ .	string	p	string × string
. ⊕ .	directory-tree-inst	f	entries-tree × entries-tree → entries-tree
{ . }	directory-tree-inst	f	string → stringset
{ . }	fidset	f	fid → fidset
ε	path	c	path
∅	directory-tree-inst	c	stringset
∅	directory-tree-base	c	entries-tree
∅	fidset	c	fidset
⊏	string	p	string × string
Boolvar	directory-tree-inst	v	bool,flexible
Pentries-tree	directory-tree-inst	v	entries-tree → bool
Ptree	directory-tree	v	directory-tree → bool
boolvar	directory-tree-inst	v	bool
boolvar0	directory-tree-inst	v	bool
boolvar1	directory-tree-inst	v	bool
butlastn	path	pf	nat × path → path with λ n, p. n ≤ # p
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
directory-tree	directory-tree-base	s
disj	path	p	path × path
disj	string	p	string × string
dnode	directory-tree-base	f	metadata × entries-tree → directory-tree
dom .	directory-tree-inst	f	entries-tree → stringset
dups	path	p	path
dups	string	p	string
entries-tree	directory-tree-base	s
fid	file-id	s
fid	file-id	v	fid
fid0	fidset	v	fid
fid1	fidset	v	fid
fids	fidset	v	fidset
fids0	fidset	v	fidset
fids1	fidset	v	fidset
fids2	fidset	v	fidset
fidset	fidset	s
fillfirst	path	f	nat × string × path → path
fillfirst	string	f	nat × char × string → string
firstn	path	pf	nat × path → path with λ n, p. n ≤ # p
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
fnode	directory-tree-base	f	fid → directory-tree
frome	string	f	string × char → string
frome	path	f	path × string → path
lastn	path	pf	nat × path → path with λ n, p. n ≤ # p
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
md	metadata	v	metadata
md0	directory-tree-base	v	metadata
metadata	metadata	s
mklist	string	f	char × nat → string
mkpath	path	f	string × nat → path
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
p	path	v	path
p'	path	v	path
p0	path	v	path
p1	path	v	path
parent	path	pf	path → path with λ p. p ≠ ε
path	path	s
pos	string	f	char × string → nat
pos	path	f	string × path → nat
q	path	v	path
restn	path	pf	nat × path → path with λ n, p. n ≤ # p
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	path	f	path → path
rev	string	f	string → string
rmdup	string	f	string → string
rmdup	path	f	path → path
sdt	directory-tree-base	v	entries-tree
sdt0	directory-tree-base	v	entries-tree
sdt1	directory-tree-base	v	entries-tree
sdt2	directory-tree-base	v	entries-tree
str	string	v	string
str-tree	directory-tree-base	v	stringdirectorytree
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
stringdirectorytree	directory-tree-base	s
strings	directory-tree-inst	v	stringset
strings0	directory-tree-inst	v	stringset
strings1	directory-tree-inst	v	stringset
strings2	directory-tree-inst	v	stringset
stringset	directory-tree-inst	s
sublist	path	pf	nat × nat × path → path with λ n, m, p. n + m ≤ # p
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
tree	directory-tree-base	v	directory-tree
tree0	directory-tree-base	v	directory-tree
tree1	directory-tree-base	v	directory-tree
tree2	directory-tree-base	v	directory-tree