[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
. ( . )	linheap	pf	Heap × Ref → Cell with λ st, a. a ∈ st
. ( . )	reflist	pf	Reflist × Nat → Ref with λ x, n. n < # x
. ( . := . )	linheap	f	Heap × Ref × Cell → Heap
. ( . := . )	reflist	pf	Reflist × Nat × Ref → Reflist with λ x, n, a. n < # x
. + .	nat-basic	f	Nat × Nat → Nat
. + .	reflist	f	Ref × Reflist → Reflist
. + .	reflist	f	Reflist × Reflist → Reflist
. + .	reflist	f	Reflist × Ref → 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
. < .	nat-basic	p	Nat × Nat
. < .	reflist	p	Reflist × Reflist
. > .	nat	p	Nat × Nat
. \ .	reflist	f	Reflist × Reflist → Reflist
. ∈ .	linheap	p	Ref × Heap
. ∈ .	reflist	p	Ref × Reflist
. ∪ .	reflist	f	Reflist × Reflist → Reflist
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	linheap	p	Heap × Heap
. ⊆ .	reflist	p	Reflist × Reflist
. ⊑ .	reflist	p	Reflist × Reflist
. ⊒ .	reflist	p	Reflist × Reflist
. butlast	reflist	pf	Reflist → Reflist with λ x. x ≠ []
. last	reflist	pf	Reflist → Ref with λ x. x ≠ []
. nxt	lincell	f	Cell → Ref
[]	reflist	c	Reflist
∅	linheap	c	Heap
Cell	lincell	s
Heap	linheap	s
Nat	nat-basic	s
Ref	Ref	s
Reflist	reflist	s
butlastn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
ce	path-reachable	v	Cell
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, x. n ≤ # x
frome	reflist	f	Reflist × Ref → Reflist
h	path-reachable	v	Heap
hd .	reflist	pf	Reflist → Ref with λ x. x ≠ []
lastn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
m	path-reachable	v	Nat
mklist	reflist	f	Ref × Nat → Reflist
n	path-reachable	v	Nat
null	Ref	c	Ref
path	path-reachable	p	Reflist × Heap
pos	reflist	f	Ref × Reflist → Nat
r	path-reachable	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
restn	reflist	pf	Nat × Reflist → Reflist with λ n, x. n ≤ # x
rev	reflist	f	Reflist → Reflist
rmdup	reflist	f	Reflist → Reflist
sublist	reflist	pf	Nat × Nat × Reflist → Reflist with λ n, m, x. n + m ≤ # x
tl .	reflist	pf	Reflist → Reflist with λ x. x ≠ []
x	path-reachable	v	Reflist