[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
# .	nat-store	f	nat-set → nat
# .	store	f	store → nat
# .	list-data	f	list → nat
# .	laddress-list	f	laddress-list → nat
. '	laddress-list	f	laddress → laddress-list
. '	list	f	elem → list
. + .	nat-basic	f	nat × nat → nat
. + .	list-data	f	elem × list → list
. + .	laddress-list	f	laddress-list × laddress → laddress-list
. + .	list	f	list × list → list
. + .	laddress-list	f	laddress-list × laddress-list → laddress-list
. + .	list	f	list × elem → list
. + .	laddress-list	f	laddress × laddress-list → laddress-list
. ++ .	nat-store	f	nat-set × nat → nat-set
. ++ .	list-dup	f	list × elem → list
. ++ .	laddress-list	f	laddress-list × laddress → laddress-list
. +1	nat-basic	f	nat → nat
. +2 .	list	f	elem × elem → list
. +2 .	laddress-list	f	laddress × laddress → laddress-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	nat-store	f	store × nat → store
. -- .	nat-store	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	list-del	f	list × elem → list
. -1l .	laddress-list	f	laddress-list × laddress → laddress-list
. -l .	list-del	f	list × elem → list
. -l .	laddress-list	f	laddress-list × laddress → laddress-list
. -p .	laddress-list	f	laddress-list × nat → laddress-list
. -p .	list-del	f	list × nat → list
. .butlast	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .butlast	list-last	pf	list → list with λ x. x ≠ []
. .butmax	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .butmin	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .head	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .head	list-data	pf	list → elem with λ x. x ≠ []
. .ladrlist	ablock	f	ablock → laddress-list
. .ladrlist:= .	ablock	f	ablock × laddress-list → ablock
. .last	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .last	list-last	pf	list → elem with λ x. x ≠ []
. .list	ablock	f	ablock → list
. .list:= .	ablock	f	ablock × list → ablock
. .map ( . )	ablock-store	f	store × (nat × ablock → ablock) → store
. .map ( . )	ablock-store	f	store × (ablock → ablock) → store
. .max	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .min	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .off	laddress	f	laddress → nat
. .off:= .	laddress	f	laddress × nat → laddress
. .ref-size	ablock	f	ablock → nat
. .ref-size:= .	ablock	f	ablock × nat → ablock
. .size	laddress	f	laddress → nat
. .size:= .	laddress	f	laddress × nat → laddress
. .tail	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .tail	list-data	pf	list → list with λ x. x ≠ []
. < .	nat-basic	p	nat × nat
. < .	nat-set	p	nat-set × nat
. < .	nat-set	p	nat × nat-set
. < .	list-data	p	list × list
. < .	laddress-list	p	laddress-list × laddress-list
. > .	nat	p	nat × nat
. [ . ]	ablock-store	pf	store × nat → ablock with λ st, n. n ∈ st
. [ . ]	ablock-store	f	store × nat × ablock → store
. [ . ]	laddress-list	pf	laddress-list × nat × laddress → laddress-list with λ lax, n, ladr. n < # lax
. [ . ]	laddress-list	pf	laddress-list × nat → laddress with λ lax, n. n < # lax
. [ . ]	list-del	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	list-del	pf	list × nat → elem with λ x, n. n < # x
. \ .	nat-store	f	nat-set × nat-set → nat-set
. \ .	nat-store	f	store × nat-set → store
. \| .	nat-store	f	store × nat-set → store
. ∈ .	ablock-store	p	ablock × store
. ∈ .	list	p	elem × list
. ∈ .	nat-store	p	nat × nat-set
. ∈ .	laddress-list	p	laddress × laddress-list
. ∈ .	nat-store	p	nat × store
. ∩ .	nat-store	f	nat-set × nat-set → nat-set
. ∪ .	nat-store	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	nat-store	p	nat-set × nat-set
. ⊆ .	store	p	store × store
. ⊑ .	list-last	p	list × list
. ⊑ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	list-last	p	list × list
. ⊕ .	store+set	f	store × store → store
@	laddress	f	nat × nat → laddress
[]	list-data	c	list
[]	laddress-list	c	laddress-list
{ . }	nat-store	f	nat → nat-set
∅	store	c	store
∅	nat-store	c	nat-set
a	elem	v	elem
a0	list-data	v	elem
ablock	ablock	s
ablock	ablock	v	ablock
ablock0	ablock-store	v	ablock
ablock1	ablock-store	v	ablock
ablock2	ablock-store	v	ablock
b	elem	v	elem
butlastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
c	elem	v	elem
dataf	ablock-store	v	ablock → ablock
disj	list-dup	p	list × list
disj	laddress-list	p	laddress-list × laddress-list
dom .	nat-store	f	store → nat-set
dropn	list-prefixn	f	nat × list → list
dropn	laddress-list	f	nat × laddress-list → laddress-list
dups	laddress-list	p	laddress-list
dups	list-dup	p	list
elem	elem	s
elemdataf	ablock-store	v	nat × ablock → ablock
fillfirst	list-last	f	nat × elem × list → list
fillfirst	laddress-list	f	nat × laddress × laddress-list → laddress-list
firstn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
frome	list-del	f	list × elem → list
frome	laddress-list	f	laddress-list × laddress → laddress-list
laddress	laddress	s
laddress-list	laddress-list	s
ladr	laddress	v	laddress
ladr0	laddress-list	v	laddress
ladr1	laddress-list	v	laddress
ladr2	laddress-list	v	laddress
lastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
lastn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
lax	laddress-list	v	laddress-list
lax0	laddress-list	v	laddress-list
lax1	laddress-list	v	laddress-list
lax2	laddress-list	v	laddress-list
lax3	laddress-list	v	laddress-list
list	list-data	s
m	nat-basic	v	nat
m0	laddress	v	nat
m1	laddress	v	nat
m2	laddress	v	nat
mkblock	ablock	f	list × laddress-list × nat → ablock
mklist	list-last	f	elem × nat → list
mklist	laddress-list	f	laddress × nat → laddress-list
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	nat-store	v	nat
n3	nat-store	v	nat
n4	nat-store	v	nat
nat	nat-basic	s
nat-set	nat-store	s
ns	nat-store	v	nat-set
ns0	nat-store	v	nat-set
ns1	nat-store	v	nat-set
ns2	nat-store	v	nat-set
pos	list-del	f	elem × list → nat
pos	laddress-list	f	laddress × laddress-list → nat
prefixn	laddress-list	f	nat × laddress-list → laddress-list
prefixn	list-prefixn	f	nat × list → list
restn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
rev	laddress-list	f	laddress-list → laddress-list
rev	list-last	f	list → list
rmdup	list-dup	f	list → list
rmdup	laddress-list	f	laddress-list → laddress-list
slice	list-prefixn	f	nat × nat × list → list
slice	laddress-list	f	nat × nat × laddress-list → laddress-list
st	store	v	store
st0	store	v	store
st1	store	v	store
st2	store	v	store
store	store	s
sublist	laddress-list	pf	nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax
sublist	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
y	list-data	v	list
z	list-data	v	list