[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('a) → Nat
# .	stream	f	Stream('a) → Natinf
# .	set-basic	f	Set('a) → Nat
. !	remtau	f	('a → Option('e)) → Stream('a) → Stream('e)
. !	remtau	f	('a → Option('e)) → List('a) → List('e)
. '	list	f	'a → List('a)
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-data	f	'a × List('a) → List('a)
. + .	list	f	List('a) × List('a) → List('a)
. + .	list	f	List('a) × 'a → List('a)
. + .	nat-inf	f	Natinf × Natinf → Natinf
. + .	stream	f	'a × Stream('a) → Stream('a)
. + .	stream	f	Stream('a) × Stream('a) → Stream('a)
. + .	stream	f	List('a) × (Nat → 'a) → Nat → 'a
. + .	remtau	f	Option('e) × Stream('e) → Stream('e)
. ++ .	list-dup	f	List('a) × 'a → List('a)
. ++ .	set-basic	f	Set('a) × 'a → Set('a)
. +1	nat-basic	f	Nat → Nat
. +2 .	list	f	'a × 'a → List('a)
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -- .	set-union	f	Set('a) × 'a → Set('a)
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-del	f	List('a) × 'a → List('a)
. -l .	list-del	f	List('a) × 'a → List('a)
. -p .	list-del	f	List('a) × Nat → List('a)
. .butlast	list-last	pf	List('a) → List('a) with λ x. x ≠ []
. .distinct	list-dup	f	List('a) → List('a)
. .drop ( . )	stream	f	(Nat → 'a) × Nat → Nat → 'a
. .drop ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .drop ( . )	stream	pf	Stream('a) × Nat → Stream('a) with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. .dropRight ( . )	list-last	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .exists ( . )	set-union	p	Set('a) × ('a → Bool)
. .ext	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 'a → Option('e)
. .f	stream-basic	pf	Stream('a) → Nat → 'a with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .filter ( . )	set-union	f	Set('a) × ('a → Bool) → Set('a)
. .foldLeft ( . )	list	f	List('a) × 'b × ('b × 'a → 'b) → 'b
. .forall ( . )	set-union	p	Set('a) × ('a → Bool)
. .get	option	pf	Option('a) → 'a with λ opt. opt ≠ None
. .getOrElse ( . )	option	f	Option('a) × 'a → 'a
. .head	list-data	pf	List('a) → 'a with λ x. x ≠ []
. .indexOf ( . )	list-del	f	List('a) × 'a → Nat
. .l	stream-basic	pf	Stream('a) → List('a) with λ σ. finp(σ)
. .last	list-last	pf	List('a) → 'a with λ x. x ≠ []
. .map ( . )	option	f	Option('a) × ('a → 'b) → Option('b)
. .map ( . )	list	f	List('a) × ('a → 'b) → List('b)
. .map ( . )	set-union	f	Set('a) × ('a → 'b) → Set('b)
. .n	nat-inf	pf	Natinf → Nat with λ n∞. n∞ ≠ ∞
. .start	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's → Bool
. .step	IO-Aut-data	f	IOAutomaton('s, 'a, 'e) → 's × 'a × 's → Bool
. .sublist ( . )	list-del	pf	List('a) × Nat × Nat → List('a) with λ x, n, m. n + m ≤ # x
. .tail	list-data	pf	List('a) → List('a) with λ x. x ≠ []
. .take ( . )	stream	f	(Nat → 'a) × Nat → List('a)
. .take ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. .take ( . )	stream	pf	Stream('a) × Nat → List('a) with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. .take ( . )	stream	pf	Stream('a) × Natinf → Stream('a) with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
. .takeRight ( . )	list-del	pf	List('a) × Nat → List('a) with λ x, n. n ≤ # x
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List('a) × List('a)
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. [ . := . ]	list-getput	pf	List('a) × Nat × 'a → List('a) with λ x, n, a. n < # x
. [ . := . ]	stream	pf	Stream('a) × Nat × 'a → Stream('a) with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. [ . ]	list-getput	pf	List('a) × Nat → 'a with λ x, n. n < # x
. [ . ]	stream	pf	Stream('a) × Nat → 'a with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. \ .	set-union	f	Set('a) × Set('a) → Set('a)
. ^ .	Koenigs-Lemma-gen	f	(List('a) → List('a)) × Nat → List('a) → List('a)
. × .	infgraph-gen-basic	f	('a → Bool) × ('a × 'a → Bool) → Graph('a)
. ∈ .	list	p	'a × List('a)
. ∈ .	set-basic	p	'a × Set('a)
. ∩ .	set-union	f	Set('a) × Set('a) → Set('a)
. ∪ .	set-union	f	Set('a) × Set('a) → Set('a)
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	set-basic	p	Set('a) × Set('a)
. ⊑ .	list-last	p	List('a) × List('a)
. ⊑ .	stream	p	Stream('a) × Stream('a)
. ⊒ .	list-last	p	List('a) × List('a)
. o .	option	f	('b → Option('c)) × ('a → Option('b)) → 'a → Option('c)
[]	list-data	c	List('a)
[]	stream	c	Stream('a)
{ . }	set-union	f	'a → Set('a)
β	weakfin-startfin-IObackward-INV-is-leqrefine	v	Stream('e)
∅	set-basic	c	Set('a)
∞	nat-inf	c	Natinf
≤B	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤BI	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤wB	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
⌜ . ⌝	stream-basic	f	List('a) → Stream('a)
⌜ . ⌝	stream-basic	f	(Nat → 'a) → Stream('a)
⌜ . ⌝	nat-inf	f	Nat → Natinf
C_≡*T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡ωT_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≡T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤*T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤ωT_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
C_≤T_A	IOrefine-def	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
Graph	infgraph-gen-basic	s
IOAut	IO-Aut-data	f	('s → Bool) × ('s × 'a × 's → Bool) × ('a → Option('e)) → IOAutomaton('s, 'a, 'e)
IOAut?	IO-Automaton	p	IOAutomaton('s, 'a, 'e)
IOAutomaton	IO-Aut-data	s
List	list-data	s
Nat	nat-basic	s
Natinf	nat-inf	s
None	option	c	Option('a)
Option	option	s
Set	set-basic	s
Some	option	f	'a → Option('a)
Stream	stream-basic	s
aα	weakfin-startfin-IObackward-INV-is-leqrefine	v	Stream('aa)
aσ	weakfin-startfin-IObackward-INV-is-leqrefine	v	Stream('as)
aINV	weakfin-startfin-IObackward-INV-is-leqrefine	v	'as → Bool
aa	weakfin-startfin-IObackward-INV-is-leqrefine	v	'aa
aaf	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → 'aa
aal	weakfin-startfin-IObackward-INV-is-leqrefine	v	List('aa)
aext	weakfin-startfin-IObackward-INV-is-leqrefine	v	'aa → Option('e)
aioaut	weakfin-startfin-IObackward-INV-is-leqrefine	v	IOAutomaton('as, 'aa, 'e)
allreachable	Koenigs-Lemma-gen	p	Graph('a)
as	weakfin-startfin-IObackward-INV-is-leqrefine	v	'as
asf	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → 'as
asl	weakfin-startfin-IObackward-INV-is-leqrefine	v	List('as)
asn	weakfin-startfin-IObackward-INV-is-leqrefine	v	('as, Nat)
asn-s	weakfin-startfin-IObackward-INV-is-leqrefine	v	Set(('as, Nat))
asnf	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → ('as, Nat)
ass	weakfin-startfin-IObackward-INV-is-leqrefine	v	Set('as)
astart	weakfin-startfin-IObackward-INV-is-leqrefine	v	'as → Bool
astep	weakfin-startfin-IObackward-INV-is-leqrefine	v	'as × 'aa × 'as → Bool
bwsim	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool)
bwsim	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool)
cα	weakfin-startfin-IObackward-INV-is-leqrefine	v	Stream('ca)
cσ	weakfin-startfin-IObackward-INV-is-leqrefine	v	Stream('cs)
cINV	weakfin-startfin-IObackward-INV-is-leqrefine	v	'cs → Bool
ca	weakfin-startfin-IObackward-INV-is-leqrefine	v	'ca
caf	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → 'ca
cal	weakfin-startfin-IObackward-INV-is-leqrefine	v	List('ca)
cext	weakfin-startfin-IObackward-INV-is-leqrefine	v	'ca → Option('e)
cioaut	weakfin-startfin-IObackward-INV-is-leqrefine	v	IOAutomaton('cs, 'ca, 'e)
cs	weakfin-startfin-IObackward-INV-is-leqrefine	v	'cs
csf	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → 'cs
csl	weakfin-startfin-IObackward-INV-is-leqrefine	v	List('cs)
cstart	weakfin-startfin-IObackward-INV-is-leqrefine	v	'cs → Bool
cstep	weakfin-startfin-IObackward-INV-is-leqrefine	v	'cs × 'ca × 'cs → Bool
disj	list-dup	p	List('a) × List('a)
disjoint	set-union	p	Set('a) × Set('a)
dom	infgraph-gen-basic	f	Graph('a) → 'a → Bool
dups	list-dup	p	List('a)
edge	infgraph-gen-basic	f	Graph('a) → 'a × 'a → Bool
ef	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat → 'e
el	weakfin-startfin-IObackward-INV-is-leqrefine	v	List('e)
exec	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
exec*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
execω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
fillfirst	list-last	f	Nat × 'a × List('a) → List('a)
finout	Koenigs-Lemma-gen	p	Graph('a)
finp	stream-basic	p	Stream('a)
finroot	Koenigs-Lemma-gen	p	Graph('a)
frag	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool
frag*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool
fragω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool
frome	list-del	f	List('a) × 'a → List('a)
haspathanylength	Koenigs-Lemma-gen	f	Graph('a) → 'a → Bool
hd	stream	pf	Stream('a) → 'a with λ σ. σ ≠ []
infgraph	Koenigs-Lemma-gen	p	Graph('a)
isroot	infgraph-gen	f	Graph('a) → 'a → Bool
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	list-last	f	'a × Nat → List('a)
move	IOtrace	f	IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
n	weakfin-startfin-IObackward-INV-is-leqrefine	v	Nat
oinj	option	p	('a → Option('b))
osurj	option	p	('a → Option('b))
path	infgraph-gen	f	Graph('a) → 'a × 'a → Bool
pathp	infgraph-gen	f	Graph('a) → Stream('a) → Bool
reach	Koenigs-Lemma-gen	f	Graph('a) → Set('a) × Nat → 'a → Bool
reach≤	Koenigs-Lemma-gen	f	Graph('a) → Set('a) × Nat → 'a → Bool
rev	list-last	f	List('a) → List('a)
t	weakfin-startfin-IObackward-INV-is-leqrefine	v	'cs × 'as → Bool
tl	stream	pf	Stream('a) → Stream('a) with λ σ. σ ≠ []
trace	IOtrace	f	IOAutomaton('s, 'a, 'e) → Stream('e) → Bool
trace*	IOtrace	f	IOAutomaton('s, 'a, 'e) → List('e) → Bool
traceω	IOtrace	f	IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool
weakbwsim	IObackward-INV	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('as → Bool)