Skip to content

Sequential transducers, Mealy and Moore machines

50 fully proved

Automata

StructureSequential transducer#✓fully proved

A sequential transducer with states in a type \(Q\), input letters in a type \(\Sigma\) and output letters in a type \(\Gamma\) consists of a transition function assigning to each state \(q \in Q\) and input letter \(a \in \Sigma\) a successor state in \(Q\) and an output word over \(\Gamma\), a start state in \(Q\), a set of accepting states \(F \subseteq Q\), an initial output word over \(\Gamma\), and, for each state in \(Q\), a final output word over \(\Gamma\).

No finiteness is assumed of \(Q\), \(\Sigma\) or \(\Gamma\).

structure SequentialTransducer (State In Out : Type*) where
  /-- On input letter `a` in state `q`, the successor state and the emitted output word. -/
  step : State → In → State × List Out
  /-- The start state. -/
  start : State
  /-- The set of accepting states. -/
  accept : Set State
  /-- The output word emitted before any input is read. -/
  initOut : List Out
  /-- The output word emitted on acceptance, depending on the final state. -/
  finalOut : State → List Out
Used by 35
Used byComposition of sequential transducers · Total output of a composite sequential transducer · Output of a composite sequential transducer · Output of the second transducer on the first one's whole output · States reached by a composite sequential transducer · State of the second transducer after the first one's whole output · One step of a composite transducer: the successor state · One step of a composite transducer: the output · Inverse sequential transduction preserves regular languages · Preimage of a language under a sequential transducer · Product DFA of a sequential transducer and a DFA · The product DFA recognizes the preimage · Runs of the product DFA · Run of a sequential transducer · Output word of a sequential transducer run · Output of a sequential transducer on a concatenation · Output of a sequential transducer on a nonempty word · Moore machine output via its sequential rendering · Final state of a sequential transducer run · Final state of a sequential transducer on a concatenation · Final state of a sequential transducer run on a nonempty word · The sequential transducer of a Mealy machine has the same run outputs · The sequential transducer of a Mealy machine has the same final states · Mealy machine as a sequential transducer · The sequential transducer of a Moore machine · Every state of the sequential transducer of a Mealy machine is accepting · Every state of the sequential transducer of a Moore machine is accepting · Final outputs of the sequential transducer of a Mealy machine · Final outputs of the sequential transducer of a Moore machine · Initial output of the sequential transducer of a Mealy machine · Initial output of the sequential transducer of a Moore machine · Translation by a sequential transducer · Translations of a composite sequential transducer · The sequential transducer of a Mealy machine computes its transduction · The sequential transducer of a Moore machine computes its transduction

Sequential Transducer

DefinitionRun of a sequential transducer#✓fully proved

The run of a sequential transducer \(S\) from a state \(q\) on an input word \(a_1 \cdots a_n\) is the pair \((q_n, w_1 w_2 \cdots w_n)\), where \(q_0 = q\) and, for each \(1 \le i \le n\), \(S\) moves from \(q_{i-1}\) on \(a_i\) to \(q_i\) emitting the word \(w_i\). The initial output and the final outputs of \(S\) are not included.

