[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
# .	nat-store	f	nat-set → nat
# .	store	f	store → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	nat-store	f	nat-set × nat → nat-set
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	nat-store	f	store × nat → store
. -- .	nat-store	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .map ( . )	store-map	f	store × (data → data) → store
. .map ( . )	nat-store	f	store × (nat × data → data) → store
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	nat-store	pf	store × nat → data with λ st, n. n ∈ st
. [ . ]	nat-store	f	store × nat × data → store
. \ .	nat-store	f	nat-set × nat-set → nat-set
. \ .	nat-store	f	store × nat-set → store
. \| .	nat-store	f	store × nat-set → store
. ∈ .	store+set	p	data × store
. ∈ .	nat-store	p	nat × nat-set
. ∈ .	nat-store	p	nat × store
. ∩ .	nat-store	f	nat-set × nat-set → nat-set
. ∪ .	nat-store	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	nat-store	p	nat-set × nat-set
. ⊆ .	store	p	store × store
. ⊕ .	store+set	f	store × store → store
{ . }	nat-store	f	nat → nat-set
∅	store	c	store
∅	nat-store	c	nat-set
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
dataf	store-map	v	data → data
dom .	nat-store	f	store → nat-set
elemdataf	nat-store	v	nat × data → data
m	nat-basic	v	nat
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	nat-store	v	nat
n3	nat-store	v	nat
n4	nat-store	v	nat
nat	nat-basic	s
nat-set	nat-store	s
ns	nat-store	v	nat-set
ns0	nat-store	v	nat-set
ns1	nat-store	v	nat-set
ns2	nat-store	v	nat-set
st	store	v	store
st0	store	v	store
st1	store	v	store
st2	store	v	store
store	store	s