Pair

📁 Source: Cslib/Computability/Automata/NA/Pair.lean

Statistics

Metric	Count
Definitions pairLang, pairViaLang, Pair	3
Theorems language_eq_fin_iSup_hmul_omegaPow, mem_pairLang, mem_pairViaLang, pairLang_append, pairLang_append_pairViaLang, pairLang_regular, pairLang_split, pairViaLang_append_pairLang, pairViaLang_regular, pairViaLang_split	10
Total	13

Cslib.Automata.NA.Buchi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
language_eq_fin_iSup_hmul_omegaPow 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi instωAcceptor Cslib.ωLanguage Cslib.ωLanguage.instCompleteAtomicBooleanAlgebra Cslib.Automata.NA.start toNA accept Cslib.ωLanguage.instHMulLanguage Cslib.LTS.pairLang Cslib.Automata.NA.toLTS Cslib.ωLanguage.OmegaPow.omegaPow Cslib.ωLanguage.instOmegaPowLanguageOfInhabited	—	Cslib.ωLanguage.ext Cslib.ωSequence.frequently_in_finite_type Cslib.ωSequence.frequently_iff_strictMono Cslib.ωLanguage.omegaPow_seq_prop Cslib.ωLanguage.mem_omegaPow Cslib.LTS.ωTr.flatten Cslib.LTS.ωTr.append Cslib.ωSequence.drop_frequently_iff_frequently

Cslib.LTS

Definitions

Name	Category	Theorems
pairLang 📖	CompOp	4 math math: pairViaLang_split, mem_pairLang, pairLang_regular, Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow
pairViaLang 📖	CompOp	2 math math: pairViaLang_regular, mem_pairViaLang

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_pairLang 📖	mathematical	—	pairLang MTr	—	—
mem_pairViaLang 📖	mathematical	—	pairViaLang MTr	—	—
pairLang_append 📖	—	pairLang	—	—	—
pairLang_append_pairViaLang 📖	—	pairLang pairViaLang	—	—	mem_pairViaLang
pairLang_regular 📖	mathematical	—	pairLang	—	Cslib.Language.IsRegular.iff_nfa
pairLang_split 📖	—	pairLang	—	—	MTr.split mem_pairLang
pairViaLang_append_pairLang 📖	—	pairViaLang pairLang	—	—	mem_pairViaLang
pairViaLang_regular 📖	mathematical	—	pairViaLang	—	Cslib.Language.IsRegular.iSup
pairViaLang_split 📖	mathematical	pairViaLang	pairLang	—	mem_pairViaLang MTr.split

Cslib.SKI

Definitions

Name	Category	Theorems
Pair 📖	CompOp	1 math math: pair_def

---

← Back to Index