[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
# .	store-access	f	store → nat
# .	dataset	f	dataset → nat
# .	set-basic	f	set → nat
. + .	nat-basic2	f	nat × nat → nat
. ++ .	dataset	f	dataset × data → dataset
. ++ .	set-basic	f	set × elem → set
. +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
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	store-base	f	store × elem × data → store
. [ . ]	store-access	f	store × elem → data
. \ .	set-union	f	set × set → set
. \ .	dataset	f	dataset × dataset → dataset
. ∈ .	store-access	p	data × store
. ∈ .	store-access	p	elem × store
. ∈ .	dataset	p	data × dataset
. ∈ .	set-basic	p	elem × set
. ∩ .	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
. ⊆ .	dataset	p	dataset × dataset
. ⊆ .	set-basic	p	set × set
{ . }	set-union	f	elem → set
{ . }	dataset	f	data → dataset
∅	store-base	c	store
∅	set-basic	c	set
∅	dataset	c	dataset
a	elem	v	elem
b	elem	v	elem
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
dom .	store-access	f	store → set
ds	dataset	v	dataset
ds0	dataset	v	dataset
ds1	dataset	v	dataset
ds2	dataset	v	dataset
elem	elem	s
m	nat-basic1	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
ran .	store-access	f	store → dataset
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