Documentation

Cslib.Computability.Automata.NA.BuchiEquiv

Equivalence of nondeterministic Buchi automata (NBAs). #

source
🔸 coverage
def Cslib.Automata.NA.Buchi.reindex {Symbol : Type u} {State : Type v} {State' : Type w} (f : State ≃ State') :
Buchi State Symbol ≃ Buchi State' Symbol

Lifts an equivalence on states to an equivalence on NBAs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    📐 coverage
    theorem Cslib.Automata.NA.Buchi.reindex_run_iff {Symbol : Type u} {State : Type v} {State' : Type w} {f : State ≃ State'} {nba : Buchi State Symbol} {xs : ωSequence Symbol} {ss' : ωSequence State'} :
    ((reindex f) nba).Run xs ss' ↔ nba.Run xs (ωSequence.map (⇑f.symm) ss')
    source
    📐 coverage
    @[simp]
    theorem Cslib.Automata.NA.Buchi.reindex_run_iff' {Symbol : Type u} {State : Type v} {State' : Type w} {f : State ≃ State'} {nba : Buchi State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
    ((reindex f) nba).Run xs (ωSequence.map (⇑f) ss) ↔ nba.Run xs ss
    source
    📐 coverage
    @[simp]
    theorem Cslib.Automata.NA.Buchi.reindex_language_eq {Symbol : Type u} {State : Type v} {State' : Type w} {f : State ≃ State'} {nba : Buchi State Symbol} :
    ωAcceptor.language ((reindex f) nba) = ωAcceptor.language nba