[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
# .	address-set-array	f	address-set-array → nat
# .	address-list-set	f	address-set → nat
# .	address-list-set	f	address-list → nat
. '	address-list-set	f	address → address-list
. + .	nat-basic	f	nat × nat → nat
. + .	address-list-set	f	address × address-list → address-list
. + .	address-list-set	f	address-list × address → address-list
. + .	address-list-set	f	address-list × address-list → address-list
. ++ .	address-list-set	f	address-set × address → address-set
. ++ .	address-list-set	f	address-list × address → address-list
. +1	nat-basic	f	nat → nat
. +2 .	address-list-set	f	address × address → address-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	address-list-set	f	address-set × address → address-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	address-list-set	f	address-list × address → address-list
. -l .	address-list-set	f	address-list × address → address-list
. -p .	address-list-set	f	address-list × nat → address-list
. .butlast	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .head	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .last	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .tail	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .toSet	address-list-set	f	address-list → address-set
. < .	address-list-set	p	address-list × address-list
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	address-set-array	pf	address-set-array × nat × address-set → address-set-array with λ asar, n, a0. n < # asar
. [ . ]	address-set-array	pf	address-set-array × nat → address-set with λ asar, n. n < # asar
. [ . ]	address-list-set	pf	address-list × nat × address → address-list with λ ax, n, adr. n < # ax
. [ . ]	address-list-set	pf	address-list × nat → address with λ ax, n. n < # ax
. \ .	address-list-set	f	address-set × address-set → address-set
. ∈ .	address-set-array	p	address-set × address-set-array
. ∈ .	address-list-set	p	address × address-list
. ∈ .	address-list-set	p	address × address-set
. ∩ .	address-list-set	f	address-set × address-set → address-set
. ∪ .	address-list-set	f	address-set × address-set → address-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	address-list-set	p	address-set × address-set
. ⊑ .	address-list-set	p	address-list × address-list
. ⊒ .	address-list-set	p	address-list × address-list
[]	address-list-set	c	address-list
{ . }	address-list-set	f	address → address-set
∅	address-list-set	c	address-set
a	address-set-array	v	address-set
address	address	s
address-list	address-list-set	s
address-set	address-list-set	s
address-set-array	address-set-array	s
adr	address	v	address
adr0	address	v	address
adr1	address	v	address
adr2	address	v	address
adr3	address	v	address
adr4	address	v	address
adr5	address	v	address
as	address-list-set	v	address-set
as0	address-list-set	v	address-set
as1	address-list-set	v	address-set
as2	address-list-set	v	address-set
asar	address-set-array	v	address-set-array
asar0	address-set-array	v	address-set-array
asar1	address-set-array	v	address-set-array
asar2	address-set-array	v	address-set-array
ax	address-list-set	v	address-list
ax0	address-list-set	v	address-list
ax1	address-list-set	v	address-list
ay	address-list-set	v	address-list
az	address-list-set	v	address-list
b	address-set-array	v	address-set
butlastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
c	address-set-array	v	address-set
cmp	address-set-array	pp	address-set-array × address-set × nat × nat with λ asar, a0, m, n. m + n ≤ # asar
cmp	address-set-array	pp	address-set-array × nat × address-set-array × nat × nat with λ asar, m, asar0, m0, n. m + n ≤ # asar ∧ m0 + n ≤ # asar0
copy	address-set-array	pf	address-set-array × nat × address-set-array × nat × nat → address-set-array with λ asar, m, asar0, m0, n. m + n ≤ # asar ∧ m0 + n ≤ # asar0
disj	address-list-set	p	address-list × address-list
disj	address-set-array-ops	p	address-set-array × nat × nat
dropn	address-list-set	f	nat × address-list → address-list
dups	address-list-set	p	address-list
fill	address-set-array	pf	address-set-array × address-set × nat × nat → address-set-array with λ asar, a0, n, m. n + m ≤ # asar
fill	address-set-array	f	address-set-array × address-set → address-set-array
fillfirst	address-list-set	f	nat × address × address-list → address-list
firstn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
frome	address-list-set	f	address-list × address → address-list
id○	address-set-array	p	address-set-array × address-set-array × nat
idrange	address-set-array	pp	address-set-array × nat × nat with λ asar, m, n. m + n ≤ # asar
lastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
m	nat-basic	v	nat
m0	array-copy	v	nat
mkarray	address-set-array	f	nat → address-set-array
mklist	address-list-set	f	address × nat → address-list
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
pos	address-list-set	f	address × address-list → nat
prefixn	address-list-set	f	nat × address-list → address-list
restn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
rev	address-set-array	pf	address-set-array × nat → address-set-array with λ asar, n. n ≤ # asar
rev	address-set-array	f	address-set-array → address-set-array
rev	address-list-set	f	address-list → address-list
rmdup	address-list-set	f	address-list → address-list
slice	address-list-set	f	nat × nat × address-list → address-list
subarray	address-set-array	pf	address-set-array × nat × nat → address-set-array with λ asar, m, n. m + n ≤ # asar
sublist	address-list-set	pf	nat × nat × address-list → address-list with λ n, m, ax. n + m ≤ # ax
union	address-set-array-ops	f	address-set-array × nat × nat → address-set