Standalone Lean project
Shared APIs and formal foundations for computer science, software verification, and certified software in Lean.
Flagship declarations
Cslib.Automata.DA.FinAcc.unique_minimal
Plain-language statement
The minimal DFA M accepting the language l is unique up to unique isomorphism.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_cover
Project documentation
na.buchiFamily is a cover if na has only finitely many states. This theorem uses the Ramsey theorem for infinite graphs and does not depend on any details of na.BuchiCongruence other than that it is of finite index.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.buchiFamily_saturation
Plain-language statement
na.buchiFamily saturates the ω-language accepted by na.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.concat_language_eq
Plain-language statement
The Buchi automaton formed from concat na1 na2 accepts the ω-language that is the concatenation of the language of na1 and the ω-language of na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_acc_freq_acc
Plain-language statement
If the intersection automaton sees one accepting condition infinitely many times, then it sees the other accepting condition infinitely many times as well.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.inter_freq_comp_acc_freq_acc
Plain-language statement
If the intersection automaton sees the accepting conditions of both component automata infinitely many times, then its own accepting condition also happens infinitely many times.
Source project: Lean Computer Science Library
Person-level attribution pending.
Project index
Showing 8 of 130 additional declarations. Use project search for the complete index.
Cslib.Automata.NA.Buchi.inter_language_eq
Plain-language statement
The language accepted by the intersection automaton is the intersection of the languages accepted by the two component automata.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.Buchi.language_eq_fin_iSup_hmul_omegaPow
Plain-language statement
The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages of the form L * M^ω, where all Ls and Ms are regular languages.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.concat_run_exists
Plain-language statement
Given an accepting finite run of na1 and a run of na2, there exists a run of concat na1 na2 that is the concatenation of the two runs.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.concat_run_proj
Plain-language statement
A run of concat na1 na2 containing at least one na2 state is the concatenation of an accepting finite run of na1 followed by a run of na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.FinAcc.finConcat_language_eq
Plain-language statement
finConcat na1 na2 accepts the concatenation of the languages of na1 and na2.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.FinAcc.loop_language_eq
Plain-language statement
finLoop na accepts the Kleene star of the language of na, assuming that the latter is nonempty.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.iProd_run_iff
Plain-language statement
Every run of the product automaton projects onto runs of its component automata, and vice versa.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Automata.NA.iSum_run_iff
Plain-language statement
An infinite run of the sum automaton is an infinite run of one of its component automata.
Source project: Lean Computer Science Library
Person-level attribution pending.