[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
# .	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
. + .	laddress-list	f	laddress-list × laddress → laddress-list
. + .	list-data	f	elem × list → list
. + .	laddress-list	f	laddress-list × laddress-list → laddress-list
. + .	list	f	list × list → list
. + .	laddress-list	f	laddress × laddress-list → laddress-list
. + .	list	f	list × elem → list
. ++ .	laddress-list	f	laddress-list × laddress → laddress-list
. ++ .	list-dup	f	list × elem → 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
. -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 ≠ []
. .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
. .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
. < .	laddress-list	p	laddress-list × laddress-list
. < .	list-data	p	list × list
. > .	nat	p	nat × nat
. [ . ]	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
. ∈ .	laddress-list	p	laddress × laddress-list
. ∈ .	list	p	elem × list
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	laddress-list	p	laddress-list × laddress-list
. ⊑ .	list-last	p	list × list
. ⊒ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	list-last	p	list × list
@	laddress	f	nat × nat → laddress
[]	list-data	c	list
[]	laddress-list	c	laddress-list
a	elem	v	elem
a0	list-data	v	elem
ablock	ablock	s
ablock	ablock	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
disj	list-dup	p	list × list
disj	laddress-list	p	laddress-list × laddress-list
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
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
nat	nat-basic	s
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	list-last	f	list → list
rev	laddress-list	f	laddress-list → laddress-list
rmdup	list-dup	f	list → list
rmdup	laddress-list	f	laddress-list → laddress-list
slice	laddress-list	f	nat × nat × laddress-list → laddress-list
slice	list-prefixn	f	nat × nat × list → list
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