[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 → nat
# .	successors	f	successors → 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
. -- .	successors	f	successors × elem → successors
. -1	nat-basic1	f	nat → nat
. .edges	node	f	node → successors
. .edges:= .	node	f	node × successors → node
. .value	node	f	node → elem
. .value:= .	node	f	node × elem → node
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	successors	f	successors × elem × ref → successors
. [ . ]	successors	f	successors × elem → ref
. \ .	successors	f	successors × set → successors
. \ .	set-union	f	set × set → set
. × .	successors	f	elem × ref → elemref
. ∈ .	successors	p	ref × successors
. ∈ .	set-basic	p	elem × set
. ∈ .	successors	p	elemref × successors
. ∈ .	successors	p	elem × successors
. ∩ .	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
. ⊆ .	successors	p	successors × successors
{ . }	set-union	f	elem → set
∅	successors	c	successors
∅	set-basic	c	set
Node	node	f	elem × successors → node
a	elem	v	elem
a0	store	v	elem
b	elem	v	elem
c	elem	v	elem
dom .	successors	f	successors → set
elem	elem	s
elemref	successors	s
elemrefvar	successors	v	elemref
m	nat-basic2	v	nat
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
nd	node	v	node
node	node	s
null	ref	c	ref
r	ref	v	ref
r0	ref	v	ref
r1	ref	v	ref
r2	successors	v	ref
ref	ref	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
succ	successors	v	successors
succ0	successors	v	successors
succ1	successors	v	successors
succ2	successors	v	successors
successors	successors	s