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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersAutomata.da_concat_det_run_2
Plain-language statement
If any M2 copy in the second state component of M1.Concat acc1 M2 ever stabilizes (in the sense of never being deactivated from some point on), then it contains an infinite run of M2 starting from its activation.
Source project: Automata Theory
Person-level attribution pending.
Automata.da_concat_det_run_cnt2
Plain-language statement
The second state component of M1.Concat acc1 M2 always has at least one inactive copy of M2 available.
Source project: Automata Theory
Person-level attribution pending.
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.