[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)
β	IOrefine-conds-imply-IOrefine	v	Stream('e)
∅	set-basic	c	Set('a)
∞	nat-inf	c	Natinf
≤B	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤BI	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤F	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤bF	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤iBI	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤nF	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤sF	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e)
≤wB	IOrefine-conds	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α	IOrefine-conds-imply-IOrefine	v	Stream('aa)
aσ	IOrefine-conds-imply-IOrefine	v	Stream('as)
aINV	IOrefine-conds-imply-IOrefine	v	'as → Bool
aa	IOrefine-conds-imply-IOrefine	v	'aa
aabs	IOrefine-conds-imply-IOrefine	v	'ca → Option('aa)
aaf	IOrefine-conds-imply-IOrefine	v	Nat → 'aa
aal	IOrefine-conds-imply-IOrefine	v	List('aa)
aext	IOrefine-conds-imply-IOrefine	v	'aa → Option('e)
aioaut	IOrefine-conds-imply-IOrefine	v	IOAutomaton('as, 'aa, 'e)
allreachable	Koenigs-Lemma-gen	p	Graph('a)
as	IOrefine-conds-imply-IOrefine	v	'as
as'	IOrefine-conds-imply-IOrefine	v	'as
asf	IOrefine-conds-imply-IOrefine	v	Nat → 'as
asl	IOrefine-conds-imply-IOrefine	v	List('as)
asn	IOrefine-conds-imply-IOrefine	v	('as, Nat)
asn-s	IOrefine-conds-imply-IOrefine	v	Set(('as, Nat))
asnf	IOrefine-conds-imply-IOrefine	v	Nat → ('as, Nat)
ass	IOrefine-conds-imply-IOrefine	v	Set('as)
astart	IOrefine-conds-imply-IOrefine	v	'as → Bool
astep	IOrefine-conds-imply-IOrefine	v	'as × 'aa × 'as → Bool
bα	IOrefine-conds-imply-IOrefine	v	Stream('ba)
bσ	IOrefine-conds-imply-IOrefine	v	Stream('bs)
ba	IOrefine-conds-imply-IOrefine	v	'ba
bal	IOrefine-conds-imply-IOrefine	v	List('ba)
bext	IOrefine-conds-imply-IOrefine	v	'ba → Option('e)
bfwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool)
bioaut	IOrefine-conds-imply-IOrefine	v	IOAutomaton('bs, 'ba, 'e)
bs	IOrefine-conds-imply-IOrefine	v	'bs
bsf	IOrefine-conds-imply-IOrefine	v	Nat → 'bs
bsl	IOrefine-conds-imply-IOrefine	v	List('bs)
bstart	IOrefine-conds-imply-IOrefine	v	'bs → Bool
bstep	IOrefine-conds-imply-IOrefine	v	'bs × 'ba × 'bs → Bool
bwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool)
bwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool)
cα	IOrefine-conds-imply-IOrefine	v	Stream('aa)
cσ	IOrefine-conds-imply-IOrefine	v	Stream('cs)
cINV	IOrefine-conds-imply-IOrefine	v	'cs → Bool
ca	IOrefine-conds-imply-IOrefine	v	'ca
caf	IOrefine-conds-imply-IOrefine	v	Nat → 'ca
cal	IOrefine-conds-imply-IOrefine	v	List('ca)
cext	IOrefine-conds-imply-IOrefine	v	'ca → Option('e)
cioaut	IOrefine-conds-imply-IOrefine	v	IOAutomaton('cs, 'ca, 'e)
cs	IOrefine-conds-imply-IOrefine	v	'cs
cs'	IOrefine-conds-imply-IOrefine	v	'cs
csf	IOrefine-conds-imply-IOrefine	v	Nat → 'cs
csl	IOrefine-conds-imply-IOrefine	v	List('cs)
cstart	IOrefine-conds-imply-IOrefine	v	'cs → Bool
cstep	IOrefine-conds-imply-IOrefine	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
el	IOrefine-conds-imply-IOrefine	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)
fwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool)
haspathanylength	Koenigs-Lemma-gen	f	Graph('a) → 'a → Bool
hd	stream	pf	Stream('a) → 'a with λ σ. σ ≠ []
imfinbwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool)
infgraph	Koenigs-Lemma-gen	p	Graph('a)
isroot	infgraph-gen	f	Graph('a) → 'a → Bool
min	nat-inf	f	Natinf × Natinf → Natinf
min	min-of-Pnat	f	(Nat → Bool) → Nat
mklist	list-last	f	'a × Nat → List('a)
move	IOtrace	f	IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool
n	IOrefine-conds-imply-IOrefine	v	Nat
nfwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool) × ('cs × 'ca × 'cs × 'as → 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
r	IOrefine-conds-imply-IOrefine	v	'as × 'cs → Bool
rab	IOrefine-conds-imply-IOrefine	v	'as × 'bs → Bool
rbc	IOrefine-conds-imply-IOrefine	v	'bs × 'cs → 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)
simplefwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool) × ('ca → Option('aa))
size01f	IOrefine-conds-imply-IOrefine	v	'cs × 'ca × 'cs × 'as → Nat
t	IOrefine-conds-imply-IOrefine	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	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('as → Bool)