[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
# .	erasequeue-base	f	queue → nat
. '	erasequeue-base	f	erasequeueentry → queue
. + .	nat-basic	f	nat × nat → nat
. + .	erasequeue-base	f	queue × erasequeueentry → queue
. + .	erasequeue-base	f	erasequeueentry × queue → queue
. + .	erasequeue-base	f	queue × queue → queue
. ++ .	erasequeue-base	f	queue × erasequeueentry → queue
. +1	nat-basic	f	nat → nat
. +2 .	erasequeue-base	f	erasequeueentry × erasequeueentry → queue
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	erasequeue-base	f	queue × erasequeueentry → queue
. -l .	erasequeue-base	f	queue × erasequeueentry → queue
. -p .	erasequeue-base	f	queue × nat → queue
. .butlast	erasequeue-base	pf	queue → queue with λ q. q ≠ []
. .head	erasequeue-base	pf	queue → erasequeueentry with λ q. q ≠ []
. .last	erasequeue-base	pf	queue → erasequeueentry with λ q. q ≠ []
. .leb	lebref	pf	lebref → nat with λ lref. lref ≠ none
. .leb:= .	lebref	pf	lebref × nat → lebref with λ lref, m. lref ≠ none
. .lebref	erasequeueentry	f	erasequeueentry → lebref
. .lebref:= .	erasequeueentry	f	erasequeueentry × lebref → erasequeueentry
. .pnum	erasequeueentry	f	erasequeueentry → nat
. .pnum:= .	erasequeueentry	f	erasequeueentry × nat → erasequeueentry
. .tail	erasequeue-base	pf	queue → queue with λ q. q ≠ []
. .vol	lebref	pf	lebref → volid with λ lref. lref ≠ none
. .vol:= .	lebref	pf	lebref × volid → lebref with λ lref, v. lref ≠ none
. < .	nat-basic	p	nat × nat
. < .	erasequeue-base	p	queue × queue
. > .	nat	p	nat × nat
. [ . ]	erasequeue-base	pf	queue × nat × erasequeueentry → queue with λ q, n, eqent. n < # q
. [ . ]	erasequeue-base	pf	queue × nat → erasequeueentry with λ q, n. n < # q
. \ .	erasequeue-base	f	queue × queue → queue
. × .	lebref	f	volid × nat → lebref
. ∈ .	erasequeue-base	p	erasequeueentry × queue
. ∪ .	erasequeue-base	f	queue × queue → queue
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	erasequeue-base	p	queue × queue
. ⊑ .	erasequeue-base	p	queue × queue
. ⊒ .	erasequeue-base	p	queue × queue
[]	erasequeue-base	c	queue
butlastn	erasequeue-base	pf	nat × queue → queue with λ n, q. n ≤ # q
disj	erasequeue-base	p	queue × queue
dups	erasequeue-base	p	queue
eq-entry	erasequeueentry	f	nat × lebref → erasequeueentry
eqent	erasequeueentry	v	erasequeueentry
eqent0	erasequeueentry	v	erasequeueentry
eqent1	erasequeue-base	v	erasequeueentry
eqent2	erasequeue-base	v	erasequeueentry
erasequeueentry	erasequeueentry	s
fillfirst	erasequeue-base	f	nat × erasequeueentry × queue → queue
filter	erasequeue-base	f	queue × queue → queue
firstn	erasequeue-base	pf	nat × queue → queue with λ n, q. n ≤ # q
frome	erasequeue-base	f	queue × erasequeueentry → queue
lastn	erasequeue-base	pf	nat × queue → queue with λ n, q. n ≤ # q
lebref	lebref	s
lref	lebref	v	lebref
lref0	erasequeueentry	v	lebref
m	nat-basic	v	nat
m0	lebref	v	nat
mklist	erasequeue-base	f	erasequeueentry × nat → queue
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
none	lebref	c	lebref
pos	erasequeue-base	f	erasequeueentry × queue → nat
q	erasequeue-base	v	queue
q0	erasequeue-base	v	queue
q1	erasequeue-base	v	queue
q2	erasequeue-base	v	queue
q5	erasequeue-base	v	queue
queue	erasequeue-base	s
restn	erasequeue-base	pf	nat × queue → queue with λ n, q. n ≤ # q
rev	erasequeue-base	f	queue → queue
rmdup	erasequeue-base	f	queue → queue
sublist	erasequeue-base	pf	nat × nat × queue → queue with λ n, m, q. n + m ≤ # q
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
volid	volid	s