[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
# .	linheap	f	heap → nat
# .	reflist	f	reflist → nat
. % .	nat-div	f	nat × nat → nat
. '	reflist	f	Ref → reflist
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic2	f	nat × nat → nat
. + .	reflist	f	Ref × reflist → reflist
. + .	reflist	f	Ref × Ref → reflist
. + .	reflist	f	reflist × reflist → reflist
. + .	reflist	f	reflist × Ref → reflist
. ++ .	reflist	f	reflist × Ref → reflist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -- .	linheap	f	heap × Ref → heap
. -1	nat-basic1	f	nat → nat
. -1l .	reflist	f	reflist × nat → reflist
. -1l .	reflist	f	reflist × Ref → reflist
. -l .	reflist	f	reflist × Ref → reflist
. .butlast	reflist	f	reflist → reflist
. .last	reflist	f	reflist → Ref
. .nxt	lincell	f	cell → Ref
. / .	nat-div	f	nat × nat → nat
. < .	reflist	p	reflist × reflist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	linheap	f	heap × Ref × cell → heap
. [ . ]	linheap	f	heap × Ref → cell
. [ . ]	reflist	f	reflist × nat → Ref
. [ . ]	reflist	f	reflist × nat × Ref → reflist
. \ .	reflist	f	reflist × reflist → reflist
. ^ .	nat-pot	f	nat × nat → nat
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ∈ .	reflist	p	Ref × reflist
. ∈ .	linheap	p	elemdata × heap
. ∈ .	linheap	p	Ref × heap
. ∪ .	reflist	f	reflist × reflist → reflist
. ⊆ .	reflist	p	reflist × reflist
. ⊆ .	linheap	p	heap × heap
. × .	linheap	f	Ref × cell → elemdata
. ⊑ .	reflist	p	reflist × reflist
. ⊒ .	reflist	p	reflist × reflist
[]	reflist	c	reflist
∅	linheap	c	heap
2^ .	nat-pot	f	nat → nat
butlastn	reflist	f	nat × reflist → reflist
ce	lincell	v	cell
ce0	linheap	v	cell
ce1	linheap	v	cell
ce2	linheap	v	cell
cell	lincell	s
cyclic	cyclic	p	Ref × heap
disj	reflist	p	reflist × reflist
dups	reflist	p	reflist
elemdata	store	s
elemdatavar	store	v	elemdata
fillfirst	reflist	f	nat × Ref × reflist → reflist
filter	reflist	f	reflist × reflist → reflist
firstn	reflist	f	nat × reflist → reflist
frome	reflist	f	reflist × Ref → reflist
H	linheap	v	heap
H0	linheap	v	heap
H1	linheap	v	heap
H2	linheap	v	heap
hd .	reflist	f	reflist → Ref
heap	linheap	s
lastn	reflist	f	nat × reflist → reflist
legal	cyclic	p	heap
log	nat-pot	f	nat × nat → nat
log2 .	nat-pot	f	nat → nat
m	nat-basic2	v	nat
mklist	reflist	f	Ref × nat → reflist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
null	Ref	c	Ref
path	path-reachable	p	reflist × heap
pos	reflist	f	Ref × reflist → nat
r	Ref	v	Ref
r0	reflist	v	Ref
r1	reflist	v	Ref
r2	reflist	v	Ref
reachable	path-reachable	p	Ref × Ref × heap
reachable*	path-reachable	p	heap × Ref × Ref
reachable-1	path-reachable	p	heap × Ref × Ref
reachable-n	path-reachable	p	heap × nat × Ref × Ref
Ref	Ref	s
reflist	reflist	s
restn	reflist	f	nat × reflist → reflist
rev	reflist	f	reflist → reflist
rmdup	reflist	f	reflist → reflist
sublist	reflist	f	nat × nat × reflist → reflist
tl .	reflist	f	reflist → reflist
x	reflist	v	reflist
x0	reflist	v	reflist
x1	reflist	v	reflist
x2	reflist	v	reflist
y	reflist	v	reflist
y0	reflist	v	reflist
y1	reflist	v	reflist
y2	reflist	v	reflist
z	reflist	v	reflist
z0	reflist	v	reflist
z1	reflist	v	reflist
z2	reflist	v	reflist