Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	set-basic	f	set → nat
# .	store	f	store → nat
. + .	nat-basic2	f	nat × nat → nat
. ++ .	set-basic	f	set × elem → set
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	set-union	f	set × elem → set
. -- .	store	f	store × elem → store
. -1	nat-basic1	f	nat → nat
. .butmax	oset	f	set → set
. .butmin	ostore	f	store → store
. .butmin	oset	f	set → set
. .keys	ostore	f	store → set
. .max	oset	f	set → elem
. .min	oset	f	set → elem
. .min	ostore	f	store → elem
. < .	oset	p	set × elem
. < .	oset	p	elem × set
. < .	oelem	p	elem × elem
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	store	f	store × elem × data → store
. [ . ]	store	f	store × elem → data
. \ .	set-union	f	set × set → set
. × .	store	f	elem × data → elemdata
. ∈ .	set-basic	p	elem × set
. ∈ .	store	p	elemdata × store
. ∈ .	store	p	elem × store
. ∩ .	set-union	f	set × set → set
. ∪ .	set-union	f	set × set → set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	set-basic	p	set × set
. ⊆ .	store	p	store × store
{ . }	set-union	f	elem → set
∅	store	c	store
∅	set-basic	c	set
a	elem	v	elem
a0	store	v	elem
b	elem	v	elem
c	elem	v	elem
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
elem	elem	s
elemdata	store	s
elemdatavar	store	v	elemdata
m	nat-basic1	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
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	v	store
st0	store	v	store
st1	store	v	store
st2	store	v	store
store	store	s