[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
. '	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
. ++ .	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)
. .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)
. .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 ( . )	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∞ ≠ ∞
. .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)
[]	list-data	c	List('a)
[]	stream	c	Stream('a)
{ . }	set-union	f	'a → Set('a)
∅	set-basic	c	Set('a)
∞	nat-inf	c	Natinf
⌜ . ⌝	stream-basic	f	List('a) → Stream('a)
⌜ . ⌝	stream-basic	f	(Nat → 'a) → Stream('a)
⌜ . ⌝	nat-inf	f	Nat → Natinf
Graph	infgraph-gen-basic	s
List	list-data	s
Nat	nat-basic	s
Natinf	nat-inf	s
Set	set-basic	s
Stream	stream-basic	s
a	Koenigs-Lemma-gen	v	'a
allreachable	Koenigs-Lemma-gen	p	Graph('a)
b	Koenigs-Lemma-gen	v	'a
cf	Koenigs-Lemma-gen	v	List('a) → List('a)
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)
eP	Koenigs-Lemma-gen	v	'a → Bool
edge	infgraph-gen-basic	f	Graph('a) → 'a × '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)
frome	list-del	f	List('a) × 'a → List('a)
g	Koenigs-Lemma-gen	v	Graph('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
m	Koenigs-Lemma-gen	v	Nat
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	list-last	f	'a × Nat → List('a)
n	Koenigs-Lemma-gen	v	Nat
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)
rf	Koenigs-Lemma-gen	v	Set('a) × Nat → 'a → Bool
s	Koenigs-Lemma-gen	v	Set('a)
tl	stream	pf	Stream('a) → Stream('a) with λ σ. σ ≠ []
x	Koenigs-Lemma-gen	v	List('a)