Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
Automata.da_concat_of_muller_accept
Plain-language statement
Any infinite word accepted by M1.Concat acc1 M2 under the Muller condition consists of a finite word accepted by M1 followed by an infinite word accepted by M2 under the Muller condition.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_ptr2_antitone
Plain-language statement
The value of DA.ConcatPtr2 is a non-increasing over time.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_ptr2_exists
Project documentation
The copy i of M2 being asserted to exist by this theorem is activated at step n and persists ever after. But i may not stay constant over time.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_to_muller_accept
Plain-language statement
Any infinite word consisting of a finite word accepted by M1 followed by an infinite word accepted by M2 under the Muller condition is accepted by M1.Concat acc1 M2 under the Muller condition
Source project: Automata Theory
Person-level attribution pending.
Automata.det_muller_accept_boolean_form
Plain-language statement
The ω-language accepted by a deterministic Muller automaton is a boolean combination of the ω-limits of accepted languages. Note that this result does not need to assume that the automaton is finite-state.
Source project: Automata Theory
Person-level attribution pending.
Automata.det_muller_accept_omega_limit
Plain-language statement
The ω-limit of the language accepted by a deterministic automaton is accepted by a deterministic Muller automaton.
Source project: Automata Theory
Person-level attribution pending.