[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)
. ∈ .	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	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
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	v	Stream('aa)
aσ	IOrefine-conds	v	Stream('as)
aINV	IOrefine-conds	v	'as → Bool
aa	IOrefine-conds	v	'aa
aabs	IOrefine-conds	v	'ca → Option('aa)
aal	IOrefine-conds	v	List('aa)
aext	IOrefine-conds	v	'aa → Option('e)
aioaut	IOrefine-conds	v	IOAutomaton('as, 'aa, 'e)
as	IOrefine-conds	v	'as
as'	IOrefine-conds	v	'as
asf	IOrefine-conds	v	Nat → 'as
asl	IOrefine-conds	v	List('as)
ass	IOrefine-conds	v	Set('as)
astart	IOrefine-conds	v	'as → Bool
astep	IOrefine-conds	v	'as × 'aa × 'as → Bool
bα	IOrefine-conds	v	Stream('ba)
bσ	IOrefine-conds	v	Stream('bs)
ba	IOrefine-conds	v	'ba
bal	IOrefine-conds	v	List('ba)
bext	IOrefine-conds	v	'ba → Option('e)
bfwsim	IOrefine-conds	p	IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('as × 'cs → Bool)
bioaut	IOrefine-conds	v	IOAutomaton('bs, 'ba, 'e)
bs	IOrefine-conds	v	'bs
bsf	IOrefine-conds	v	Nat → 'bs
bsl	IOrefine-conds	v	List('bs)
bstart	IOrefine-conds	v	'bs → Bool
bstep	IOrefine-conds	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	v	Stream('aa)
cσ	IOrefine-conds	v	Stream('cs)
cINV	IOrefine-conds	v	'cs → Bool
ca	IOrefine-conds	v	'ca
cal	IOrefine-conds	v	List('ca)
cext	IOrefine-conds	v	'ca → Option('e)
cioaut	IOrefine-conds	v	IOAutomaton('cs, 'ca, 'e)
cs	IOrefine-conds	v	'cs
cs'	IOrefine-conds	v	'cs
csf	IOrefine-conds	v	Nat → 'cs
csl	IOrefine-conds	v	List('cs)
cstart	IOrefine-conds	v	'cs → Bool
cstep	IOrefine-conds	v	'cs × 'ca × 'cs → Bool
disj	list-dup	p	List('a) × List('a)
disjoint	set-union	p	Set('a) × Set('a)
dups	list-dup	p	List('a)
el	IOrefine-conds	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)
finp	stream-basic	p	Stream('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)
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)
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
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))
r	IOrefine-conds	v	'as × 'cs → Bool
rab	IOrefine-conds	v	'as × 'bs → Bool
rbc	IOrefine-conds	v	'bs × 'cs → 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	v	'cs × 'ca × 'cs × 'as → Nat
t	IOrefine-conds	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)