Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	store	f	Map → Nat
# .	set-basic	f	Set → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. ++ .	set-basic	f	Set × Elem → Set
. +1	nat-basic	f	Nat → Nat
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -- .	store	f	Map × Elem → Map
. -- .	set-union	f	Set × Elem → Set
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. .butmax	oset	pf	Set → Set with λ s. s ≠ ∅
. .butmin	oset	pf	Set → Set with λ s. s ≠ ∅
. .butmin	ostore	pf	Map → Map with λ st. st ≠ ∅
. .keys	ostore	f	Map → Set
. .max	oset	pf	Set → Elem with λ s. s ≠ ∅
. .min	oset	pf	Set → Elem with λ s. s ≠ ∅
. .min	ostore	pf	Map → Elem with λ st. st ≠ ∅
. < .	oelem	p	Elem × Elem
. < .	nat-basic	p	Nat × Nat
. < .	oset	p	Elem × Set
. < .	oset	p	Set × Elem
. > .	nat	p	Nat × Nat
. [ . ]	store	f	Map × Elem × Data → Map
. [ . ]	store	pf	Map × Elem → Data with λ st, a. a ∈ st
. \ .	set-union	f	Set × Set → Set
. ∈ .	store	p	Elem × Map
. ∈ .	set-basic	p	Elem × Set
. ∩ .	set-union	f	Set × Set → Set
. ∪ .	set-union	f	Set × Set → Set
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	store	p	Map × Map
. ⊆ .	set-basic	p	Set × Set
{ . }	set-union	f	Elem → Set
∅	store	c	Map
∅	set-basic	c	Set
Data	data	s
Elem	elem	s
Map	store	s
Nat	nat-basic	s
Set	set-basic	s
a	ostore	v	Elem
d	ostore	v	Data
disjoint	set-union	p	Set × Set
n	ostore	v	Nat
st	ostore	v	Map