Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	linheap	f	heap → nat
. + .	nat-basic	f	nat × nat → nat
. +1	nat-basic	f	nat → nat
. - .	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
. .nxt	lincell	f	cell → Ref
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	linheap	pf	heap × Ref → cell with λ H, r. r ∈ H
. [ . ]	linheap	f	heap × Ref × cell → heap
. ∈ .	linheap	p	Ref × heap
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	linheap	p	heap × heap
∅	linheap	c	heap
H	linheap	v	heap
H0	linheap	v	heap
H1	linheap	v	heap
H2	linheap	v	heap
Ref	Ref	s
ce	lincell	v	cell
ce0	linheap	v	cell
ce1	linheap	v	cell
ce2	linheap	v	cell
cell	lincell	s
heap	linheap	s
m	nat-basic	v	nat
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
null	Ref	c	Ref
r	Ref	v	Ref
r0	linheap	v	Ref
r1	linheap	v	Ref