[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
!	separation-rg	function, Id × Ref[A] → Id × Heap[A] → Bool → Heap[A] → Bool
#	map	function, Map[A, B] → Nat
#	heap	function, Heap[A] → Nat
#	heap-old	function, Heap[A] → Nat
#	set-basic	function, Set[A] → Nat
#	list-data	function, List[A] → Nat
#	tree	function, Tree[A] → Nat
'	list	function, A → List[A]
*	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
*	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
*	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
+	nat-basic	function, Nat × Nat → Nat
+	list-data	function, A × List[A] → List[A]
+	list	function, List[A] × A → List[A]
+	list	function, List[A] × List[A] → List[A]
++	list-dup	function, List[A] × A → List[A]
++	heap	partial function, Heap[A] × Ref[A] → Heap[A]
++	heap-old	partial function, Heap[A] × Ref[A] → Heap[A]
++	set-basic	function, Set[A] × A → Set[A]
+1	nat-basic	function, Nat → Nat
+2	list	function, A × A → List[A]
+h	heapmap	partial function, Map[Ref[A], A] × Ref[A] → Map[Ref[A], A]
-	nat	partial function, Nat × Nat → Nat
-*	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
-*	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
-*	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
--	set-union	function, Set[A] × A → Set[A]
--	map	function, Map[A, B] × A → Map[A, B]
--	heap	partial function, Heap[A] × Ref[A] → Heap[A]
--	heap-old	partial function, Heap[A] × Ref[A] → Heap[A]
--h	heapmap	partial function, Map[Ref[A], A] × Ref[A] → Map[Ref[A], A]
-1	nat-basic	partial function, Nat → Nat
-⊗	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
-⊗	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
-⊗	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
. ( . )	map	partial function, Map[A, B] × A → B
. ( . )	heap	partial function, Heap[A] × Ref[A] → A
. ( . )	tree-path	partial function, Tree[A] × List[Bool] → Tree[A]
. ( . )	heap-old	partial function, Heap[A] × Ref[A] → A
. ( . := . )	map	function, Map[A, B] × A × B → Map[A, B]
. ( . := . )	heap	partial function, Heap[A] × Ref[A] × A → Heap[A]
. ( . := . )	tree-path	partial function, Tree[A] × List[Bool] × Tree[A] → Tree[A]
. ( . := . )	heap-old	partial function, Heap[A] × Ref[A] × A → Heap[A]
<	nat-basic	predicate, Nat × Nat
<	list-data	predicate, List[A] × List[A]
==>	heap-aux	function, Ref[(A, B)] × A × B → Heap[(A, B)] → Bool
=>	refmap-maplet	function, Ref[A] × A → Map[Ref[A], A] → Bool
=>	map-maplet	function, A × B → Map[A, B] → Bool
=>	maplet	function, Ref[A] × A → Heap[A] → Bool
=>	heap-is-map-instance	function, Ref[A] × A → Map[Ref[A], A] → Bool
=>?	refmap-ex-maplet	function, Ref[A] → Map[Ref[A], A] → Bool
=>?	heap-is-map-instance	function, Ref[A] → Map[Ref[A], A] → Bool
=>?	ex-maplet	function, Ref[A] → Heap[A] → Bool
=>_	map-ex-maplet	function, A → Map[A, B] → Bool
=>_	refmap-ex-maplet	function, Ref[A] → Map[Ref[A], A] → Bool
=>_	heap-is-map-instance	function, Ref[A] → Map[Ref[A], A] → Bool
=>_	ex-maplet	function, Ref[A] → Heap[A] → Bool
>	nat	predicate, Nat × Nat
Cell	cellparam	sort,
Cell	cell	sort,
Heap	heap	sort,
Heap	heap-old	sort,
Id	ownership	sort,
IdxO	gownership	sort,
List	list-data	sort,
Map	map	sort,
Nat	nat-basic	sort,
Node	node	sort,
O	gownership	function, IdxO[A] → Ref[A] → Id
Ref	polyref	sort,
Set	set-basic	sort,
Tree	tree	sort,
True	refmap-separation	predicate, Bool
True	separation	predicate, Bool
True	map-separation	predicate, Bool
[]	list-data	constant, List[A]
\	heapfuns-map	function, Map[A, B] × Map[A, B] → Map[A, B]
\	heapfuns-map	function, Map[A, B] × Set[A] → Map[A, B]
\	set-union	function, Set[A] × Set[A] → Set[A]
\	heapfuns	function, Heap[A] × Heap[A] → Heap[A]
\	heapfuns	function, Heap[A] × Set[Ref[A]] → Heap[A]
\	heap-old	function, Heap[A] × Heap[A] → Heap[A]
\	heap-old	function, Heap[A] × Set[Ref[A]] → Heap[A]
\	heap-is-map-instance	function, Map[Ref[A], A] × Map[Ref[A], A] → Map[Ref[A], A]
\	heap-is-map-instance	function, Map[Ref[A], A] × Set[Ref[A]] → Map[Ref[A], A]
]	heap-aux	predicate, Heap[(A, B)] → Bool × Set[Ref[(A, B)]] × Ref[(A, B)] → A × Ref[(A, B)] → B
]	heap-aux	function, Heap[(A, B)] × Ref[(A, B)] × A × B → Heap[(A, B)]
]	heap-fun	predicate, Heap[A] → Bool × Set[Ref[A]] × Ref[A] → A
]a	heap-aux	function, Heap[(A, B)] × Ref[(A, B)] → B
]h	heapmap	partial function, Map[Ref[A], A] × Ref[A] × A → Map[Ref[A], A]
]h	heapmap	partial function, Map[Ref[A], A] × Ref[A] → A
]o	heap-aux	function, Heap[(A, B)] × Ref[(A, B)] → A
^*	relops	function, A × A → Bool → A × A → Bool
^-1	relops	function, A × B → Bool → B × A → Bool
_∃	refmap-maplet	function, B × C → Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
_∃	refmap-maplet	function, B → Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
_∃	map-maplet	function, C × D → Map[A, B] → Bool → Map[A, B] → Bool
_∃	map-maplet	function, C → Map[A, B] → Bool → Map[A, B] → Bool
_∃	maplet	function, B × C × D → Heap[A] → Bool → Heap[A] → Bool
_∃	maplet	function, B × C → Heap[A] → Bool → Heap[A] → Bool
_∃	maplet	function, B → Heap[A] → Bool → Heap[A] → Bool
_∃	heap-is-map-instance	function, B × C × D → Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
_∃	heap-is-map-instance	function, B × C → Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
_∃	heap-is-map-instance	function, B → Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
_∃	existential	function, A → Heap[A] → Bool → Heap[A] → Bool
a	heap-aux	variable, B
a	list-dup	variable, A
a	set-union	variable, A
a	linked-list-seg	variable, A
a	dlinked-maplist-seg	variable, A
a	map	variable, A
a	dlinked-list-seg	variable, A
a	linked-tree-path	variable, A
a	tree-path	variable, A
a	cell	variable, A
a	iter-set	variable, A
a	set-basic	variable, A
a	dlinked-list	variable, A
a	iter-map	variable, A
a	list-data	variable, A
a	linked-maptree	variable, A
a	relops	variable, A
a	heap-is-map-instance	variable, A
a	list	variable, A
a	linked-maplist	variable, A
a	list-last	variable, A
a	heapmap	variable, A
a	linked-tree	variable, A
a	linked-list	variable, A
a	existential	variable, A
a	dlinked-maplist	variable, A
a	linked-maplist-seg	variable, A
aP	iter-set	variable, A → Heap[A] → Bool
adP	iter-map	variable, A × B → Heap[A] → Bool
alloc#	heap	procedure, : Heap[A] → Ref[A]
alloc#	heapmap	procedure, : Map[Ref[A], A] → Ref[A]
b	list-dup	variable, A
b	set-union	variable, B
b	linked-list-seg	variable, A
b	dlinked-maplist-seg	variable, A
b	refmap-maplet	variable, B
b	map	variable, A
b	dlinked-list-seg	variable, A
b	linked-tree-path	variable, Bool
b	tree-path	variable, Bool
b	set-basic	variable, A
b	dlinked-list	variable, A
b	maplet	variable, B
b	relops	variable, B
b	heap-is-map-instance	variable, B
b	list	variable, B
b	list-last	variable, A
b	heapmap	variable, B
b	separation	variable, B
b	dlinked-maplist	variable, A
b	linked-maplist-seg	variable, A
bP	refmap-maplet	variable, B → Map[Ref[A], A] → Bool
bP	maplet	variable, B → Heap[A] → Bool
bcP	refmap-maplet	variable, B × C → Map[Ref[A], A] → Bool
bcP	maplet	variable, B × C → Heap[A] → Bool
bcdP	maplet	variable, B × C × D → Heap[A] → Bool
branch	tree	function, Tree[A] × A × Tree[A] → Tree[A]
butlast	list-last	partial function, List[A] → List[A]
bv	heap-aux	variable, Bool
bv	heap-sep	variable, Bool
bv	refmap-separation	variable, Bool
bv	map-sep	variable, Bool
bv	separation	variable, Bool
bv	heap-fun	variable, Bool
bv	map-separation	variable, Bool
bx	list-dup	variable, List[B]
bx	list	variable, List[B]
c	list-dup	variable, A
c	linked-list-seg	variable, A
c	dlinked-maplist-seg	variable, A
c	refmap-maplet	variable, C
c	map-maplet	variable, C
c	map	variable, A
c	dlinked-list-seg	variable, A
c	dlinked-list	variable, A
c	maplet	variable, C
c	relops	variable, C
c	heap-is-map-instance	variable, C
c	list-last	variable, A
c	heapmap	variable, C
c	separation	variable, C
c	dlinked-maplist	variable, A
cP	map-maplet	variable, C → Map[A, B] → Bool
cdP	map-maplet	variable, C × D → Map[A, B] → Bool
ce	linked-list-seg	variable, Cell[A]
ce	cell	variable, Cell[A]
ce	linked-maplist	variable, Cell[A]
ce	linked-list	variable, Cell[A]
ce	linked-maplist-seg	variable, Cell[A]
cod	relops	function, A × B → Bool → B → Bool
cur	dlinked-maplist-seg	variable, Ref[Node[A]]
cur	dlinked-list-seg	variable, Ref[Node[A]]
d	heapfuns-map	variable, B
d	heapfuns	variable, A
d	map-maplet	variable, D
d	map	variable, B
d	heap	variable, A
d	heap-old	variable, A
d	iter-map	variable, B
d	maplet	variable, D
d	heap-is-map-instance	variable, D
d	heapmap	variable, D
d	separation	variable, D
disj	list-dup	predicate, List[A] × List[A]
disjoint	set-union	predicate, Set[A] × Set[A]
distinct	list-dup	function, List[A] → List[A]
dll	dlinked-list	function, Ref[Node[A]] × Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool
dll	dlinked-list	function, Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool
dll	dlinked-maplist	function, Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool
dll	dlinked-maplist	function, Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool
dll-trav	dlinked-maplist-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool
dll-trav	dlinked-list-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool
dlls	dlinked-maplist-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool
dlls	dlinked-maplist-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Map[Ref[Node[A]], Node[A]] → Bool
dlls	dlinked-list-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool
dlls	dlinked-list-seg	function, Ref[Node[A]] × Ref[Node[A]] × Ref[Node[A]] × List[A] → Heap[Node[A]] → Bool
dom	heapfuns-map	function, Map[A, B] → Set[A]
dom	heapfuns	function, Heap[A] → Set[Ref[A]]
dom	heap-old	function, Heap[A] → Set[Ref[A]]
dom	relops	function, A × B → Bool → A → Bool
dom	heap-is-map-instance	function, Map[Ref[A], A] → Set[Ref[A]]
dropRight	list-last	partial function, List[A] × Nat → List[A]
dups	list-dup	predicate, List[A]
emp	heap-sep	predicate, Heap[A]
emp	heap-is-map-instance	predicate, Map[Ref[A], A]
emp	map-sep	predicate, Map[A, B]
exists	set-union	predicate, Set[A] × A → Bool
f	heap-aux	variable, Ref[(A, B)] → A
f	list-dup	variable, A → B
f	set-union	variable, A → B
f	relops	variable, A → B
f	list	variable, A → B
f	heap-fun	variable, Ref[A] → A
fa	list-dup	variable, B
false	heap-sep	predicate, Heap[A]
false	heap-is-map-instance	predicate, Map[Ref[A], A]
false	map-sep	predicate, Map[A, B]
fillfirst	list-last	function, Nat × A × List[A] → List[A]
filter	set-union	function, Set[A] × A → Bool → Set[A]
foldLeft	list	function, List[A] × B × B × A → B → B
footprint	heap-mod	predicate, Set[Ref[A]] × Heap[A] → Bool × Heap[A]
forall	set-union	predicate, Set[A] × A → Bool
funp	relops	predicate, A × B → Bool
g	heap-aux	variable, Ref[(A, B)] → B
guar	separation-rg	predicate, Id × Ref[A] → Id × Heap[A] × Ref[A] → Id × Heap[A]
h	heap-aux	variable, Heap[(A, B)]
h	heapfuns-map	variable, Map[A, B]
h	separation-rg	variable, Heap[A]
h	linked-list-seg	variable, Heap[Cell[A]]
h	heapfuns	variable, Heap[A]
h	heap-sep	variable, Heap[A]
h	dlinked-maplist-seg	variable, Map[Ref[Node[A]], Node[A]]
h	refmap-maplet	variable, Map[Ref[A], A]
h	map-maplet	variable, Map[A, B]
h	heap	variable, Heap[A]
h	refmap-separation	variable, Map[Ref[A], A]
h	dlinked-list-seg	variable, Heap[Node[A]]
h	linked-tree-path	variable, Heap[Node[A]]
h	heap-old	variable, Heap[A]
h	iter-set	variable, Heap[A]
h	map-ex-maplet	variable, Map[A, B]
h	iter-n	variable, Heap[A]
h	dlinked-list	variable, Heap[Node[A]]
h	iter-map	variable, Heap[A]
h	heap-mod	variable, Heap[A]
h	linked-maptree	variable, Map[Ref[Node[A]], Node[A]]
h	maplet	variable, Heap[A]
h	refmap-ex-maplet	variable, Map[Ref[A], A]
h	heap-is-map-instance	variable, Map[Ref[A], A]
h	linked-maplist	variable, Map[Ref[Cell[A]], Cell[A]]
h	map-sep	variable, Map[A, B]
h	heapmap	variable, Map[Ref[A], A]
h	linked-tree	variable, Heap[Node[A]]
h	linked-list	variable, Heap[Cell[A]]
h	separation	variable, Heap[A]
h	existential	variable, Heap[A]
h	dlinked-maplist	variable, Map[Ref[Node[A]], Node[A]]
h	heap-fun	variable, Heap[A]
h	ex-maplet	variable, Heap[A]
h	linked-maplist-seg	variable, Map[Ref[Cell[A]], Cell[A]]
h	map-separation	variable, Map[A, B]
hO	separation-rg	variable, Ref[A] → Id
hP	heap-aux	variable, Heap[(A, B)] → Bool
hP	heapfuns-map	variable, Map[A, B] → Bool
hP	separation-rg	variable, Heap[A] → Bool
hP	linked-list-seg	variable, Heap[Cell[A]] → Bool
hP	heapfuns	variable, Heap[A] → Bool
hP	heap-sep	variable, Heap[A] → Bool
hP	dlinked-maplist-seg	variable, Map[Ref[Node[A]], Node[A]] → Bool
hP	refmap-maplet	variable, Map[Ref[A], A] → Bool
hP	map-maplet	variable, Map[A, B] → Bool
hP	heap	variable, Heap[A] → Bool
hP	refmap-separation	variable, Map[Ref[A], A] → Bool
hP	dlinked-list-seg	variable, Heap[Node[A]] → Bool
hP	linked-tree-path	variable, Heap[Node[A]] → Bool
hP	heap-old	variable, Heap[A] → Bool
hP	iter-set	variable, Heap[A] → Bool
hP	map-ex-maplet	variable, Map[A, B] → Bool
hP	iter-n	variable, Heap[A] → Bool
hP	dlinked-list	variable, Heap[Node[A]] → Bool
hP	iter-map	variable, Heap[A] → Bool
hP	heap-mod	variable, Heap[A] → Bool
hP	linked-maptree	variable, Map[Ref[Node[A]], Node[A]] → Bool
hP	maplet	variable, Heap[A] → Bool
hP	refmap-ex-maplet	variable, Map[Ref[A], A] → Bool
hP	heap-is-map-instance	variable, Map[Ref[A], A] → Bool
hP	linked-maplist	variable, Map[Ref[Cell[A]], Cell[A]] → Bool
hP	map-sep	variable, Map[A, B] → Bool
hP	heapmap	variable, Map[Ref[A], A] → Bool
hP	linked-tree	variable, Heap[Node[A]] → Bool
hP	linked-list	variable, Heap[Cell[A]] → Bool
hP	separation	variable, Heap[A] → Bool
hP	existential	variable, Heap[A] → Bool
hP	dlinked-maplist	variable, Map[Ref[Node[A]], Node[A]] → Bool
hP	calculus	variable, Heap[A] → Bool
hP	heap-fun	variable, Heap[A] → Bool
hP	ex-maplet	variable, Heap[A] → Bool
hP	linked-maplist-seg	variable, Map[Ref[Cell[A]], Cell[A]] → Bool
hP	map-separation	variable, Map[A, B] → Bool
hPa	existential	variable, A → Heap[A] → Bool
hQ	calculus	variable, Heap[A] → Bool
hR	heap-aux	variable, Heap[(A, B)] → Bool
ha	heap-aux	variable, Heap[(A, B)]
hasvalnext	cellparam	predicate, Cell[A]
hd	dlinked-maplist-seg	variable, Ref[Node[A]]
hd	dlinked-list-seg	variable, Ref[Node[A]]
head	list-data	partial function, List[A] → A
head	list-data	variable, A
id	ownership	variable, Id
id	separation-rg	variable, Id
id	gownership	variable, Id
id	gownership	function, IdxO[A] → Id
idxO	gownership	variable, IdxO[A]
inj	relops	predicate, A × B → Bool
irel	relops	variable, B × A → Bool
ite	heap-sep	function, Bool × Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
ite	heap-is-map-instance	function, Bool × Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
ite	map-sep	function, Bool × Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
last	list-last	partial function, List[A] → A
leaf	tree	constant, Tree[A]
left	node	variable, Ref[Node[A]]
left	node	function, Node[A] → Ref[Node[A]]
left	tree	partial function, Tree[A] → Tree[A]
left	tree	variable, Tree[A]
left:=	node	function, Node[A] × Ref[Node[A]] → Node[A]
left:=	tree	partial function, Tree[A] × Tree[A] → Tree[A]
ll-lasso	linked-list-seg	function, Ref[Cell[A]] × List[A] → Heap[Cell[A]] → Bool
ll-trav	linked-list-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Heap[Cell[A]] → Bool
ll-trav	linked-list-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Heap[Cell[A]] → Bool
ll-trav	linked-maplist-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool
ll-trav	linked-maplist-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool
lls	linked-list-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Heap[Cell[A]] → Bool
lls	linked-maplist-seg	function, Ref[Cell[A]] × Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool
ls	linked-maplist	function, Ref[Cell[A]] × List[A] → Map[Ref[Cell[A]], Cell[A]] → Bool
ls	linked-list	function, Ref[Cell[A]] × List[A] → Heap[Cell[A]] → Bool
lst	dlinked-maplist-seg	variable, Ref[Node[A]]
lst	dlinked-list-seg	variable, Ref[Node[A]]
m	set-union	variable, Nat
m	iter-n	variable, Nat
m	list-last	variable, Nat
map	set-union	function, Set[A] × A → B → Set[B]
map	list	function, List[A] × A → B → List[B]
me	separation-rg	variable, Id
mk	heap-aux	function, Set[Ref[(A, B)]] × Ref[(A, B)] → A × Ref[(A, B)] → B → Heap[(A, B)]
mk	heap-fun	function, Set[Ref[A]] × Ref[A] → A → Heap[A]
mklist	list-last	function, A × Nat → List[A]
mknode	node	function, Ref[Node[A]] × A × Ref[Node[A]] → Node[A]
modify	heap-mod	function, Set[Ref[A]] → Heap[A] × Heap[A] → Bool
modify*	heap-mod	function, Set[Ref[A]] → Heap[A] × Heap[A] → Bool
n	set-union	variable, Nat
n	heap	variable, Nat
n	set-basic	variable, Nat
n	iter-n	variable, Nat
n	list-data	variable, Nat
n	relops	variable, Nat
n	heap-is-map-instance	variable, Nat
n	list	variable, Nat
n	list-last	variable, Nat
n	heapmap	variable, Nat
n	separation	variable, Nat
nP	iter-n	variable, Nat → Heap[A] → Bool
nd	dlinked-maplist-seg	variable, Node[A]
nd	dlinked-list-seg	variable, Node[A]
nd	linked-tree-path	variable, Node[A]
nd	dlinked-list	variable, Node[A]
nd	node	variable, Node[A]
nd	dlinked-maplist	variable, Node[A]
next	cellparam	function, Cell[A] → Ref[Cell[A]]
null	polyref	constant, Ref[A]
nxt	dlinked-maplist-seg	variable, Ref[Node[A]]
nxt	dlinked-list-seg	variable, Ref[Node[A]]
nxt	cell	variable, Ref[Cell[A]]
nxt	cell	function, Cell[A] → Ref[Cell[A]]
nxt:=	cell	function, Cell[A] × Ref[Cell[A]] → Cell[A]
o	heap-aux	variable, A
o	heapfuns-map	variable, B
o	separation-rg	variable, A
o	heapfuns	variable, A
o	refmap-maplet	variable, A
o	map-maplet	variable, B
o	heap	variable, A
o	refmap-separation	variable, A
o	heap-old	variable, A
o	map-ex-maplet	variable, B
o	maplet	variable, A
o	relops	function, A × B → Bool × B × C → Bool → A × C → Bool
o	refmap-ex-maplet	variable, A
o	separation	variable, A
o	heap-fun	variable, A
o	ex-maplet	variable, A
o	map-separation	variable, B
oP	heap-fun	variable, A → Heap[A] → Bool
oa	heap-aux	variable, (A, B)
oaR	heap-aux	variable, A × B → Heap[(A, B)] → Bool
ob	heap-mod	variable, A
of	ownership	variable, Ref[A] → Id
of	separation-rg	variable, Ref[A] → Id
of	gownership	variable, Ref[A] → Id
ohP	separation-rg	variable, A → Heap[A] → Bool
p	set-union	variable, A → Bool
p	linked-tree-path	variable, List[Bool]
p	tree-path	variable, List[Bool]
pelem	relops	variable, A × A → Bool
pfunp	relops	predicate, A × B → Bool
precise	heap-sep	predicate, Heap[A] → Bool
precise	heap-is-map-instance	predicate, Map[Ref[A], A] → Bool
precise	map-sep	predicate, Map[A, B] → Bool
prv	dlinked-maplist-seg	variable, Ref[Node[A]]
prv	dlinked-list-seg	variable, Ref[Node[A]]
r	heap-aux	variable, Ref[(A, B)]
r	heapfuns-map	variable, A
r	separation-rg	variable, Ref[A]
r	linked-list-seg	variable, Ref[Cell[A]]
r	heapfuns	variable, Ref[A]
r	dlinked-maplist-seg	variable, Ref[Node[A]]
r	refmap-maplet	variable, Ref[A]
r	map-maplet	variable, A
r	heap	variable, Ref[A]
r	refmap-separation	variable, Ref[A]
r	dlinked-list-seg	variable, Ref[Node[A]]
r	linked-tree-path	variable, Ref[Node[A]]
r	heap-old	variable, Ref[A]
r	cell	variable, Ref[Cell[A]]
r	map-ex-maplet	variable, A
r	dlinked-list	variable, Ref[Node[A]]
r	heap-mod	variable, Ref[A]
r	linked-maptree	variable, Ref[Node[A]]
r	maplet	variable, Ref[A]
r	refmap-ex-maplet	variable, Ref[A]
r	reachable	variable, Ref[A]
r	heap-is-map-instance	variable, Ref[A]
r	linked-maplist	variable, Ref[Cell[A]]
r	heapmap	variable, Ref[A]
r	linked-tree	variable, Ref[Node[A]]
r	linked-list	variable, Ref[Cell[A]]
r	separation	variable, Ref[A]
r	dlinked-maplist	variable, Ref[Node[A]]
r	heap-fun	variable, Ref[A]
r	ex-maplet	variable, Ref[A]
r	linked-maplist-seg	variable, Ref[Cell[A]]
r	map-separation	variable, A
rR	heap-aux	variable, Ref[(A, B)] → Heap[(A, B)] → Bool
reach	reachable	function, Ref[A] × Ref[A] × Ref[A] → Bool → Set[Ref[A]]
rel	relops	variable, A × B → Bool
relac	relops	variable, A × C → Bool
relbc	relops	variable, B × C → Bool
rely	separation-rg	predicate, Id × Ref[A] → Id × Heap[A] × Ref[A] → Id × Heap[A]
rev	list-last	function, List[A] → List[A]
rhP	heap-fun	variable, Ref[A] → Heap[A] → Bool
right	node	variable, Ref[Node[A]]
right	node	function, Node[A] → Ref[Node[A]]
right	tree	partial function, Tree[A] → Tree[A]
right	tree	variable, Tree[A]
right:=	node	function, Node[A] × Ref[Node[A]] → Node[A]
right:=	tree	partial function, Tree[A] × Tree[A] → Tree[A]
rrR	heap-aux	variable, (Ref[(A, B)], Ref[(A, B)]) → Heap[(A, B)] → Bool
rrhP	heap-fun	variable, Ref[A] × Ref[A] → Heap[A] → Bool
rrp	reachable	variable, Ref[A] × Ref[A] → Bool
rs	heap-aux	variable, Set[Ref[(A, B)]]
rs	heapfuns-map	variable, Set[A]
rs	heapfuns	variable, Set[Ref[A]]
rs	heap-old	variable, Set[Ref[A]]
rs	heap-mod	variable, Set[Ref[A]]
rs	heap-fun	variable, Set[Ref[A]]
rtc	relops	function, Nat × A × A → Bool → A × A → Bool
s	set-union	variable, Set[A]
s	iter-set	variable, Set[A]
s	set-basic	variable, Set[A]
st	map	variable, Map[A, B]
st	iter-map	variable, Map[A, B]
surj	relops	predicate, A × B → Bool
t	linked-tree-path	variable, Tree[A]
t	tree-path	variable, Tree[A]
t	linked-maptree	variable, Tree[A]
t	tree	variable, Tree[A]
t	linked-tree	variable, Tree[A]
tail	list-data	partial function, List[A] → List[A]
tail	list-data	variable, List[A]
toFun	relops	partial function, A × B → Bool → A → B
total	relops	predicate, A × B → Bool
tr	linked-maptree	function, Ref[Node[A]] × Tree[A] → Map[Ref[Node[A]], Node[A]] → Bool
tr	linked-tree	function, Ref[Node[A]] × Tree[A] → Heap[Node[A]] → Bool
trp	linked-tree-path	partial function, Ref[Node[A]] × Tree[A] × List[Bool] × Ref[Node[A]] → Heap[Node[A]] → Bool
true	heap-sep	predicate, Heap[A]
true	heap-is-map-instance	predicate, Map[Ref[A], A]
true	map-sep	predicate, Map[A, B]
val	cellparam	function, Cell[A] → B
val	cell	variable, A
val	cell	function, Cell[A] → A
val	node	variable, A
val	node	function, Node[A] → A
val	tree	partial function, Tree[A] → A
val	tree	variable, A
val:=	cell	function, Cell[A] × A → Cell[A]
val:=	node	function, Node[A] × A → Node[A]
val:=	tree	partial function, Tree[A] × A → Tree[A]
x	list-dup	variable, List[A]
x	linked-list-seg	variable, List[A]
x	dlinked-maplist-seg	variable, List[A]
x	dlinked-list-seg	variable, List[A]
x	dlinked-list	variable, List[A]
x	list-data	variable, List[A]
x	list	variable, List[A]
x	linked-maplist	variable, List[A]
x	list-last	variable, List[A]
x	linked-list	variable, List[A]
x	dlinked-maplist	variable, List[A]
x	linked-maplist-seg	variable, List[A]
y	list-dup	variable, List[A]
y	linked-list-seg	variable, List[A]
y	dlinked-maplist-seg	variable, List[A]
y	dlinked-list-seg	variable, List[A]
y	dlinked-list	variable, List[A]
y	list-data	variable, List[A]
y	list	variable, List[A]
y	linked-maplist	variable, List[A]
y	list-last	variable, List[A]
y	linked-list	variable, List[A]
y	dlinked-maplist	variable, List[A]
y	linked-maplist-seg	variable, List[A]
z	list-dup	variable, List[A]
z	linked-list-seg	variable, List[A]
z	dlinked-maplist-seg	variable, List[A]
z	dlinked-list-seg	variable, List[A]
z	dlinked-list	variable, List[A]
z	list-data	variable, List[A]
z	list	variable, List[A]
z	list-last	variable, List[A]
z	dlinked-maplist	variable, List[A]
}	set-union	function, A → Set[A]
}	heap-sep	function, Heap[A] → Heap[A] → Bool
}	heap-is-map-instance	function, Map[Ref[A], A] → Map[Ref[A], A] → Bool
}	map-sep	function, Map[A, B] → Map[A, B] → Bool
¬	heap-sep	function, Heap[A] → Bool → Heap[A] → Bool
¬	heap-is-map-instance	function, Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
¬	map-sep	function, Map[A, B] → Bool → Map[A, B] → Bool
×	gownership	function, Id × Ref[A] → Id → IdxO[A]
×	cell	function, A × Ref[Cell[A]] → Cell[A]
→	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
→	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
→	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
∅	map	constant, Map[A, B]
∅	heap	constant, Heap[A]
∅	heap-old	constant, Heap[A]
∅	set-basic	constant, Set[A]
∈	map	predicate, A × Map[A, B]
∈	heap	predicate, Ref[A] × Heap[A]
∈	tree-path	predicate, List[Bool] × Tree[A]
∈	heap-old	predicate, Ref[A] × Heap[A]
∈	set-basic	predicate, A × Set[A]
∈	list	predicate, A × List[A]
∧	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
∧	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
∧	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
∧_	iter-set	function, A → Heap[A] → Bool × Set[A] → Heap[A] → Bool
∧_	iter-map	function, A × B → Heap[A] → Bool × Map[A, B] → Heap[A] → Bool
∨	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
∨	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
∨	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
∩	set-union	function, Set[A] × Set[A] → Set[A]
∪	heapfuns-map	function, Map[A, B] × Map[A, B] → Map[A, B]
∪	set-union	function, Set[A] × Set[A] → Set[A]
∪	heapfuns	function, Heap[A] × Heap[A] → Heap[A]
∪	heap-old	function, Heap[A] × Heap[A] → Heap[A]
∪	heap-is-map-instance	function, Map[Ref[A], A] × Map[Ref[A], A] → Map[Ref[A], A]
≡	refmap-separation	predicate, Map[Ref[A], A] × Map[Ref[A], A]
≡	heap-mod	function, Heap[A] × Heap[A] → Set[Ref[A]] → Bool
≡	heap-is-map-instance	predicate, Map[Ref[A], A] × Map[Ref[A], A]
≡	separation	predicate, Heap[A] × Heap[A]
≡	map-separation	predicate, Map[A, B] × Map[A, B]
≤	nat	predicate, Nat × Nat
≥	nat	predicate, Nat × Nat
⊆	heapfuns	predicate, Heap[A] × Heap[A]
⊆	heap-sep	predicate, Heap[A] → Bool × Heap[A] → Bool
⊆	map	predicate, Map[A, B] × Map[A, B]
⊆	heap-old	predicate, Heap[A] × Heap[A]
⊆	set-basic	predicate, Set[A] × Set[A]
⊆	heap-is-map-instance	predicate, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool
⊆	heap-is-map-instance	predicate, Map[Ref[A], A] × Map[Ref[A], A]
⊆	map-sep	predicate, Map[A, B] → Bool × Map[A, B] → Bool
⊑	list-last	predicate, List[A] × List[A]
⊒	list-last	predicate, List[A] × List[A]
⊗	heap-sep	function, Heap[A] → Bool × Heap[A] → Bool → Heap[A] → Bool
⊗	heap-is-map-instance	function, Map[Ref[A], A] → Bool × Map[Ref[A], A] → Bool → Map[Ref[A], A] → Bool
⊗	map-sep	function, Map[A, B] → Bool × Map[A, B] → Bool → Map[A, B] → Bool
⊗_	iter-set	function, A → Heap[A] → Bool × Set[A] → Heap[A] → Bool
⊗_	iter-n	function, Nat → Heap[A] → Bool × Nat × Nat → Heap[A] → Bool
⊗_	iter-map	function, A × B → Heap[A] → Bool × Map[A, B] → Heap[A] → Bool
⊥	heapfuns-map	predicate, Map[A, B] × Map[A, B]
⊥	heapfuns	predicate, Heap[A] × Heap[A]
⊥	heap-old	predicate, Heap[A] × Heap[A]
⊥	heap-is-map-instance	predicate, Map[Ref[A], A] × Map[Ref[A], A]
⌝	heap-sep	function, Bool → Heap[A] → Bool
⌝	heap-is-map-instance	function, Bool → Map[Ref[A], A] → Bool
⌝	map-sep	function, Bool → Map[A, B] → Bool