def runFrom (S : SequentialTransducer State In Out) (q : State) : List In → State × List Out
  | [] => (q, [])
  | a :: xs =>
      let (q', w) := S.step q a
      let (q'', w') := S.runFrom q' xs
      (q'', w ++ w')
Uses 1 · Used by 3
Statement usesSequential transducer
Used byComposition of sequential transducers · Output word of a sequential transducer run · Final state of a sequential transducer run

DefinitionFinal state of a sequential transducer run#✓fully proved

For a sequential transducer \(S\), a state \(q\) and an input word \(w\), the final state of the run of \(S\) from \(q\) on \(w\) is obtained by starting in \(q\), reading the letters of \(w\) in order, moving at each letter to the successor state given by the transition function of \(S\), and taking the state reached at the end.

def runState (S : SequentialTransducer State In Out) (q : State) (xs : List In) : State :=
  (S.runFrom q xs).1
Uses 2 · Used by 17
Statement usesSequential transducer · Run of a sequential transducer
Used byComposition of sequential transducers · Total output of a composite sequential transducer · Output of a composite sequential transducer · Output of the second transducer on the first one's whole output · States reached by a composite sequential transducer · State of the second transducer after the first one's whole output · One step of a composite transducer: the successor state · The product DFA recognizes the preimage · Runs of the product DFA · Output of a sequential transducer on a concatenation · Final state of a sequential transducer on a concatenation · Final state of a sequential transducer run on a nonempty word · The sequential transducer of a Mealy machine has the same final states · Translation by a sequential transducer · Translations of a composite sequential transducer · The sequential transducer of a Mealy machine computes its transduction · The sequential transducer of a Moore machine computes its transduction

DefinitionOutput word of a sequential transducer run#✓fully proved

For a sequential transducer \(S\), a state \(q\) and an input word \(x\), the output word of the run from \(q\) on \(x\) is the concatenation of the output words that \(S\) emits on the successive letters of \(x\), starting in \(q\) and moving to the successor state after each letter; the initial and final outputs are not included.

def runOut (S : SequentialTransducer State In Out) (q : State) (xs : List In) : List Out :=
  (S.runFrom q xs).2
Uses 2 · Used by 17
Statement usesSequential transducer · Run of a sequential transducer
Used byComposition of sequential transducers · Total output of a composite sequential transducer · Output of a composite sequential transducer · Output of the second transducer on the first one's whole output · States reached by a composite sequential transducer · State of the second transducer after the first one's whole output · One step of a composite transducer: the output · The product DFA recognizes the preimage · Runs of the product DFA · Output of a sequential transducer on a concatenation · Output of a sequential transducer on a nonempty word · Moore machine output via its sequential rendering · The sequential transducer of a Mealy machine has the same run outputs · Translation by a sequential transducer · Translations of a composite sequential transducer · The sequential transducer of a Mealy machine computes its transduction · The sequential transducer of a Moore machine computes its transduction

TheoremFinal state of a sequential transducer run on a nonempty word#✓fully proved

Let \(S\) be a sequential transducer, \(q\) a state, \(a\) an input letter and \(w\) an input word, and let \(q'\) be the successor state of \(q\) on \(a\) under the transition function of \(S\). Then the final state of the run of \(S\) from \(q\) on the word \(aw\) equals the final state of the run of \(S\) from \(q'\) on \(w\).

theorem runState_cons (S : SequentialTransducer State In Out) (q : State) (a : In)
    (xs : List In) :
    S.runState q (a :: xs) = S.runState (S.step q a).1 xs
Uses 2 · Used by 3
Statement usesSequential transducer · Final state of a sequential transducer run
Used byStates reached by a composite sequential transducer · Runs of the product DFA · The sequential transducer of a Mealy machine has the same final states

TheoremOutput of a sequential transducer on a nonempty word#✓fully proved

Let \(S\) be a sequential transducer, \(q\) a state, \(a\) an input letter and \(x\) an input word, and let \(q'\) and \(w\) be the successor state and the output word of \(S\) in state \(q\) on letter \(a\). The output word of the run of \(S\) from \(q\) on \(ax\) is \(w\) followed by the output word of the run from \(q'\) on \(x\).

theorem runOut_cons (S : SequentialTransducer State In Out) (q : State) (a : In)
    (xs : List In) :
    S.runOut q (a :: xs) = (S.step q a).2 ++ S.runOut (S.step q a).1 xs
Uses 2 · Used by 5
Statement usesSequential transducer · Output word of a sequential transducer run
Used byOutput of a composite sequential transducer · States reached by a composite sequential transducer · Runs of the product DFA · Moore machine output via its sequential rendering · The sequential transducer of a Mealy machine has the same run outputs

TheoremFinal state of a sequential transducer on a concatenation#✓fully proved

For a sequential transducer \(S\), a state \(q\) and input words \(x\) and \(y\), the final state of the run of \(S\) from \(q\) on \(xy\) is the final state of the run on \(y\) from the final state of the run from \(q\) on \(x\).

theorem runState_append (S : SequentialTransducer State In Out) (xs ys : List In)
    (q : State) :
    S.runState q (xs ++ ys) = S.runState (S.runState q xs) ys
Uses 2 · Used by 2
Statement usesSequential transducer · Final state of a sequential transducer run
Used byStates reached by a composite sequential transducer · State of the second transducer after the first one's whole output

TheoremOutput of a sequential transducer on a concatenation#✓fully proved

For a sequential transducer \(S\), a state \(q\) and input words \(x\) and \(y\), the output word of the run of \(S\) from \(q\) on \(xy\) is the output word of the run from \(q\) on \(x\) followed by the output word of the run on \(y\) from the final state of the run from \(q\) on \(x\).

theorem runOut_append (S : SequentialTransducer State In Out) (xs ys : List In)
    (q : State) :
    S.runOut q (xs ++ ys) =
      S.runOut q xs ++ S.runOut (S.runState q xs) ys
Uses 3 · Used by 2
Statement usesSequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run
Used byOutput of a composite sequential transducer · Output of the second transducer on the first one's whole output

DefinitionTranslation by a sequential transducer#✓fully proved

A sequential transducer \(S\) translates an input word \(x\) to an output word \(y\) when the run of \(S\) on \(x\) from its start state ends in an accepting state \(q\) and \(y\) is the concatenation of the initial output of \(S\), the output words emitted by the transitions along the run, and the final output of \(S\) at \(q\).

def Translates (S : SequentialTransducer State In Out) (xs : List In)
    (ys : List Out) : Prop :=
  S.runState S.start xs ∈ S.accept ∧
    S.initOut ++ S.runOut S.start xs ++ S.finalOut (S.runState S.start xs) = ys
Uses 3 · Used by 5
Statement usesSequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run
Used byPreimage of a language under a sequential transducer · The product DFA recognizes the preimage · Translations of a composite sequential transducer · The sequential transducer of a Mealy machine computes its transduction · The sequential transducer of a Moore machine computes its transduction

DefinitionComposition of sequential transducers#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\) with start state \(s_1\), initial output \(\iota_1\) and final output map \(\phi_1\), and let \(S_2\) be one from \(M\) to \(O\) with start state \(s_2\), initial output \(\iota_2\) and final output map \(\phi_2\). For a transducer \(S\), a state \(q\) and a word \(w\), write \(\delta_S(q, w)\) for the state \(S\) reaches by reading \(w\) from \(q\) and \(\lambda_S(q, w)\) for the concatenation of the words it emits along the way. The composition of \(S_1\) and \(S_2\) is the sequential transducer from \(I\) to \(O\) whose states are the pairs \((q_1, q_2)\) of a state of \(S_1\) and a state of \(S_2\), where: reading a letter \(a\) in state \((q_1, q_2)\), if \(S_1\) reading \(a\) in \(q_1\) moves to \(q_1'\) and emits \(w\), the composition moves to \((q_1', \delta_{S_2}(q_2, w))\) and emits \(\lambda_{S_2}(q_2, w)\); the start state is \((s_1, \delta_{S_2}(s_2, \iota_1))\); the initial output is \(\iota_2\) followed by \(\lambda_{S_2}(s_2, \iota_1)\); a state \((q_1, q_2)\) is accepting when \(q_1\) is accepting for \(S_1\) and \(\delta_{S_2}(q_2, \phi_1(q_1))\) is accepting for \(S_2\); and the final output at \((q_1, q_2)\) is \(\lambda_{S_2}(q_2, \phi_1(q_1))\) followed by \(\phi_2(\delta_{S_2}(q_2, \phi_1(q_1)))\).

In words: run \(S_1\) and feed its output, including its initial output (fed through \(S_2\) before any input is read) and its final output, through \(S_2\).

def comp (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) :
    SequentialTransducer (State₁ × State₂) In Out where
  step := fun (q₁, q₂) a =>
    let (q₁', w₁) := S₁.step q₁ a
    let (q₂', w₂) := S₂.runFrom q₂ w₁
    ((q₁', q₂'), w₂)
  start := (S₁.start, S₂.runState S₂.start S₁.initOut)
  accept := {p : State₁ × State₂ | p.1 ∈ S₁.accept ∧
    S₂.runState p.2 (S₁.finalOut p.1) ∈ S₂.accept}
  initOut := S₂.initOut ++ S₂.runOut S₂.start S₁.initOut
  finalOut := fun (q₁, q₂) =>
    S₂.runOut q₂ (S₁.finalOut q₁) ++ S₂.finalOut (S₂.runState q₂ (S₁.finalOut q₁))
Uses 4 · Used by 6
Statement usesSequential transducer · Run of a sequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run
Used byTotal output of a composite sequential transducer · Output of a composite sequential transducer · States reached by a composite sequential transducer · One step of a composite transducer: the successor state · One step of a composite transducer: the output · Translations of a composite sequential transducer

TheoremOne step of a composite transducer: the successor state#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\), \(S_2\) one from \(M\) to \(O\), and \(C\) their composition. Let \(q_1\) be a state of \(S_1\), \(q_2\) a state of \(S_2\) and \(a \in I\) a letter, and suppose that \(S_1\), reading \(a\) in state \(q_1\), moves to \(q_1'\) and emits the word \(w\). Then \(C\), reading \(a\) in state \((q_1, q_2)\), moves to \((q_1', q_2')\), where \(q_2'\) is the state \(S_2\) reaches by reading \(w\) from \(q_2\).

theorem comp_step_fst (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (q₁ : State₁) (q₂ : State₂)
    (a : In) :
    ((comp S₁ S₂).step (q₁, q₂) a).1 =
      ((S₁.step q₁ a).1, S₂.runState q₂ (S₁.step q₁ a).2)
Uses 3 · Used by 2
Statement usesSequential transducer · Composition of sequential transducers · Final state of a sequential transducer run
Used byOutput of a composite sequential transducer · States reached by a composite sequential transducer

TheoremOne step of a composite transducer: the output#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\), \(S_2\) one from \(M\) to \(O\), and \(C\) their composition. Let \(q_1\) be a state of \(S_1\), \(q_2\) a state of \(S_2\) and \(a \in I\) a letter, and let \(w\) be the word \(S_1\) emits when it reads \(a\) in state \(q_1\). Then the word \(C\) emits when it reads \(a\) in state \((q_1, q_2)\) is the concatenation of the words \(S_2\) emits while reading \(w\) from \(q_2\).

theorem comp_step_snd (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (q₁ : State₁) (q₂ : State₂)
    (a : In) :
    ((comp S₁ S₂).step (q₁, q₂) a).2 = S₂.runOut q₂ (S₁.step q₁ a).2
Uses 3 · Used by 1
Statement usesSequential transducer · Composition of sequential transducers · Output word of a sequential transducer run
Used byOutput of a composite sequential transducer

TheoremStates reached by a composite sequential transducer#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\), \(S_2\) one from \(M\) to \(O\), and \(C\) their composition. For a transducer \(S\), a state \(q\) and a word \(w\), write \(\delta_S(q, w)\) for the state \(S\) reaches by reading \(w\) from \(q\) and \(\lambda_S(q, w)\) for the concatenation of the words it emits along the way (without initial or final output). Then for all states \(q_1\) of \(S_1\) and \(q_2\) of \(S_2\) and every word \(x\) over \(I\), \(\delta_C((q_1, q_2), x) = (\delta_{S_1}(q_1, x), \delta_{S_2}(q_2, \lambda_{S_1}(q_1, x)))\).

theorem comp_runState (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) (q₁ : State₁)
    (q₂ : State₂) :
    (comp S₁ S₂).runState (q₁, q₂) xs =
      (S₁.runState q₁ xs, S₂.runState q₂ (S₁.runOut q₁ xs))
Uses 8 · Used by 2
Statement usesSequential transducer · Composition of sequential transducers · Output word of a sequential transducer run · Final state of a sequential transducer run
Proof usesOne step of a composite transducer: the successor state · Output of a sequential transducer on a nonempty word · Final state of a sequential transducer on a concatenation · Final state of a sequential transducer run on a nonempty word
Used byTotal output of a composite sequential transducer · Translations of a composite sequential transducer

TheoremOutput of a composite sequential transducer#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\), \(S_2\) one from \(M\) to \(O\), and \(C\) their composition. For a transducer \(S\), a state \(q\) and a word \(w\), write \(\lambda_S(q, w)\) for the concatenation of the words \(S\) emits while reading \(w\) from \(q\) (without initial or final output). Then for all states \(q_1\) of \(S_1\) and \(q_2\) of \(S_2\) and every word \(x\) over \(I\), \(\lambda_C((q_1, q_2), x) = \lambda_{S_2}(q_2, \lambda_{S_1}(q_1, x))\).

theorem comp_runOut (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) (q₁ : State₁)
    (q₂ : State₂) :
    (comp S₁ S₂).runOut (q₁, q₂) xs = S₂.runOut q₂ (S₁.runOut q₁ xs)
Uses 8 · Used by 1
Statement usesSequential transducer · Composition of sequential transducers · Output word of a sequential transducer run
Proof usesOne step of a composite transducer: the successor state · One step of a composite transducer: the output · Output of a sequential transducer on a concatenation · Output of a sequential transducer on a nonempty word · Final state of a sequential transducer run
Used byTotal output of a composite sequential transducer

TheoremState of the second transducer after the first one's whole output#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\) and \(S_2\) one from \(M\) to \(O\), with start states \(s_1\) and \(s_2\). For a transducer \(S\), a state \(q\) and a word \(w\), write \(\delta_S(q, w)\) for the state \(S\) reaches by reading \(w\) from \(q\) and \(\lambda_S(q, w)\) for the concatenation of the words it emits along the way (without initial or final output); juxtaposition of words is concatenation. For a word \(x\) over \(I\), let \(\iota\) be the initial output of \(S_1\), let \(u = \lambda_{S_1}(s_1, x)\), and let \(f\) be the final output of \(S_1\) at \(\delta_{S_1}(s_1, x)\). Then \(\delta_{S_2}(s_2, \iota u f) = \delta_{S_2}(\delta_{S_2}(\delta_{S_2}(s_2, \iota), u), f)\).

theorem comp_runState_initOut (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) :
    S₂.runState S₂.start
        (S₁.initOut ++ S₁.runOut S₁.start xs ++
          S₁.finalOut (S₁.runState S₁.start xs)) =
      S₂.runState (S₂.runState (S₂.runState S₂.start S₁.initOut)
        (S₁.runOut S₁.start xs)) (S₁.finalOut (S₁.runState S₁.start xs))
Uses 4 · Used by 2
Statement usesSequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run
Proof usesFinal state of a sequential transducer on a concatenation
Used byTotal output of a composite sequential transducer · Translations of a composite sequential transducer

TheoremOutput of the second transducer on the first one's whole output#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\) and \(S_2\) one from \(M\) to \(O\), with start states \(s_1\) and \(s_2\). For a transducer \(S\), a state \(q\) and a word \(w\), write \(\delta_S(q, w)\) for the state \(S\) reaches by reading \(w\) from \(q\) and \(\lambda_S(q, w)\) for the concatenation of the words it emits along the way (without initial or final output); juxtaposition of words is concatenation. For a word \(x\) over \(I\), let \(\iota\) be the initial output of \(S_1\), let \(u = \lambda_{S_1}(s_1, x)\), let \(f\) be the final output of \(S_1\) at \(\delta_{S_1}(s_1, x)\), and let \(r = \delta_{S_2}(s_2, \iota)\). Then \(\lambda_{S_2}(s_2, \iota u f) = \lambda_{S_2}(s_2, \iota) \, \lambda_{S_2}(r, u) \, \lambda_{S_2}(\delta_{S_2}(r, u), f)\).

theorem comp_runOut_initOut (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) :
    S₂.runOut S₂.start
        (S₁.initOut ++ S₁.runOut S₁.start xs ++
          S₁.finalOut (S₁.runState S₁.start xs)) =
      S₂.runOut S₂.start S₁.initOut ++
        S₂.runOut (S₂.runState S₂.start S₁.initOut) (S₁.runOut S₁.start xs) ++
          S₂.runOut (S₂.runState (S₂.runState S₂.start S₁.initOut)
            (S₁.runOut S₁.start xs)) (S₁.finalOut (S₁.runState S₁.start xs))
Uses 4 · Used by 1
Statement usesSequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run
Proof usesOutput of a sequential transducer on a concatenation
Used byTotal output of a composite sequential transducer

TheoremTotal output of a composite sequential transducer#✓fully proved

Let \(S_1\) be a sequential transducer from \(I\) to \(M\), \(S_2\) one from \(M\) to \(O\), and \(C\) their composition. For a sequential transducer \(S\) with start state \(s\), initial output \(\iota\) and final output map \(\phi\), and a word \(x\), let \(\delta_S(s, x)\) be the state \(S\) reaches by reading \(x\) from \(s\) and \(\lambda_S(s, x)\) the concatenation of the words it emits along the way, and call the concatenation \(\iota \, \lambda_S(s, x) \, \phi(\delta_S(s, x))\) the whole output of \(S\) on \(x\) (acceptance plays no role). Then for every word \(x\) over \(I\), the whole output of \(C\) on \(x\) equals the whole output of \(S_2\) on the whole output of \(S_1\) on \(x\).

theorem comp_output_eq (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) :
    (comp S₁ S₂).initOut ++ (comp S₁ S₂).runOut (comp S₁ S₂).start xs ++
        (comp S₁ S₂).finalOut ((comp S₁ S₂).runState (comp S₁ S₂).start xs) =
      S₂.initOut ++ S₂.runOut S₂.start
        (S₁.initOut ++ S₁.runOut S₁.start xs ++
          S₁.finalOut (S₁.runState S₁.start xs)) ++
        S₂.finalOut (S₂.runState S₂.start
          (S₁.initOut ++ S₁.runOut S₁.start xs ++
            S₁.finalOut (S₁.runState S₁.start xs)))
Uses 8 · Used by 1
Statement usesSequential transducer · Composition of sequential transducers · Output word of a sequential transducer run · Final state of a sequential transducer run
Proof usesOutput of a composite sequential transducer · Output of the second transducer on the first one's whole output · States reached by a composite sequential transducer · State of the second transducer after the first one's whole output
Used byTranslations of a composite sequential transducer

TheoremTranslations of a composite sequential transducer#✓fully proved

Let \(S_1\) be a sequential transducer from an alphabet \(A\) to an alphabet \(B\), and \(S_2\) one from \(B\) to an alphabet \(C\). For every word \(x\) over \(A\) and every word \(y\) over \(C\), the composition of \(S_1\) and \(S_2\) translates \(x\) to \(y\) if and only if there is a word \(z\) over \(B\) such that \(S_1\) translates \(x\) to \(z\) and \(S_2\) translates \(z\) to \(y\).

theorem translates_comp_iff (S₁ : SequentialTransducer State₁ In Mid)
    (S₂ : SequentialTransducer State₂ Mid Out) (xs : List In) (ys : List Out) :
    (comp S₁ S₂).Translates xs ys ↔
      ∃ zs, S₁.Translates xs zs ∧ S₂.Translates zs ys
Uses 8
Statement usesSequential transducer · Translation by a sequential transducer · Composition of sequential transducers
Proof usesTotal output of a composite sequential transducer · States reached by a composite sequential transducer · State of the second transducer after the first one's whole output · Output word of a sequential transducer run · Final state of a sequential transducer run

DefinitionPreimage of a language under a sequential transducer#✓fully proved

Let \(S\) be a sequential transducer with input alphabet \(\Sigma\) and output alphabet \(\Gamma\), and let \(L\) be a language over \(\Gamma\). The preimage of \(L\) under \(S\) is the language over \(\Sigma\) consisting of the words \(x\) for which there is a word \(y \in L\) such that \(S\) translates \(x\) to \(y\).

def preimage (S : SequentialTransducer State In Out) (L : Language Out) : Language In :=
  {xs | ∃ ys ∈ L, S.Translates xs ys}
Uses 2 · Used by 2
Statement usesSequential transducer · Translation by a sequential transducer
Used byInverse sequential transduction preserves regular languages · The product DFA recognizes the preimage

DefinitionProduct DFA of a sequential transducer and a DFA#✓fully proved

Let \(S\) be a sequential transducer with state type \(Q\), input alphabet \(\Sigma\) and output alphabet \(\Gamma\), and let \(M\) be a DFA over \(\Gamma\) with state type \(P\). The product DFA of \(S\) and \(M\) is the DFA over \(\Sigma\) with state type \(Q \times P\) defined as follows. In state \((q, r)\) on a letter \(a\), if \(S\) moves from \(q\) to \(q'\) emitting the word \(w\), it moves to \((q', r')\), where \(r'\) is the state \(M\) reaches from \(r\) on \(w\). Its start state is \((q_0, r_0)\), where \(q_0\) is the start state of \(S\) and \(r_0\) is the state \(M\) reaches from its start state on the initial output of \(S\). A state \((q, r)\) is accepting when \(q\) is an accepting state of \(S\) and the state \(M\) reaches from \(r\) on the final output of \(S\) at \(q\) is an accepting state of \(M\).

def preimageDFA (S : SequentialTransducer State In Out) (M : DFA Out σ) :
    DFA In (State × σ) where
  step := fun (q, r) a =>
    let (q', w) := S.step q a
    (q', M.evalFrom r w)
  start := (S.start, M.evalFrom M.start S.initOut)
  accept := {p : State × σ | p.1 ∈ S.accept ∧
    M.evalFrom p.2 (S.finalOut p.1) ∈ M.accept}
Uses 1 · Used by 3
Statement usesSequential transducer
Used byInverse sequential transduction preserves regular languages · The product DFA recognizes the preimage · Runs of the product DFA

TheoremRuns of the product DFA#✓fully proved

Let \(S\) be a sequential transducer and \(M\) a DFA over the output alphabet of \(S\). For every input word \(x\), state \(q\) of \(S\) and state \(r\) of \(M\), the product DFA of \(S\) and \(M\), started in \((q, r)\) and run on \(x\), ends in the state \((q', r')\), where \(q'\) is the final state of the run of \(S\) from \(q\) on \(x\) and \(r'\) is the state that \(M\) reaches from \(r\) on the output word of that run.

theorem preimageDFA_evalFrom (S : SequentialTransducer State In Out) (M : DFA Out σ)
    (xs : List In) (q : State) (r : σ) :
    (S.preimageDFA M).evalFrom (q, r) xs =
      (S.runState q xs, M.evalFrom r (S.runOut q xs))
Uses 6 · Used by 1
Statement usesSequential transducer · Product DFA of a sequential transducer and a DFA · Output word of a sequential transducer run · Final state of a sequential transducer run
Proof usesOutput of a sequential transducer on a nonempty word · Final state of a sequential transducer run on a nonempty word
Used byThe product DFA recognizes the preimage

TheoremThe product DFA recognizes the preimage#✓fully proved

Let \(S\) be a sequential transducer with output alphabet \(\Gamma\) and let \(M\) be a DFA over \(\Gamma\). The language accepted by the product DFA of \(S\) and \(M\) equals the preimage under \(S\) of the language accepted by \(M\), that is, the set of input words that \(S\) translates to some word accepted by \(M\).

theorem preimageDFA_accepts (S : SequentialTransducer State In Out) (M : DFA Out σ) :
    (S.preimageDFA M).accepts = S.preimage (M.accepts)
Uses 7 · Used by 1
Statement usesSequential transducer · Preimage of a language under a sequential transducer · Product DFA of a sequential transducer and a DFA
Proof usesTranslation by a sequential transducer · Runs of the product DFA · Output word of a sequential transducer run · Final state of a sequential transducer run
Used byInverse sequential transduction preserves regular languages

TheoremInverse sequential transduction preserves regular languages#✓fully proved

Let \(S\) be a sequential transducer with finitely many states, input alphabet \(I\) and output alphabet \(O\), and let \(L\) be a regular language over \(O\). Then the preimage of \(L\) under \(S\), the set of words over \(I\) that \(S\) translates to some word of \(L\), is regular.

The proof is the product of \(S\) with a DFA for \(L\), started in the DFA state reached on the initial output of \(S\).

theorem isRegular_preimage [Finite State] (S : SequentialTransducer State In Out)
    {L : Language Out} (hL : L.IsRegular) : (S.preimage L).IsRegular
Uses 4
Statement usesSequential transducer · Preimage of a language under a sequential transducer
Proof usesProduct DFA of a sequential transducer and a DFA · The product DFA recognizes the preimage

Automata

StructureMealy machine#✓fully proved

A Mealy machine with state set \(Q\), input alphabet \(I\) and output alphabet \(O\) consists of a start state in \(Q\) and a transition function that, given a state \(q \in Q\) and an input letter \(a \in I\), returns a successor state in \(Q\) and a single output letter in \(O\); thus the output of a transition depends on the state and the input letter.

structure MealyMachine (State In Out : Type*) where
  /-- The transition function: successor state and output letter. -/
  step : State → In → State × Out
  /-- The start state. -/
  start : State
Used by 13
Used byRun of a Mealy machine · Output word of a Mealy machine run · Output of a Mealy machine on a nonempty word · Final state of a Mealy machine run · Final state of a Mealy machine on a nonempty word · The sequential transducer of a Mealy machine has the same run outputs · The sequential transducer of a Mealy machine has the same final states · Mealy machine as a sequential transducer · Every state of the sequential transducer of a Mealy machine is accepting · Final outputs of the sequential transducer of a Mealy machine · Initial output of the sequential transducer of a Mealy machine · Transduction of a Mealy machine · The sequential transducer of a Mealy machine computes its transduction

Mealy Machine

DefinitionRun of a Mealy machine#✓fully proved

The run of a Mealy machine \(M\) from a state \(q\) on an input word \(a_1 \cdots a_n\) is the pair \((q_n, o_1 \cdots o_n)\), where \(q_0 = q\) and, for each \(1 \le i \le n\), \(M\) moves from \(q_{i-1}\) on \(a_i\) to \(q_i\) emitting the output letter \(o_i\).

def runFrom (M : MealyMachine State In Out) (q : State) :
    List In → State × List Out
  | [] => (q, [])
  | a :: xs =>
      let (q', o) := M.step q a
      let (q'', w) := M.runFrom q' xs
      (q'', o :: w)
Uses 1 · Used by 3
Statement usesMealy machine
Used byOutput word of a Mealy machine run · Final state of a Mealy machine run · Transduction of a Mealy machine

DefinitionFinal state of a Mealy machine run#✓fully proved

For a Mealy machine \(M\), a state \(q\) and an input word \(x\), the final state of the run from \(q\) on \(x\) is the state reached by starting in \(q\) and moving, on each successive letter of \(x\), to the successor state given by the transition function of \(M\); on the empty word it is \(q\).

def runState (M : MealyMachine State In Out) (q : State) (xs : List In) : State :=
  (M.runFrom q xs).1
Uses 2 · Used by 2
Statement usesMealy machine · Run of a Mealy machine
Used byFinal state of a Mealy machine on a nonempty word · The sequential transducer of a Mealy machine has the same final states

DefinitionOutput word of a Mealy machine run#✓fully proved

For a Mealy machine \(M\), a state \(q\) and an input word \(x\), the output word of \(M\) from \(q\) on \(x\) is the second component of the run of \(M\) from \(q\) on \(x\): the word of output letters emitted along that run, one per input letter.

def runOut (M : MealyMachine State In Out) (q : State) (xs : List In) : List Out :=
  (M.runFrom q xs).2
Uses 2 · Used by 3
Statement usesMealy machine · Run of a Mealy machine
Used byOutput of a Mealy machine on a nonempty word · The sequential transducer of a Mealy machine has the same run outputs · The sequential transducer of a Mealy machine computes its transduction

TheoremFinal state of a Mealy machine on a nonempty word#✓fully proved

Let \(M\) be a Mealy machine, \(q\) a state, \(a\) an input letter and \(x\) an input word, and let \(q'\) be the successor state of \(M\) in state \(q\) on letter \(a\). The final state of the run of \(M\) from \(q\) on \(ax\) is the final state of the run from \(q'\) on \(x\).

theorem runState_cons (M : MealyMachine State In Out) (q : State) (a : In)
    (xs : List In) :
    M.runState q (a :: xs) = M.runState (M.step q a).1 xs
Uses 2 · Used by 1
Statement usesMealy machine · Final state of a Mealy machine run
Used byThe sequential transducer of a Mealy machine has the same final states

TheoremOutput of a Mealy machine on a nonempty word#✓fully proved

Let \(M\) be a Mealy machine, \(q\) a state, \(a\) an input letter and \(x\) an input word, and let \(q'\) and \(o\) be the successor state and the output letter of \(M\) in state \(q\) on letter \(a\). The output word of the run of \(M\) from \(q\) on \(ax\) is \(o\) followed by the output word of the run from \(q'\) on \(x\).

theorem runOut_cons (M : MealyMachine State In Out) (q : State) (a : In)
    (xs : List In) :
    M.runOut q (a :: xs) = (M.step q a).2 :: M.runOut (M.step q a).1 xs
Uses 2 · Used by 1
Statement usesMealy machine · Output word of a Mealy machine run
Used byThe sequential transducer of a Mealy machine has the same run outputs

DefinitionTransduction of a Mealy machine#✓fully proved

Let \(M\) be a Mealy machine with start state \(q_0\). On an input word \(a_1 a_2 \cdots a_n\), for each \(i\) let \(q_i\) and \(b_i\) be the state that \(M\) moves to and the letter that it outputs when it reads \(a_i\) in state \(q_{i-1}\). The transduction of \(M\) on this word is the output word \(b_1 b_2 \cdots b_n\).

def transduce (M : MealyMachine State In Out) (xs : List In) : List Out :=
  (M.runFrom M.start xs).2
Uses 2 · Used by 1
Statement usesMealy machine · Run of a Mealy machine
Used byThe sequential transducer of a Mealy machine computes its transduction

DefinitionMealy machine as a sequential transducer#✓fully proved

The sequential transducer of a Mealy machine \(M\) has the states and the start state of \(M\); on an input letter \(a\) in a state \(q\) it moves to the state that \(M\) moves to and emits the one-letter word consisting of the letter that \(M\) outputs on this transition. Every state accepts, and the initial and final outputs are empty.

def toSequential (M : MealyMachine State In Out) : SequentialTransducer State In Out where
  step q a := let (q', o) := M.step q a; (q', [o])
  start := M.start
  accept := Set.univ
  initOut := []
  finalOut := fun _ => []
Uses 2 · Used by 6
Statement usesMealy machine · Sequential transducer
Used byThe sequential transducer of a Mealy machine has the same run outputs · The sequential transducer of a Mealy machine has the same final states · Every state of the sequential transducer of a Mealy machine is accepting · Final outputs of the sequential transducer of a Mealy machine · Initial output of the sequential transducer of a Mealy machine · The sequential transducer of a Mealy machine computes its transduction

TheoremThe sequential transducer of a Mealy machine has the same final states#✓fully proved

For a Mealy machine \(M\), a state \(q\) and an input word \(w\), the final state of the run from \(q\) on \(w\) of the sequential transducer associated with \(M\) equals the final state of the run of \(M\) from \(q\) on \(w\).

theorem seq_runState_eq (M : MealyMachine State In Out) (xs : List In) (q : State) :
    (M.toSequential).runState q xs = M.runState q xs
Uses 7
Statement usesMealy machine · Final state of a Mealy machine run · Mealy machine as a sequential transducer · Final state of a sequential transducer run
Proof usesFinal state of a Mealy machine on a nonempty word · Sequential transducer · Final state of a sequential transducer run on a nonempty word

TheoremThe sequential transducer of a Mealy machine has the same run outputs#✓fully proved

For a Mealy machine \(M\), a state \(q\) and an input word \(w\), the output word of the run from \(q\) on \(w\) of the sequential transducer associated with \(M\) (excluding its initial and final outputs) equals the output word of the run of \(M\) from \(q\) on \(w\).

theorem seq_runOut_eq (M : MealyMachine State In Out) (xs : List In) (q : State) :
    (M.toSequential).runOut q xs = M.runOut q xs
Uses 7 · Used by 1
Statement usesMealy machine · Output word of a Mealy machine run · Mealy machine as a sequential transducer · Output word of a sequential transducer run
Proof usesOutput of a Mealy machine on a nonempty word · Sequential transducer · Output of a sequential transducer on a nonempty word
Used byThe sequential transducer of a Mealy machine computes its transduction

TheoremEvery state of the sequential transducer of a Mealy machine is accepting#✓fully proved

For a Mealy machine \(M\), the set of accepting states of the sequential transducer associated with \(M\) is the set of all states.

theorem toSequential_accept (M : MealyMachine State In Out) :
    (M.toSequential).accept = Set.univ
Uses 3 · Used by 1
Statement usesMealy machine · Mealy machine as a sequential transducer · Sequential transducer
Used byThe sequential transducer of a Mealy machine computes its transduction

TheoremInitial output of the sequential transducer of a Mealy machine#✓fully proved

For every Mealy machine \(M\), the initial output of the sequential transducer of \(M\) is the empty word.

theorem toSequential_initOut (M : MealyMachine State In Out) :
    (M.toSequential).initOut = []
Uses 3 · Used by 1
Statement usesMealy machine · Mealy machine as a sequential transducer · Sequential transducer
Used byThe sequential transducer of a Mealy machine computes its transduction

TheoremFinal outputs of the sequential transducer of a Mealy machine#✓fully proved

For every Mealy machine \(M\) and every state \(q\), the final output of the sequential transducer of \(M\) at \(q\) is the empty word.

theorem toSequential_finalOut (M : MealyMachine State In Out) (q : State) :
    (M.toSequential).finalOut q = []
Uses 3 · Used by 1
Statement usesMealy machine · Mealy machine as a sequential transducer · Sequential transducer
Used byThe sequential transducer of a Mealy machine computes its transduction

TheoremThe sequential transducer of a Mealy machine computes its transduction#✓fully proved

For every Mealy machine \(M\), input word \(x\) and output word \(y\), the sequential transducer of \(M\) translates \(x\) to \(y\) if and only if the transduction of \(M\) on \(x\) is \(y\).

theorem translates_toSequential_iff (M : MealyMachine State In Out) (xs : List In)
    (ys : List Out) :
    (M.toSequential).Translates xs ys ↔ M.transduce xs = ys
Uses 12
Statement usesMealy machine · Mealy machine as a sequential transducer · Transduction of a Mealy machine · Translation by a sequential transducer
Proof usesOutput word of a Mealy machine run · The sequential transducer of a Mealy machine has the same run outputs · Every state of the sequential transducer of a Mealy machine is accepting · Final outputs of the sequential transducer of a Mealy machine · Initial output of the sequential transducer of a Mealy machine · Sequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run

Automata

StructureMoore machine#✓fully proved

A Moore machine with state type \(Q\), input alphabet \(\Sigma\) and output alphabet \(\Gamma\) consists of a transition function, assigning to each state \(q\) and input letter \(a\) a successor state \(\delta(q, a) \in Q\), an output function \(\lambda : Q \to \Gamma\), and a start state \(q_0 \in Q\). The output depends only on the state.

structure MooreMachine (State In Out : Type*) where
  /-- The transition function: successor state on an input letter. -/
  step : State → In → State
  /-- The output of a state. -/
  out : State → Out
  /-- The start state. -/
  start : State
Used by 12
Used byRun of a Moore machine · Output word of a Moore machine run · Output of a Moore machine on a nonempty word · Moore machine output via its sequential rendering · Final state of a Moore machine run · Final state of a Moore machine run on a nonempty word · The sequential transducer of a Moore machine · Every state of the sequential transducer of a Moore machine is accepting · Final outputs of the sequential transducer of a Moore machine · Initial output of the sequential transducer of a Moore machine · Transduction of a Moore machine · The sequential transducer of a Moore machine computes its transduction

Moore Machine

DefinitionRun of a Moore machine#✓fully proved

The run of a Moore machine \(M\) with output function \(\lambda\) from a state \(q\) on an input word \(a_1 \cdots a_n\) is the pair \((q_n, \lambda(q_0) \lambda(q_1) \cdots \lambda(q_n))\), where \(q_0 = q\) and, for each \(1 \le i \le n\), \(q_i\) is the successor of \(q_{i-1}\) on \(a_i\). The output word has \(n + 1\) letters and begins with the output of the starting state.

def runFrom (M : MooreMachine State In Out) (q : State) :
    List In → State × List Out
  | [] => (q, [M.out q])
  | a :: xs =>
      let q' := M.step q a
      let (q'', w) := M.runFrom q' xs
      (q'', M.out q :: w)
Uses 1 · Used by 3
Statement usesMoore machine
Used byOutput word of a Moore machine run · Final state of a Moore machine run · Transduction of a Moore machine

DefinitionFinal state of a Moore machine run#✓fully proved

For a Moore machine \(M\), a state \(q\) and an input word \(x\), the final state of the run from \(q\) on \(x\) is the state reached by starting in \(q\) and moving, on each successive letter of \(x\), to the successor state given by the transition function of \(M\); on the empty word it is \(q\).

def runState (M : MooreMachine State In Out) (q : State) (xs : List In) : State :=
  (M.runFrom q xs).1
Uses 2 · Used by 1
Statement usesMoore machine · Run of a Moore machine
Used byFinal state of a Moore machine run on a nonempty word

DefinitionOutput word of a Moore machine run#✓fully proved

For a Moore machine \(M\), a state \(q\) and an input word \(x\), the output word of \(M\) from \(q\) on \(x\) is the second component of the run of \(M\) from \(q\) on \(x\): the outputs of the states visited along that run, starting with the output of \(q\); it has one more letter than \(x\).

def runOut (M : MooreMachine State In Out) (q : State) (xs : List In) : List Out :=
  (M.runFrom q xs).2
Uses 2 · Used by 2
Statement usesMoore machine · Run of a Moore machine
Used byOutput of a Moore machine on a nonempty word · Moore machine output via its sequential rendering

TheoremFinal state of a Moore machine run on a nonempty word#✓fully proved

For a Moore machine \(M\) with transition function \(\delta\), a state \(q\), an input letter \(a\) and an input word \(w\), the final state of the run of \(M\) from \(q\) on the word \(aw\) equals the final state of the run of \(M\) from \(\delta(q, a)\) on \(w\).

theorem runState_cons (M : MooreMachine State In Out) (q : State) (a : In)
    (xs : List In) :
    M.runState q (a :: xs) = M.runState (M.step q a) xs
Uses 2
Statement usesMoore machine · Final state of a Moore machine run

TheoremOutput of a Moore machine on a nonempty word#✓fully proved

Let \(M\) be a Moore machine, \(q\) a state, \(a\) an input letter and \(x\) an input word, and let \(q'\) be the successor state of \(M\) in state \(q\) on letter \(a\). The output word of the run of \(M\) from \(q\) on \(ax\) is the output of \(q\) followed by the output word of the run from \(q'\) on \(x\).

theorem runOut_cons (M : MooreMachine State In Out) (q : State) (a : In)
    (xs : List In) :
    M.runOut q (a :: xs) = M.out q :: M.runOut (M.step q a) xs
Uses 2 · Used by 1
Statement usesMoore machine · Output word of a Moore machine run
Used byMoore machine output via its sequential rendering

DefinitionTransduction of a Moore machine#✓fully proved

Let \(M\) be a Moore machine with start state \(q_0\), and write \(o(q)\) for the output of a state \(q\). On an input word \(a_1 a_2 \cdots a_n\), let \(q_i\) be the state that \(M\) moves to from \(q_{i-1}\) on \(a_i\). The transduction of \(M\) on this word is the output word \(o(q_0)\, o(q_1) \cdots o(q_n)\), of length \(n + 1\).

def transduce (M : MooreMachine State In Out) (xs : List In) : List Out :=
  (M.runFrom M.start xs).2
Uses 2 · Used by 1
Statement usesMoore machine · Run of a Moore machine
Used byThe sequential transducer of a Moore machine computes its transduction

DefinitionThe sequential transducer of a Moore machine#✓fully proved

Let \(M\) be a Moore machine with transition function \(\delta\), output function \(\lambda\) and start state \(q_0\). Its sequential transducer has the same states and the start state \(q_0\); reading a letter \(a\) in state \(q\) it moves to \(\delta(q, a)\) and emits the one-letter word \(\lambda(\delta(q, a))\); every state is accepting; the initial output is the one-letter word \(\lambda(q_0)\); and every final output is empty.

def toSequential (M : MooreMachine State In Out) : SequentialTransducer State In Out where
  step q a := (M.step q a, [M.out (M.step q a)])
  start := M.start
  accept := Set.univ
  initOut := [M.out M.start]
  finalOut := fun _ => []
Uses 2 · Used by 5
Statement usesMoore machine · Sequential transducer
Used byMoore machine output via its sequential rendering · Every state of the sequential transducer of a Moore machine is accepting · Final outputs of the sequential transducer of a Moore machine · Initial output of the sequential transducer of a Moore machine · The sequential transducer of a Moore machine computes its transduction

TheoremMoore machine output via its sequential rendering#✓fully proved

For a Moore machine \(M\), a state \(q\) and an input word \(x\), the output word of the run of \(M\) from \(q\) on \(x\) is the output of \(q\) followed by the output word of the run of the sequential rendering of \(M\) from \(q\) on \(x\).

theorem runOut_eq_cons (M : MooreMachine State In Out) (xs : List In) (q : State) :
    M.runOut q xs = M.out q :: (M.toSequential).runOut q xs
Uses 7 · Used by 1
Statement usesMoore machine · Output word of a Moore machine run · The sequential transducer of a Moore machine · Output word of a sequential transducer run
Proof usesOutput of a Moore machine on a nonempty word · Sequential transducer · Output of a sequential transducer on a nonempty word
Used byThe sequential transducer of a Moore machine computes its transduction

TheoremEvery state of the sequential transducer of a Moore machine is accepting#✓fully proved

For a Moore machine \(M\), the set of accepting states of the sequential transducer associated with \(M\) is the set of all states.

theorem toSequential_accept (M : MooreMachine State In Out) :
    (M.toSequential).accept = Set.univ
Uses 3 · Used by 1
Statement usesMoore machine · The sequential transducer of a Moore machine · Sequential transducer
Used byThe sequential transducer of a Moore machine computes its transduction

TheoremInitial output of the sequential transducer of a Moore machine#✓fully proved

For every Moore machine \(M\), the initial output of the sequential transducer of \(M\) is the one-letter word consisting of the output of the start state of \(M\).

theorem toSequential_initOut (M : MooreMachine State In Out) :
    (M.toSequential).initOut = [M.out M.start]
Uses 3 · Used by 1
Statement usesMoore machine · The sequential transducer of a Moore machine · Sequential transducer
Used byThe sequential transducer of a Moore machine computes its transduction

TheoremFinal outputs of the sequential transducer of a Moore machine#✓fully proved

For a Moore machine \(M\) and every state \(q\), the final output word at \(q\) of the sequential transducer associated with \(M\) is empty.

theorem toSequential_finalOut (M : MooreMachine State In Out) (q : State) :
    (M.toSequential).finalOut q = []
Uses 3 · Used by 1
Statement usesMoore machine · The sequential transducer of a Moore machine · Sequential transducer
Used byThe sequential transducer of a Moore machine computes its transduction

TheoremThe sequential transducer of a Moore machine computes its transduction#✓fully proved

For every Moore machine \(M\), input word \(x\) and output word \(y\), the sequential transducer of \(M\) translates \(x\) to \(y\) if and only if the transduction of \(M\) on \(x\) is \(y\).

theorem translates_toSequential_iff (M : MooreMachine State In Out) (xs : List In)
    (ys : List Out) :
    (M.toSequential).Translates xs ys ↔ M.transduce xs = ys
Uses 11
Statement usesMoore machine · The sequential transducer of a Moore machine · Transduction of a Moore machine · Translation by a sequential transducer
Proof usesMoore machine output via its sequential rendering · Every state of the sequential transducer of a Moore machine is accepting · Final outputs of the sequential transducer of a Moore machine · Initial output of the sequential transducer of a Moore machine · Sequential transducer · Output word of a sequential transducer run · Final state of a sequential transducer run

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.