Documentation

Complexitylib.Models.FiniteAutomaton.Complementation.Internal.Bridge

Two-way complementation on the canonical automata model #

Translate the existing endmarker, movement, and state conventions into the source model without adding states. Swapping the configuration components identifies the step relations and finite runs, including zero-step acceptance.

source
def Complexity.FiniteAutomaton.Complementation.Internal.decodeSymbol {Alpha : Type} :
Fin 2 ⊕ Alpha → Symbol Alpha

Translate the two numbered endmarkers and ordinary letters.

Equations
Instances For
    source
    def Complexity.FiniteAutomaton.Complementation.Internal.decodeMove (m : Fin 3) :
    Move

    Translate source move codes zero, one, and two into left, stay, and right.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.FiniteAutomaton.Complementation.Internal.encodeMove :
      Move → Fin 3

      Encode left, stay, and right moves as zero, one, and two.

      Equations
      Instances For
        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.decode_encode_move (m : Move) :
        decodeMove (encodeMove m) = m
        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.decodeMove_rel (m : Fin 3) (i j : ℕ) :
        ↑j = ↑i + ↑↑m - 1 ↔ (decodeMove m).Rel i j
        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.decodeSymbol_tapeSymbol {Alpha : Type} (w : List Alpha) (p : Fin (w.length + 2)) :
        decodeSymbol (tapeSymbol w p) = scanned w p
        source
        def Complexity.FiniteAutomaton.Complementation.Internal.asSource {Alpha : Type} {s : ℕ} (M : NMachine Alpha s) :
        TwoNFA Alpha (Fin s)

        View a canonical nondeterministic automaton as a source automaton on the same states.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Complexity.FiniteAutomaton.Complementation.Internal.asSource_step {Alpha : Type} {s : ℕ} (M : NMachine Alpha s) (w : List Alpha) (c d : Fin s × Fin (w.length + 2)) :
          (c, d) ∈ (asSource M).step w ↔ M.Step w c.swap d.swap
          source
          theorem Complexity.FiniteAutomaton.Complementation.Internal.asSource_language {Alpha : Type} {s : ℕ} (M : NMachine Alpha s) (w : List Alpha) :
          w ∈ (asSource M).language ↔ M.Accepts false w