Standalone Lean project
A reusable Lean library for automata, languages, and related computer-science proofs.
Flagship declarations
acc_lang_congr
Plain-language statement
The language accepted by c.toDA with a unique accepting state s is exactly the equivalence class of s.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_concat_e
Plain-language statement
The language of the concatenation NA that is accepted by M0's accepting states is the language accepted by M0.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_concat_ne
Plain-language statement
The language of the concatenation NA that is accepted by M1's accepting states is the language accepted by M0 concatenated with the language accepted by M1 minus the empty word.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_inter
Plain-language statement
The language accepted by the product NA is the intersection of the languages accepted by the component automata.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_loop
Plain-language statement
The language accepted by the loop NA is the Kleene star of the language accepted by M.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_loop_concat
Plain-language statement
The concatenation of the language accepted by the loop NA with itself is a subset of itself.
Source project: Automata Theory
Person-level attribution pending.
Project index
Showing 8 of 57 additional declarations. Use project search for the complete index.
Automata.acc_lang_pset
Plain-language statement
The language accepted by M.Pset is the same as that accepted by M, where the accepting states of M.Pset are those that contains at least one accepting state of M.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_lang_union
Plain-language statement
The language accepted by the sum NA is the union of the languages accepted by the component automata.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_concat
Plain-language statement
The ω-language of the concatenation NA that is accepted by M1's accepting states is the language accepted by M0 concatenated with the ω-language accepted by M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_inter2
Plain-language statement
The ω-language accepted by the OI2 NA is the intersection of the ω-languages accepted by M0 and M1.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_loop
Plain-language statement
The ω-language accepted by the loop NA is the ω-power of the language accepted by M.
Source project: Automata Theory
Person-level attribution pending.
Automata.acc_omega_lang_union
Plain-language statement
The ω-language accepted by the sum NA is the union of the ω-languages accepted by the component automata.
Source project: Automata Theory
Person-level attribution pending.
Automata.buchi_congr_ample
Project documentation
The BuchiCongr of an NA is ample if the NA is finite-state. For simplicity, this result is proved using a Ramsey theorem on infinite graphs.
Source project: Automata Theory
Person-level attribution pending.
Automata.buchi_congr_saturates
Plain-language statement
The BuchiCongr of an NA saturates the ω-language accepted by the NA. Note that this result does not need to assume that the NA is finite-state.
Source project: Automata Theory
Person-level attribution pending.