[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
!	remtau	function, 'a → Option('e) → List('a) → List('e)
!	remtau	function, 'a → Option('e) → Stream('a) → Stream('e)
#	stream	function, Stream('a) → Natinf
#	list-data	function, List('a) → Nat
#	set-basic	function, Set('a) → Nat
'	list	function, 'a → List('a)
+	nat-inf	function, Natinf × Natinf → Natinf
+	list	function, List('a) × 'a → List('a)
+	list	function, List('a) × List('a) → List('a)
+	stream	function, List('a) × Nat → 'a → Nat → 'a
+	stream	function, Stream('a) × Stream('a) → Stream('a)
+	stream	function, 'a × Stream('a) → Stream('a)
+	list-data	function, 'a × List('a) → List('a)
+	remtau	function, Option('e) × Stream('e) → Stream('e)
+	nat-basic	function, Nat × Nat → Nat
++	list-dup	function, List('a) × 'a → List('a)
++	set-basic	function, Set('a) × 'a → Set('a)
+1	nat-basic	function, Nat → Nat
+2	list	function, 'a × 'a → List('a)
-	nat	partial function, Nat × Nat → Nat
--	set-union	function, Set('a) × 'a → Set('a)
-1	nat-basic	partial function, Nat → Nat
-1l	list-del	function, List('a) × 'a → List('a)
-l	list-del	function, List('a) × 'a → List('a)
-p	list-del	function, List('a) × Nat → List('a)
.butlast	list-last	partial function, List('a) → List('a)
.distinct	list-dup	function, List('a) → List('a)
.drop	list-del	partial function, List('a) × Nat → List('a)
.drop	stream	partial function, Stream('a) × Nat → Stream('a)
.drop	stream	function, Nat → 'a × Nat → Nat → 'a
.dropRight	list-last	partial function, List('a) × Nat → List('a)
.exists	set-union	predicate, Set('a) × 'a → Bool
.ext	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 'a → Option('e)
.f	stream-basic	partial function, Stream('a) → Nat → 'a
.filter	set-union	function, Set('a) × 'a → Bool → Set('a)
.foldLeft	list	function, List('a) × 'b × 'b × 'a → 'b → 'b
.forall	set-union	predicate, Set('a) × 'a → Bool
.get	option	partial function, Option('a) → 'a
.getOrElse	option	function, Option('a) × 'a → 'a
.head	list-data	partial function, List('a) → 'a
.indexOf	list-del	function, List('a) × 'a → Nat
.l	stream-basic	partial function, Stream('a) → List('a)
.last	list-last	partial function, List('a) → 'a
.map	option	function, Option('a) × 'a → 'b → Option('b)
.map	list	function, List('a) × 'a → 'b → List('b)
.map	set-union	function, Set('a) × 'a → 'b → Set('b)
.n	nat-inf	partial function, Natinf → Nat
.start	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 's → Bool
.step	IO-Aut-data	function, IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool
.sublist	list-del	partial function, List('a) × Nat × Nat → List('a)
.tail	list-data	partial function, List('a) → List('a)
.take	list-del	partial function, List('a) × Nat → List('a)
.take	stream	partial function, Stream('a) × Natinf → Stream('a)
.take	stream	partial function, Stream('a) × Nat → List('a)
.take	stream	function, Nat → 'a × Nat → List('a)
.takeRight	list-del	partial function, List('a) × Nat → List('a)
<	nat-inf	predicate, Natinf × Natinf
<	list-data	predicate, List('a) × List('a)
<	nat-basic	predicate, Nat × Nat
>	nat	predicate, Nat × Nat
C_≡*T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡ωT_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤*T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤T_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤ωT_A	IOrefine-def	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
Graph	infgraph-gen-basic	sort,
IOAut	IO-Aut-data	function, 's → Bool × 's × 'a × 's → Bool × 'a → Option('e) → IOAutomaton('s, 'a, 'e)
IOAut?	IO-Automaton	predicate, IOAutomaton('s, 'a, 'e)
IOAutomaton	IO-Aut-data	sort,
List	list-data	sort,
Nat	nat-basic	sort,
Natinf	nat-inf	sort,
None	option	constant, Option('a)
Option	option	sort,
Set	set-basic	sort,
Some	option	function, 'a → Option('a)
Stream	stream-basic	sort,
[]	stream	constant, Stream('a)
[]	list-data	constant, List('a)
\	set-union	function, Set('a) × Set('a) → Set('a)
]	list-getput	partial function, List('a) × Nat × 'a → List('a)
]	list-getput	partial function, List('a) × Nat → 'a
]	stream	partial function, Stream('a) × Nat × 'a → Stream('a)
]	stream	partial function, Stream('a) × Nat → 'a
^	Koenigs-Lemma-gen	function, List('a) → List('a) × Nat → List('a) → List('a)
a	list-getput	variable, 'a
a	list-del	variable, 'a
a	IOtrace-lift	variable, 'a
a	wellfounded	variable, 'a
a	Koenigs-Lemma-gen	variable, 'a
a	list-dup	variable, 'a
a	infgraph-gen-basic	variable, 'a
a	remtau-cont	variable, 'a
a	list	variable, 'a
a	product-refine	variable, 'a
a	infinite-append	variable, 'a
a	IOtrace	variable, 'a
a	stream	variable, 'a
a	funops	variable, 'a
a	list-data	variable, 'a
a	list-last	variable, 'a
a	set-basic	variable, 'a
a	product	variable, 'a
a	infgraph-gen	variable, 'a
a	set-union	variable, 'a
a	remtau	variable, 'a
a	streamseq-mon-lim	variable, 'a
a	IO-Automaton	variable, 'a
a	IO-Aut-data	variable, 'a
a	contfun-lim	variable, 'a
aINV	IObackward-INV	variable, 'as → Bool
aINV	IOrefine-conds	variable, 'as → Bool
aINV	IObackward-INV-is-leqstarrefine	variable, 'as → Bool
aINV	IOrefine-conds-imply-IOrefine	variable, 'as → Bool
aINV	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'as → Bool
aa	IObackward-INV	variable, 'aa
aa	IOrefine-conds	variable, 'aa
aa	IObackward-INV-is-leqstarrefine	variable, 'aa
aa	product-refine	variable, 'aa
aa	IOrefine-conds-imply-IOrefine	variable, 'aa
aa	IOrefine-def	variable, 'aa
aa	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'aa
aabs	IOrefine-conds	variable, 'ca → Option('aa)
aabs	IOrefine-conds-imply-IOrefine	variable, 'ca → Option('aa)
aaf	product-refine	variable, Nat → 'aa
aaf	IOrefine-conds-imply-IOrefine	variable, Nat → 'aa
aaf	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → 'aa
aal	IObackward-INV	variable, List('aa)
aal	IOrefine-conds	variable, List('aa)
aal	IObackward-INV-is-leqstarrefine	variable, List('aa)
aal	product-refine	variable, List('aa)
aal	IOrefine-conds-imply-IOrefine	variable, List('aa)
aal	IOrefine-def	variable, List('aa)
aal	weakfin-startfin-IObackward-INV-is-leqrefine	variable, List('aa)
aext	IObackward-INV	variable, 'aa → Option('e)
aext	IOrefine-conds	variable, 'aa → Option('e)
aext	IObackward-INV-is-leqstarrefine	variable, 'aa → Option('e)
aext	product-refine	variable, 'aa → Option('e)
aext	IOrefine-conds-imply-IOrefine	variable, 'aa → Option('e)
aext	IOrefine-def	variable, 'aa → Option('e)
aext	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'aa → Option('e)
af	IOtrace-lift	variable, Nat → 'a
af	wellfounded	variable, 'a → 'a
af	remtau-cont	variable, Nat → 'a
af	IOtrace	variable, Nat → 'a
af	remtau	variable, Nat → 'a
af	contfun-lim	variable, Nat → 'a
aioaut	IObackward-INV	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IOrefine-conds	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IObackward-INV-is-leqstarrefine	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IOrefine-conds-imply-IOrefine	variable, IOAutomaton('as, 'aa, 'e)
aioaut	IOrefine-def	variable, IOAutomaton('as, 'aa, 'e)
aioaut	weakfin-startfin-IObackward-INV-is-leqrefine	variable, IOAutomaton('as, 'aa, 'e)
al	IOtrace-lift	variable, List('a)
al	remtau-cont	variable, List('a)
al	IOtrace	variable, List('a)
al	remtau	variable, List('a)
al	contfun-lim	variable, List('a)
alf	IOtrace	variable, Nat → List('a)
alf	contfun-lim	variable, Nat → List('a)
allreachable	Koenigs-Lemma-gen	predicate, Graph('a)
alp	contfun-lim	variable, List('a) → Bool
aren	product-refine	variable, 'aa → 'pa
as	IObackward-INV	variable, 'as
as	IOrefine-conds	variable, 'as
as	IObackward-INV-is-leqstarrefine	variable, 'as
as	product-refine	variable, 'as
as	IOrefine-conds-imply-IOrefine	variable, 'as
as	IOrefine-def	variable, 'as
as	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'as
as'	IOrefine-conds	variable, 'as
as'	IOrefine-conds-imply-IOrefine	variable, 'as
asf	IObackward-INV	variable, Nat → 'as
asf	IOrefine-conds	variable, Nat → 'as
asf	IObackward-INV-is-leqstarrefine	variable, Nat → 'as
asf	product-refine	variable, Nat → 'as
asf	IOrefine-conds-imply-IOrefine	variable, Nat → 'as
asf	IOrefine-def	variable, Nat → 'as
asf	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → 'as
asl	IObackward-INV	variable, List('as)
asl	IOrefine-conds	variable, List('as)
asl	IObackward-INV-is-leqstarrefine	variable, List('as)
asl	product-refine	variable, List('as)
asl	IOrefine-conds-imply-IOrefine	variable, List('as)
asl	IOrefine-def	variable, List('as)
asl	weakfin-startfin-IObackward-INV-is-leqrefine	variable, List('as)
asn	IOrefine-conds-imply-IOrefine	variable, ('as, Nat)
asn	weakfin-startfin-IObackward-INV-is-leqrefine	variable, ('as, Nat)
asn-s	IOrefine-conds-imply-IOrefine	variable, Set(('as, Nat))
asn-s	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Set(('as, Nat))
asnf	IOrefine-conds-imply-IOrefine	variable, Nat → ('as, Nat)
asnf	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → ('as, Nat)
ass	IOrefine-conds	variable, Set('as)
ass	IOrefine-conds-imply-IOrefine	variable, Set('as)
ass	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Set('as)
astart	IObackward-INV	variable, 'as → Bool
astart	IOrefine-conds	variable, 'as → Bool
astart	IObackward-INV-is-leqstarrefine	variable, 'as → Bool
astart	product-refine	variable, 'as → Bool
astart	IOrefine-conds-imply-IOrefine	variable, 'as → Bool
astart	IOrefine-def	variable, 'as → Bool
astart	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'as → Bool
astep	IObackward-INV	variable, 'as × 'aa × 'as → Bool
astep	IOrefine-conds	variable, 'as × 'aa × 'as → Bool
astep	IObackward-INV-is-leqstarrefine	variable, 'as × 'aa × 'as → Bool
astep	product-refine	variable, 'as × 'aa × 'as → Bool
astep	IOrefine-conds-imply-IOrefine	variable, 'as × 'aa × 'as → Bool
astep	IOrefine-def	variable, 'as × 'aa × 'as → Bool
astep	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'as × 'aa × 'as → Bool
aα	IObackward-INV	variable, Stream('aa)
aα	IOrefine-conds	variable, Stream('aa)
aα	IObackward-INV-is-leqstarrefine	variable, Stream('aa)
aα	product-refine	variable, Stream('aa)
aα	IOrefine-conds-imply-IOrefine	variable, Stream('aa)
aα	IOrefine-def	variable, Stream('aa)
aα	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Stream('aa)
aσ	IObackward-INV	variable, Stream('as)
aσ	IOrefine-conds	variable, Stream('as)
aσ	IObackward-INV-is-leqstarrefine	variable, Stream('as)
aσ	product-refine	variable, Stream('as)
aσ	IOrefine-conds-imply-IOrefine	variable, Stream('as)
aσ	IOrefine-def	variable, Stream('as)
aσ	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Stream('as)
b	list-getput	variable, 'a
b	option	variable, 'b
b	list-del	variable, 'a
b	wellfounded	variable, 'b
b	Koenigs-Lemma-gen	variable, 'a
b	list-dup	variable, 'a
b	infgraph-gen-basic	variable, 'a
b	list	variable, 'b
b	funops	variable, 'b
b	list-last	variable, 'a
b	infgraph-gen	variable, 'a
b	set-union	variable, 'b
b	streamseq-mon-lim	variable, 'a
b	contfun-lim	variable, 'b
ba	IOrefine-conds	variable, 'ba
ba	IOrefine-conds-imply-IOrefine	variable, 'ba
bal	IOrefine-conds	variable, List('ba)
bal	IOrefine-conds-imply-IOrefine	variable, List('ba)
bc	wellfounded	variable, ('b, 'c)
bext	IOrefine-conds	variable, 'ba → Option('e)
bext	IOrefine-conds-imply-IOrefine	variable, 'ba → Option('e)
bf	contfun-lim	variable, Nat → 'b
bfwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'as × 'cs → Bool
bioaut	IOrefine-conds	variable, IOAutomaton('bs, 'ba, 'e)
bioaut	IOrefine-conds-imply-IOrefine	variable, IOAutomaton('bs, 'ba, 'e)
bl	contfun-lim	variable, List('b)
bs	IOrefine-conds	variable, 'bs
bs	IOrefine-conds-imply-IOrefine	variable, 'bs
bsf	IOrefine-conds	variable, Nat → 'bs
bsf	IOrefine-conds-imply-IOrefine	variable, Nat → 'bs
bsl	IOrefine-conds	variable, List('bs)
bsl	IOrefine-conds-imply-IOrefine	variable, List('bs)
bstart	IOrefine-conds	variable, 'bs → Bool
bstart	IOrefine-conds-imply-IOrefine	variable, 'bs → Bool
bstep	IOrefine-conds	variable, 'bs × 'ba × 'bs → Bool
bstep	IOrefine-conds-imply-IOrefine	variable, 'bs × 'ba × 'bs → Bool
bwsim	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool
bwsim	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool × 'cs → Bool × 'as → Bool
bwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool
bwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool × 'cs → Bool × 'as → Bool
bα	IOrefine-conds	variable, Stream('ba)
bα	IOrefine-conds-imply-IOrefine	variable, Stream('ba)
bσ	IOrefine-conds	variable, Stream('bs)
bσ	IOrefine-conds-imply-IOrefine	variable, Stream('bs)
c	list-getput	variable, 'a
c	wellfounded	variable, 'c
c	list-dup	variable, 'a
c	funops	variable, 'c
c	list-last	variable, 'a
cINV	IObackward-INV	variable, 'cs → Bool
cINV	IOrefine-conds	variable, 'cs → Bool
cINV	IObackward-INV-is-leqstarrefine	variable, 'cs → Bool
cINV	IOrefine-conds-imply-IOrefine	variable, 'cs → Bool
cINV	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'cs → Bool
ca	IObackward-INV	variable, 'ca
ca	IOrefine-conds	variable, 'ca
ca	IObackward-INV-is-leqstarrefine	variable, 'ca
ca	product-refine	variable, 'ca
ca	IOrefine-conds-imply-IOrefine	variable, 'ca
ca	IOrefine-def	variable, 'ca
ca	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'ca
caf	product-refine	variable, Nat → 'ca
caf	IOrefine-conds-imply-IOrefine	variable, Nat → 'ca
caf	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → 'ca
cal	IObackward-INV	variable, List('ca)
cal	IOrefine-conds	variable, List('ca)
cal	IObackward-INV-is-leqstarrefine	variable, List('ca)
cal	product-refine	variable, List('ca)
cal	IOrefine-conds-imply-IOrefine	variable, List('ca)
cal	IOrefine-def	variable, List('ca)
cal	weakfin-startfin-IObackward-INV-is-leqrefine	variable, List('ca)
cext	IObackward-INV	variable, 'ca → Option('e)
cext	IOrefine-conds	variable, 'ca → Option('e)
cext	IObackward-INV-is-leqstarrefine	variable, 'ca → Option('e)
cext	product-refine	variable, 'ca → Option('e)
cext	IOrefine-conds-imply-IOrefine	variable, 'ca → Option('e)
cext	IOrefine-def	variable, 'ca → Option('e)
cext	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'ca → Option('e)
cf	Koenigs-Lemma-gen	variable, List('a) → List('a)
chn	wellfounded	variable, Nat → 'a
chngen	wellfounded	variable, Nat → Nat → 'a
cioaut	IObackward-INV	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IOrefine-conds	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IObackward-INV-is-leqstarrefine	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IOrefine-conds-imply-IOrefine	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	IOrefine-def	variable, IOAutomaton('cs, 'ca, 'e)
cioaut	weakfin-startfin-IObackward-INV-is-leqrefine	variable, IOAutomaton('cs, 'ca, 'e)
cod	funops	function, 'a → 'b → 'b → Bool
cont	contfun-lim	predicate, Stream('s) × Stream('a) → Stream('b)
cont	contfun-lim	predicate, Stream('a) → Stream('b)
cren	product-refine	variable, 'ca → 'pa
cs	IObackward-INV	variable, 'cs
cs	IOrefine-conds	variable, 'cs
cs	IObackward-INV-is-leqstarrefine	variable, 'cs
cs	product-refine	variable, 'cs
cs	IOrefine-conds-imply-IOrefine	variable, 'cs
cs	IOrefine-def	variable, 'cs
cs	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'cs
cs'	IOrefine-conds	variable, 'cs
cs'	IOrefine-conds-imply-IOrefine	variable, 'cs
csf	IObackward-INV	variable, Nat → 'cs
csf	IOrefine-conds	variable, Nat → 'cs
csf	IObackward-INV-is-leqstarrefine	variable, Nat → 'cs
csf	product-refine	variable, Nat → 'cs
csf	IOrefine-conds-imply-IOrefine	variable, Nat → 'cs
csf	IOrefine-def	variable, Nat → 'cs
csf	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → 'cs
csl	IObackward-INV	variable, List('cs)
csl	IOrefine-conds	variable, List('cs)
csl	IObackward-INV-is-leqstarrefine	variable, List('cs)
csl	product-refine	variable, List('cs)
csl	IOrefine-conds-imply-IOrefine	variable, List('cs)
csl	IOrefine-def	variable, List('cs)
csl	weakfin-startfin-IObackward-INV-is-leqrefine	variable, List('cs)
cstart	IObackward-INV	variable, 'cs → Bool
cstart	IOrefine-conds	variable, 'cs → Bool
cstart	IObackward-INV-is-leqstarrefine	variable, 'cs → Bool
cstart	product-refine	variable, 'cs → Bool
cstart	IOrefine-conds-imply-IOrefine	variable, 'cs → Bool
cstart	IOrefine-def	variable, 'cs → Bool
cstart	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'cs → Bool
cstep	IObackward-INV	variable, 'cs × 'ca × 'cs → Bool
cstep	IOrefine-conds	variable, 'cs × 'ca × 'cs → Bool
cstep	IObackward-INV-is-leqstarrefine	variable, 'cs × 'ca × 'cs → Bool
cstep	product-refine	variable, 'cs × 'ca × 'cs → Bool
cstep	IOrefine-conds-imply-IOrefine	variable, 'cs × 'ca × 'cs → Bool
cstep	IOrefine-def	variable, 'cs × 'ca × 'cs → Bool
cstep	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'cs × 'ca × 'cs → Bool
cα	IObackward-INV	variable, Stream('ca)
cα	IOrefine-conds	variable, Stream('aa)
cα	IObackward-INV-is-leqstarrefine	variable, Stream('ca)
cα	product-refine	variable, Stream('ca)
cα	IOrefine-conds-imply-IOrefine	variable, Stream('aa)
cα	IOrefine-def	variable, Stream('aa)
cα	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Stream('ca)
cσ	IObackward-INV	variable, Stream('cs)
cσ	IOrefine-conds	variable, Stream('cs)
cσ	IObackward-INV-is-leqstarrefine	variable, Stream('cs)
cσ	product-refine	variable, Stream('cs)
cσ	IOrefine-conds-imply-IOrefine	variable, Stream('cs)
cσ	IOrefine-def	variable, Stream('cs)
cσ	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Stream('cs)
disj	list-dup	predicate, List('a) × List('a)
disjoint	set-union	predicate, Set('a) × Set('a)
dom	infgraph-gen-basic	function, Graph('a) → 'a → Bool
dups	list-dup	predicate, List('a)
e	IOtrace-lift	variable, 'e
e	remtau-cont	variable, 'e
e	project-right	variable, 'e
e	product-refine	variable, 'e
e	IOtrace	variable, 'e
e	product	variable, 'e
e	remtau	variable, 'e
e	IO-Automaton	variable, 'e
e	IO-Aut-data	variable, 'e
eP	Koenigs-Lemma-gen	variable, 'a → Bool
eP	infgraph-gen	variable, 'a → Bool
edge	infgraph-gen-basic	function, Graph('a) → 'a × 'a → Bool
ef	IOtrace-lift	variable, Nat → 'e
ef	remtau-cont	variable, Nat → 'e
ef	project-right	variable, Nat → 'e
ef	IOtrace	variable, Nat → 'e
ef	remtau	variable, Nat → 'e
ef	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat → 'e
el	IOtrace-lift	variable, List('e)
el	IObackward-INV	variable, List('e)
el	IOrefine-conds	variable, List('e)
el	IObackward-INV-is-leqstarrefine	variable, List('e)
el	remtau-cont	variable, List('e)
el	project-right	variable, List('e)
el	product-refine	variable, List('e)
el	IOtrace	variable, List('e)
el	IOrefine-conds-imply-IOrefine	variable, List('e)
el	remtau	variable, List('e)
el	IOrefine-def	variable, List('e)
el	weakfin-startfin-IObackward-INV-is-leqrefine	variable, List('e)
es	infgraph-gen-basic	variable, 'a × 'a → Bool
exec	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
exec*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
execω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
ext	IOtrace-lift	variable, 'a → Option('e)
ext	remtau-cont	variable, 'a → Option('e)
ext	product-refine	variable, 'a → Option('e)
ext	IOtrace	variable, 'a → Option('e)
ext	remtau	variable, 'a → Option('e)
ext	IO-Automaton	variable, 'a → Option('e)
ext	IO-Aut-data	variable, 'a → Option('e)
f	option	variable, 'a → 'b
f	list-del	variable, 'a → 'b
f	stream-basic	variable, Nat → 'a
f	list	variable, 'a → 'b
f	infinite-append	variable, 'a → 'a
f	funops	variable, 'a → 'b
f	set-union	variable, 'a → 'b
f	contfun-lim	variable, Stream('a) → Stream('b)
fillfirst	list-last	function, Nat × 'a × List('a) → List('a)
finout	Koenigs-Lemma-gen	predicate, Graph('a)
finp	stream-basic	predicate, Stream('a)
finroot	Koenigs-Lemma-gen	predicate, Graph('a)
frag	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
frag*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
fragv	IOtrace	variable, Stream('s) × Stream('a) → Bool
fragω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
frome	list-del	function, List('a) × 'a → List('a)
fu	project-right	function, 'la → 'pa × 'ra → 'pa → 'pa → Option('pa)
fwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'as × 'cs → Bool
g	Koenigs-Lemma-gen	variable, Graph('a)
g	infgraph-gen-basic	variable, Graph('a)
g	funops	variable, 'b → 'c
g	infgraph-gen	variable, Graph('a)
g1	infgraph-gen-basic	variable, Graph('a)
g2	infgraph-gen-basic	variable, Graph('a)
h	funops	variable, 'a → 'c
haspathanylength	Koenigs-Lemma-gen	function, Graph('a) → 'a → Bool
hd	stream	partial function, Stream('a) → 'a
head	list-data	variable, 'a
hideext	project-right	variable, 'e → Option('f)
hideext	product	variable, 'e → Option('f)
hidingok	product	predicate, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa × 'e → Option('f)
iNV	IOtrace	variable, 's → Bool
ii	infinite-append	variable, Nat → Nat
ii	IOtrace	variable, Nat → Nat
ii	streamseq-mon-lim	variable, Nat → Nat
iigen	infinite-append	variable, Nat → Nat → Nat
imfinbwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool × 'cs → Bool × 'as → Bool
infgraph	Koenigs-Lemma-gen	predicate, Graph('a)
inj	funops	predicate, 'a → 'b
ioa	IOtrace-lift	variable, IOAutomaton('s, 'a, 'e)
ioa	IOtrace	variable, IOAutomaton('s, 'a, 'e)
ioa	IO-Automaton	variable, IOAutomaton('s, 'a, 'e)
ioaut	IO-Aut-data	variable, IOAutomaton('s, 'a, 'e)
isroot	infgraph-gen	function, Graph('a) → 'a → Bool
jj	infinite-append	variable, Nat → Nat
l	stream-basic	variable, List('a)
la	project-right	variable, 'la
la	product	variable, 'la
laf	project-right	variable, Nat → 'la
lal	project-right	variable, List('la)
lext	project-right	variable, 'la → Option('e)
lext	product	variable, 'la → Option('e)
lf	infinite-append	variable, Nat → List('a)
lf	streamseq-mon-lim	variable, Nat → List('a)
lf	contfun-lim	variable, List('a) → List('b)
lfgen	infinite-append	variable, Nat → Nat → List('a)
lift	product-refine	function, List('as) × 's → List(('s, 'as))
lift	contfun-lim	partial function, List('s) × List('a) → List('b) → Stream('s) × Stream('a) → Stream('b)
lift	contfun-lim	partial function, List('a) → List('b) → Stream('a) → Stream('b)
lift	contfun-lim	function, List('s) × List('a) → Bool → Stream('s) × Stream('a) → Bool
lift	contfun-lim	function, List('a) → Bool → Stream('a) → Bool
lifted	contfun-lim	function, List('s) × List('a) → Bool → (List('s) × List('a) → List('b)) × (Stream('s) × Stream('a) → Stream('b)) → Bool
lifted	contfun-lim	function, List('a) → Bool → (List('a) → List('b)) × (Stream('a) → Stream('b)) → Bool
lim	streamseq-mon-lim	partial function, Stream(Stream('a)) → Stream('a)
lioaut	product	variable, IOAutomaton('ls, 'la, 'e)
lren	project-right	variable, 'la → 'pa
lren	product	variable, 'la → 'pa
ls	project-right	variable, 'ls
ls	product	variable, 'ls
lsf	project-right	variable, Nat → 'ls
lsl	project-right	variable, List('ls)
lstart	project-right	variable, 'ls → Bool
lstart	product	variable, 'ls → Bool
lstep	project-right	variable, 'ls × 'la × 'ls → Bool
lstep	product	variable, 'ls × 'la × 'ls → Bool
lα	project-right	variable, Stream('la)
lσ	project-right	variable, Stream('ls)
m	list-getput	variable, Nat
m	list-del	variable, Nat
m	Koenigs-Lemma-gen	variable, Nat
m	nat-inf	variable, Nat
m	stream-basic	variable, Nat
m	remtau-cont	variable, Nat
m	infinite-append	variable, Nat
m	IOtrace	variable, Nat
m	stream	variable, Nat
m	list-last	variable, Nat
m	set-union	variable, Nat
m	remtau	variable, Nat
m	streamseq-mon-lim	variable, Nat
min	nat-inf	function, Natinf × Natinf → Natinf
min	min-of-Pnat	function, Nat → Bool → Nat
mklist	list-last	function, 'a × Nat → List('a)
mon	streamseq-mon-lim	predicate, Stream(Stream('a))
mon	contfun-lim	predicate, List('s) × List('a) → List('b)
mon	contfun-lim	predicate, List('a) → List('b)
mon	contfun-lim	predicate, Stream('s) × Stream('a) → Stream('b)
mon	contfun-lim	predicate, Stream('a) → Stream('b)
move	IOtrace	function, IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
movev	IOtrace	variable, 's × Stream('e) × 's → Bool
n	list-getput	variable, Nat
n	list-del	variable, Nat
n	Koenigs-Lemma-gen	variable, Nat
n	nat-inf	variable, Nat
n	remtau-cont	variable, Nat
n	project-right	variable, Nat
n	product-refine	variable, Nat
n	infinite-append	variable, Nat
n	IOtrace	variable, Nat
n	stream	variable, Nat
n	IOrefine-conds-imply-IOrefine	variable, Nat
n	list-data	variable, Nat
n	list-last	variable, Nat
n	infgraph-gen	variable, Nat
n	set-union	variable, Nat
n	remtau	variable, Nat
n	streamseq-mon-lim	variable, Nat
n	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Nat
n	contfun-lim	variable, Nat
nexta	infinite-append	variable, Nat × 'a → 'a
nextj	infinite-append	variable, Nat × 'a → Nat
nextl	infinite-append	variable, Nat × 'a → List('a)
nf	stream-basic	variable, Nat → 'a
nf	infinite-append	variable, Nat → 'a
nf	stream	variable, Nat → 'a
nf	streamseq-mon-lim	variable, Nat → 'a
nfgen	infinite-append	variable, Nat → Nat → 'a
nfwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'as × 'cs → Bool × 'cs × 'ca × 'cs × 'as → Nat
nnf	streamseq-mon-lim	variable, Nat → Nat
nounsharedextR	product-refine	predicate, 'ca → 'pa × 'ca → Option('e) × 'a → 'pa
np	streamseq-mon-lim	variable, Nat → Bool
n∞	nat-inf	variable, Natinf
n∞	stream	variable, Natinf
n∞	streamseq-mon-lim	variable, Natinf
o	option	function, 'b → Option('c) × 'a → Option('b) → 'a → Option('c)
o	funops	function, 'a → 'b × 'b → 'c → 'a → 'c
oe	remtau-cont	variable, Option('e)
oe	IOtrace	variable, Option('e)
oe	remtau	variable, Option('e)
oe	IO-Automaton	variable, Option('e)
oe	IO-Aut-data	variable, Option('e)
of	option	variable, 'a → Option('b)
og	option	variable, 'b → Option('c)
oinj	option	predicate, 'a → Option('b)
opt	option	variable, Option('a)
osurj	option	predicate, 'a → Option('b)
p	wellfounded	variable, 'a → Bool
p	set-union	variable, 'a → Bool
p	streamseq-mon-lim	variable, 'a → Bool
pa	project-right	variable, 'pa
pa	product-refine	variable, 'pa
pa	product	variable, 'pa
paf	project-right	variable, Nat → 'pa
paf	product-refine	variable, Nat → 'pa
pal	project-right	variable, List('pa)
pal	product-refine	variable, List('pa)
pas	product-refine	variable, ('s, 'as)
pasf	product-refine	variable, Nat → ('s, 'as)
pasl	product-refine	variable, List(('s, 'as))
pastart	product-refine	variable, ('s, 'as) → Bool
pastep	product-refine	variable, ('s, 'as) × 'pa × ('s, 'as) → Bool
path	infgraph-gen	function, Graph('a) → 'a × 'a → Bool
pathp	infgraph-gen	function, Graph('a) → Stream('a) → Bool
paσ	product-refine	variable, Stream(('s, 'as))
pbd	contfun-lim	predicate, Stream('s) × Stream('a) → Stream('b)
pbd	contfun-lim	predicate, Stream('a) → Stream('b)
pcont	contfun-lim	function, Stream('s) × Stream('a) → Bool → (Stream('s) × Stream('a) → Stream('b)) → Bool
pcont	contfun-lim	function, Stream('a) → Bool → (Stream('a) → Stream('b)) → Bool
pcs	product-refine	variable, ('s, 'cs)
pcsf	product-refine	variable, Nat → ('s, 'cs)
pcsl	product-refine	variable, List(('s, 'cs))
pcstart	product-refine	variable, ('s, 'cs) → Bool
pcstep	product-refine	variable, ('s, 'cs) × 'pa × ('s, 'cs) → Bool
pcσ	product-refine	variable, Stream(('s, 'cs))
pext	product-refine	variable, 'pa → Option('e)
pext	product	variable, 'pa → Option('e)
pfxclosed	contfun-lim	predicate, List('s) × List('a) → Bool
pfxclosed	contfun-lim	predicate, Stream('s) × Stream('a) → Bool
pfxclosed	contfun-lim	predicate, List('a) → Bool
pfxclosed	contfun-lim	predicate, Stream('a) → Bool
pioaut	product	variable, IOAutomaton(('ls, 'rs), 'pa, 'e)
pmon	contfun-lim	function, List('s) × List('a) → Bool → (List('s) × List('a) → List('b)) → Bool
pmon	contfun-lim	function, Stream('s) × Stream('a) → Bool → (Stream('s) × Stream('a) → Stream('b)) → Bool
pmon	contfun-lim	function, List('a) → Bool → (List('a) → List('b)) → Bool
pmon	contfun-lim	function, Stream('a) → Bool → (Stream('a) → Stream('b)) → Bool
pnat	min-of-Pnat	variable, Nat → Bool
ppbd	contfun-lim	function, Stream('s) × Stream('a) → Bool → (Stream('s) × Stream('a) → Stream('b)) → Bool
ppbd	contfun-lim	function, Stream('a) → Bool → (Stream('a) → Stream('b)) → Bool
ps	project-right	variable, ('ls, 'rs)
ps	product	variable, ('ls, 'rs)
psf	project-right	variable, Nat → ('ls, 'rs)
psl	project-right	variable, List(('ls, 'rs))
pstart	product	variable, ('ls, 'rs) → Bool
pstep	product	variable, ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) → ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool
pα	project-right	variable, Stream('pa)
pα	product-refine	variable, Stream('pa)
pσ	project-right	variable, Stream(('ls, 'rs))
q	wellfounded	variable, 'b × 'c → Bool
r	IOrefine-conds	variable, 'as × 'cs → Bool
r	IOrefine-conds-imply-IOrefine	variable, 'as × 'cs → Bool
ra	project-right	variable, 'ra
ra	product	variable, 'ra
rab	IOrefine-conds	variable, 'as × 'bs → Bool
rab	IOrefine-conds-imply-IOrefine	variable, 'as × 'bs → Bool
raf	project-right	variable, Nat → 'ra
ral	project-right	variable, List('ra)
rbc	IOrefine-conds	variable, 'bs × 'cs → Bool
rbc	IOrefine-conds-imply-IOrefine	variable, 'bs × 'cs → Bool
reach	Koenigs-Lemma-gen	function, Graph('a) → Set('a) × Nat → 'a → Bool
reach≤	Koenigs-Lemma-gen	function, Graph('a) → Set('a) × Nat → 'a → Bool
redext	product-refine	variable, 'e → Option('f)
ren	product-refine	variable, 'a → 'pa
ren	product	variable, 'a → 'b
repla	product-refine	function, 's × 'a × 's → Bool × 'cs × 'ca × 'cs → Bool × 'ca → 'pa × 'a → 'pa × 'aa → 'pa × 'ca → Option('e) × 'aa → Option('e) × List(('s, 'cs)) × List('pa) × Stream('as) × Stream('aa) → List('pa)
repla	product-refine	function, 's × 'a × 's → Bool × 'cs × 'ca × 'cs → Bool × 'ca → 'pa × 'a → 'pa × 'aa → 'pa × 'ca → Option('e) × 'aa → Option('e) × Stream(('s, 'cs)) × Stream('pa) × Stream('as) × Stream('aa) → Stream('pa)
repls	product-refine	function, 's × 'a × 's → Bool × 'cs × 'ca × 'cs → Bool × 'ca → 'pa × 'a → 'pa × 'aa → 'pa × 'ca → Option('e) × 'aa → Option('e) × List(('s, 'cs)) × List('pa) × Stream('as) × Stream('aa) → List(('s, 'as))
repls	product-refine	function, 's × 'a × 's → Bool × 'cs × 'ca × 'cs → Bool × 'ca → 'pa × 'a → 'pa × 'aa → 'pa × 'ca → Option('e) × 'aa → Option('e) × Stream(('s, 'cs)) × Stream('pa) × Stream('as) × Stream('aa) → Stream(('s, 'as))
rev	list-last	function, List('a) → List('a)
rext	project-right	variable, 'ra → Option('e)
rext	product	variable, 'ra → Option('e)
rf	Koenigs-Lemma-gen	variable, Set('a) × Nat → 'a → Bool
rioaut	product	variable, IOAutomaton('rs, 'ra, 'e)
rren	project-right	variable, 'ra → 'pa
rren	product	variable, 'ra → 'pa
rs	project-right	variable, 'rs
rs	product	variable, 'rs
rsf	project-right	variable, Nat → 'rs
rsl	project-right	variable, List('rs)
rstart	project-right	variable, 'rs → Bool
rstart	product	variable, 'rs → Bool
rstep	project-right	variable, 'rs × 'ra × 'rs → Bool
rstep	product	variable, 'rs × 'ra × 'rs → Bool
rα	project-right	variable, Stream('ra)
rσ	project-right	variable, Stream('rs)
s	IOtrace-lift	variable, 's
s	list-to-set	variable, 's
s	Koenigs-Lemma-gen	variable, Set('a)
s	product-refine	variable, 's
s	IOtrace	variable, 's
s	set-basic	variable, Set('a)
s	set-union	variable, Set('a)
s	IO-Automaton	variable, 's
s	IO-Aut-data	variable, 's
sameshared	product-refine	predicate, 'ca → 'pa × 'aa → 'pa × 'a → 'pa
sf	IOtrace-lift	variable, Nat → 's
sf	IOtrace	variable, Nat → 's
sf	contfun-lim	variable, Nat → 's
sharingok	product	predicate, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa
simplefwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'as × 'cs → Bool × 'ca → Option('aa)
size01f	IOrefine-conds	variable, 'cs × 'ca × 'cs × 'as → Nat
size01f	IOrefine-conds-imply-IOrefine	variable, 'cs × 'ca × 'cs × 'as → Nat
sl	IOtrace-lift	variable, List('s)
sl	list-to-set	variable, List('s)
sl	IOtrace	variable, List('s)
sl	contfun-lim	variable, List('s)
slf	IOtrace	variable, Nat → List('s)
start	IOtrace-lift	variable, 's → Bool
start	product-refine	variable, 's → Bool
start	IOtrace	variable, 's → Bool
start	IO-Automaton	variable, 's → Bool
start	IO-Aut-data	variable, 's → Bool
step	IOtrace-lift	variable, 's × 'a × 's → Bool
step	product-refine	variable, 's × 'a × 's → Bool
step	IOtrace	variable, 's × 'a × 's → Bool
step	IO-Automaton	variable, 's × 'a × 's → Bool
step	IO-Aut-data	variable, 's × 'a × 's → Bool
strP	infgraph-gen	variable, Stream('a) → Bool
surj	funops	predicate, 'a → 'b
surj	product	predicate, 'la → 'pa × 'ra → 'pa
t	IObackward-INV	variable, 'cs × 'as → Bool
t	IOrefine-conds	variable, 'cs × 'as → Bool
t	IObackward-INV-is-leqstarrefine	variable, 'cs × 'as → Bool
t	IOrefine-conds-imply-IOrefine	variable, 'cs × 'as → Bool
t	weakfin-startfin-IObackward-INV-is-leqrefine	variable, 'cs × 'as → Bool
tail	list-data	variable, List('a)
tl	stream	partial function, Stream('a) → Stream('a)
trace	IOtrace	function, IOAutomaton('s, 'a, 'e) → Stream('e) → Bool
trace*	IOtrace	function, IOAutomaton('s, 'a, 'e) → List('e) → Bool
tracev	IOtrace	variable, Stream('e) → Bool
traceω	IOtrace	function, IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool
trans	wellfounded	predicate, 'a × 'a → Bool
trf	contfun-lim	variable, List('s) × List('a) → List('b)
trlp	contfun-lim	variable, List('s) × List('a) → Bool
trp	contfun-lim	variable, Stream('s) × Stream('a) → Bool
twf	wellfounded	predicate, 'a × 'a → Bool
twfinv	wellfounded	predicate, 'a × 'a → Bool
vs	infgraph-gen-basic	variable, 'a → Bool
weakbwsim	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool × 'as → Bool
weakbwsim	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × 'cs × 'as → Bool × 'as → Bool
wf	wellfounded	predicate, 'a × 'a → Bool
wf1≪	wellfounded	variable, 'b × 'b → Bool
wf2≪	wellfounded	variable, 'c × 'c → Bool
wfinv	wellfounded	predicate, 'a × 'a → Bool
wf≪	wellfounded	variable, 'a × 'a → Bool
wf≫	wellfounded	variable, 'a × 'a → Bool
x	list-getput	variable, List('a)
x	list-del	variable, List('a)
x	Koenigs-Lemma-gen	variable, List('a)
x	stream-basic	variable, List('a)
x	list-dup	variable, List('a)
x	list	variable, List('a)
x	stream	variable, List('a)
x	list-data	variable, List('a)
x	list-last	variable, List('a)
x	infgraph-gen	variable, List('a)
x	streamseq-mon-lim	variable, List('a)
y	list-getput	variable, List('a)
y	list-del	variable, List('a)
y	list-dup	variable, List('a)
y	list	variable, List('a)
y	stream	variable, List('a)
y	list-data	variable, List('a)
y	list-last	variable, List('a)
z	list-getput	variable, List('a)
z	list-del	variable, List('a)
z	list-dup	variable, List('a)
z	list	variable, List('a)
z	stream	variable, List('a)
z	list-data	variable, List('a)
z	list-last	variable, List('a)
}	list-to-set	function, List('s) → Set('s)
}	set-union	function, 'a → Set('a)
×	infgraph-gen-basic	function, 'a → Bool × 'a × 'a → Bool → Graph('a)
Π	product	partial function, IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × 'la → 'pa × 'ra → 'pa → IOAutomaton(('ls, 'rs), 'pa, 'e)
Π	product	function, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa → 'pa → Option('e)
Π	product	function, 'ls × 'la × 'ls → Bool × 'rs × 'ra × 'rs → Bool × 'la → 'pa × 'ra → 'pa × 'la → Option('e) × 'ra → Option('e) → ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool
Π	product	function, 'ls → Bool × 'rs → Bool → ('ls, 'rs) → Bool
Πh	product	partial function, IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × 'la → 'pa × 'ra → 'pa × 'e → Option('f) → IOAutomaton(('ls, 'rs), 'pa, 'f)
Πh	product	function, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa × 'e → Option('f) → 'pa → Option('f)
Πhok	product	predicate, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa × 'e → Option('f)
Πok	product	predicate, 'la → Option('e) × 'ra → Option('e) × 'la → 'pa × 'ra → 'pa
α	IOtrace-lift	variable, Stream('a)
α	remtau-cont	variable, Stream('a)
α	IOtrace	variable, Stream('a)
α	remtau	variable, Stream('a)
α	contfun-lim	variable, Stream('a)
αf	contfun-lim	variable, Nat → Stream('a)
αp	contfun-lim	variable, Stream('a) → Bool
β	IOtrace-lift	variable, Stream('e)
β	IOrefine-conds	variable, Stream('e)
β	remtau-cont	variable, Stream('e)
β	project-right	variable, Stream('e)
β	product-refine	variable, Stream('e)
β	IOtrace	variable, Stream('e)
β	IOrefine-conds-imply-IOrefine	variable, Stream('e)
β	remtau	variable, Stream('e)
β	IOrefine-def	variable, Stream('e)
β	weakfin-startfin-IObackward-INV-is-leqrefine	variable, Stream('e)
β	contfun-lim	variable, Stream('b)
βf	contfun-lim	variable, Stream('s) × Stream('a) → Stream('b)
πra	project-right	function, 'ls × 'la × 'ls → Bool × 'rs × 'ra × 'rs → Bool × 'la → 'pa × 'ra → 'pa × List(('ls, 'rs)) × List('pa) → List('ra)
πra	project-right	function, 'ls × 'la × 'ls → Bool × 'rs × 'ra × 'rs → Bool × 'la → 'pa × 'ra → 'pa × Stream(('ls, 'rs)) × Stream('pa) → Stream('ra)
πrs	project-right	function, 'ls × 'la × 'ls → Bool × 'rs × 'ra × 'rs → Bool × 'la → 'pa × 'ra → 'pa × List(('ls, 'rs)) × List('pa) → List('rs)
πrs	project-right	function, 'ls × 'la × 'ls → Bool × 'rs × 'ra × 'rs → Bool × 'la → 'pa × 'ra → 'pa × Stream(('ls, 'rs)) × Stream('pa) → Stream('rs)
σ	IOtrace-lift	variable, Stream('s)
σ	stream-basic	variable, Stream('a)
σ	infinite-append	variable, Stream('a)
σ	IOtrace	variable, Stream('s)
σ	stream	variable, Stream('a)
σ	infgraph-gen	variable, Stream('a)
σ	streamseq-mon-lim	variable, Stream('a)
σ	contfun-lim	variable, Stream('s)
σf	streamseq-mon-lim	variable, Nat → Stream('a)
σf	contfun-lim	variable, Nat → Stream('s)
σσ	streamseq-mon-lim	variable, Stream(Stream('a))
∅	set-basic	constant, Set('a)
∈	list	predicate, 'a × List('a)
∈	set-basic	predicate, 'a × Set('a)
∞	nat-inf	constant, Natinf
∩	set-union	function, Set('a) × Set('a) → Set('a)
∪	set-union	function, Set('a) × Set('a) → Set('a)
≤	nat	predicate, Nat × Nat
≤B	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤B	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤BI	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤BI	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤F	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤bF	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤iBI	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤nF	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤sF	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤wB	IObackward-INV	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤wB	IOrefine-conds	predicate, IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≥	nat	predicate, Nat × Nat
⊆	set-basic	predicate, Set('a) × Set('a)
⊑	stream	predicate, Stream('a) × Stream('a)
⊑	list-last	predicate, List('a) × List('a)
⊒	list-last	predicate, List('a) × List('a)
⌝	nat-inf	function, Nat → Natinf
⌝	stream-basic	function, Nat → 'a → Stream('a)
⌝	stream-basic	function, List('a) → Stream('a)