[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('a) → nat
# .	store	f	store('a, 'b) → nat
. + .	nat-basic	f	nat × nat → nat
. ++ .	set-basic	f	set('a) × 'a → set('a)
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	set-union	f	set('a) × 'a → set('a)
. -- .	store	f	store('a, 'b) × 'a → store('a, 'b)
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .butmax	oset	pf	set(tord) → set(tord) with λ s. s ≠ ∅
. .butmin	oset	pf	set(tord) → set(tord) with λ s. s ≠ ∅
. .butmin	ostore	pf	store(tord, 'b) → store(tord, 'b) with λ st. st ≠ ∅
. .keys	ostore	f	store(tord, 'b) → set(tord)
. .max	oset	pf	set(tord) → tord with λ s. s ≠ ∅
. .min	oset	pf	set(tord) → tord with λ s. s ≠ ∅
. .min	ostore	pf	store(tord, 'b) → tord with λ st. st ≠ ∅
. < .	nat-basic	p	nat × nat
. < .	tord	p	tord × tord
. < .	oset	p	tord × set(tord)
. < .	oset	p	set(tord) × tord
. > .	nat	p	nat × nat
. [ . := . ]	store	f	store('a, 'b) × 'a × 'b → store('a, 'b)
. [ . ]	store	pf	store('a, 'b) × 'a → 'b with λ st, a. a ∈ st
. \ .	set-union	f	set('a) × set('a) → set('a)
. ∈ .	set-basic	p	'a × set('a)
. ∈ .	store	p	'a × store('a, 'b)
. ∩ .	set-union	f	set('a) × set('a) → set('a)
. ∪ .	set-union	f	set('a) × set('a) → set('a)
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	set-basic	p	set('a) × set('a)
. ⊆ .	store	p	store('a, 'b) × store('a, 'b)
. map .	set-union	f	set('a) × ('a → 'b) → set('b)
{ . }	set-union	f	'a → set('a)
∅	set-basic	c	set('a)
∅	store	c	store('a, 'b)
a	ostore	v	tord
d	ostore	v	'b
disjoint	set-union	p	set('a) × set('a)
filter	set-union	f	set('a) × ('a → bool) → set('a)
nat	nat-basic	s
s	ostore	v	set(tord)
set	set-basic	s
st	ostore	v	store(tord, 'b)
store	store	s
tord	tord	s