Copying states of a finite-state transducer #
A state that emits each input symbol unchanged, stays in that state, and emits nothing at end of input copies every word. This rule applies to arbitrary alphabets and state types; it is shared by the binary predecessor and the unary-magnitude signed-integer transducers.
Main results #
Turing.MultiTapeTM.Transducer.run_eq_self: a copying state preserves the input word.
theorem Turing.MultiTapeTM.Transducer.run_eq_self {Symbol : Type u_1} {Q : Type u_2} (T : Transducer Symbol Q) (q : Q) (hstep : ∀ (a : Symbol), T.step q a = (q, [a])) (hfinal : T.final q = []) (w : List Symbol) :
A transducer started in a copying state preserves every word, provided that state emits nothing at the end of the input.