[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
. '	reflist	f	Ref → reflist
. + .	nat-basic	f	nat × nat → nat
. + .	reflist	f	reflist × Ref → reflist
. + .	reflist	f	Ref × reflist → reflist
. + .	reflist	f	reflist × reflist → reflist
. ++ .	reflist	f	reflist × Ref → reflist
. +1	nat-basic	f	nat → nat
. +2 .	reflist	f	Ref × Ref → reflist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	linheap	f	heap × Ref → heap
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	reflist	f	reflist × Ref → reflist
. -l .	reflist	f	reflist × Ref → reflist
. -p .	reflist	f	reflist × nat → reflist
. .butlast	reflist	pf	reflist → reflist with λ x0. x0 ≠ []
. .last	reflist	pf	reflist → Ref with λ x0. x0 ≠ []
. .nxt	lincell	f	cell → Ref
. < .	reflist	p	reflist × reflist
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	reflist	pf	reflist × nat × Ref → reflist with λ x0, n, r. n < # x0
. [ . ]	reflist	pf	reflist × nat → Ref with λ x0, n. n < # x0
. [ . ]	linheap	pf	heap × Ref → cell with λ H, r. r ∈ H
. [ . ]	linheap	f	heap × Ref × cell → heap
. \ .	reflist	f	reflist × reflist → reflist
. ∈ .	reflist	p	Ref × reflist
. ∈ .	linheap	p	Ref × heap
. ∪ .	reflist	f	reflist × reflist → reflist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	reflist	p	reflist × reflist
. ⊆ .	linheap	p	heap × heap
. ⊑ .	reflist	p	reflist × reflist
. ⊒ .	reflist	p	reflist × reflist
[]	reflist	c	reflist
∅	linheap	c	heap
H	linheap	v	heap
H0	linheap	v	heap
H1	linheap	v	heap
H2	linheap	v	heap
Ref	Ref	s
butlastn	reflist	pf	nat × reflist → reflist with λ n, x0. n ≤ # x0
ce	lincell	v	cell
ce0	linheap	v	cell
ce1	linheap	v	cell
ce2	linheap	v	cell
cell	lincell	s
disj	reflist	p	reflist × reflist
dups	reflist	p	reflist
fillfirst	reflist	f	nat × Ref × reflist → reflist
filter	reflist	f	reflist × reflist → reflist
firstn	reflist	pf	nat × reflist → reflist with λ n, x0. n ≤ # x0
frome	reflist	f	reflist × Ref → reflist
hd .	reflist	pf	reflist → Ref with λ x0. x0 ≠ []
heap	linheap	s
lastn	reflist	pf	nat × reflist → reflist with λ n, x0. n ≤ # x0
m	nat-basic	v	nat
mklist	reflist	f	Ref × nat → reflist
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
null	Ref	c	Ref
path	path-reachable	p	reflist × heap
pos	reflist	f	Ref × reflist → nat
r	Ref	v	Ref
r0	linheap	v	Ref
r1	linheap	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
reflist	reflist	s
restn	reflist	pf	nat × reflist → reflist with λ n, x0. n ≤ # x0
rev	reflist	f	reflist → reflist
rmdup	reflist	f	reflist → reflist
sublist	reflist	pf	nat × nat × reflist → reflist with λ n, m, x0. n + m ≤ # x0
tl .	reflist	pf	reflist → reflist with λ x0. x0 ≠ []
x	reflist	v	reflist
x0	reflist	v	reflist
x1	reflist	v	reflist
y	reflist	v	reflist
z	reflist	v	reflist