[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
# .	set-basic	f	set → nat
# .	list-data	f	list → nat
# .	dataset	f	dataset → nat
# .	store-access	f	store → nat
. '	list	f	elem → list
. + .	nat-basic2	f	nat × nat → nat
. + .	list	f	elem × elem → list
. + .	list-data	f	elem × list → list
. + .	list	f	list × elem → list
. + .	list	f	list × list → list
. ++ .	list-dup	f	list × elem → list
. ++ .	set-basic	f	set × elem → set
. ++ .	dataset	f	dataset × data → dataset
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	store-access	f	store × elem → store
. -- .	set-union	f	set × elem → set
. -- .	dataset	f	dataset × data → dataset
. -1	nat-basic1	f	nat → nat
. -1l .	list-del	f	list × nat → list
. -1l .	list-del	f	list × elem → list
. -l .	list-del	f	list × elem → list
. .butlast	list-last	f	list → list
. .first	list-data	f	list → elem
. .last	list-last	f	list → elem
. .rest	list-data	f	list → list
. < .	list-data	p	list × list
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	store-base	f	store × elem × data → store
. [ . ]	list-del	f	list × nat × elem → list
. [ . ]	store-access	f	store × elem → data
. [ . ]	list-del	f	list × nat → elem
. \ .	set-union	f	set × set → set
. \ .	dataset	f	dataset × dataset → dataset
. ∈ .	list	p	elem × list
. ∈ .	store-access	p	data × store
. ∈ .	set-basic	p	elem × set
. ∈ .	store-access	p	elem × store
. ∈ .	dataset	p	data × dataset
. ∩ .	set-union	f	set × set → set
. ∩ .	dataset	f	dataset × dataset → dataset
. ∪ .	set-union	f	set × set → set
. ∪ .	dataset	f	dataset × dataset → dataset
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	store-access	p	store × store
. ⊆ .	set-basic	p	set × set
. ⊆ .	dataset	p	dataset × dataset
. ⊑ .	list-last	p	list × list
. ⊒ .	list-last	p	list × list
[]	list-data	c	list
{ . }	dataset	f	data → dataset
{ . }	set-union	f	elem → set
∅	store-base	c	store
∅	set-basic	c	set
∅	dataset	c	dataset
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	list-last	f	nat × list → list
c	elem	v	elem
d	dataset	v	data
d0	dataset	v	data
d1	dataset	v	data
d2	data	v	data
data	dataset	s
dataset	dataset	s
disj	list-dup	p	list × list
dom .	store-access	f	store → set
ds	dataset	v	dataset
ds0	dataset	v	dataset
ds1	dataset	v	dataset
ds2	dataset	v	dataset
dups	list-dup	p	list
elem	elem	s
fillfirst	list-last	f	nat × elem × list → list
firstn	list-del	f	nat × list → list
frome	list-del	f	list × elem → list
iter .	store-iter	f	store → list
lastn	list-del	f	nat × list → list
list	list-data	s
m	nat-basic1	v	nat
mklist	list-last	f	elem × nat → list
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
pos	list-del	f	elem × list → nat
ran .	store-access	f	store → dataset
restn	list-del	f	nat × list → list
rev	list-last	f	list → list
rmdup	list-dup	f	list → list
s	set-basic	v	set
s0	set-basic	v	set
s1	set-basic	v	set
s2	set-basic	v	set
set	set-basic	s
st	store-base	v	store
st0	store-base	v	store
st1	store-base	v	store
st2	store-base	v	store
store	store-base	s
sublist	list-del	f	nat × nat × list → list
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list