Regular-domain TM2 computations #
Reverse the input DFA as well as the string representation, guard the marked simulator, and then use polynomial-time reversal to restore the original order. The source need only have a runtime bound on accepted strings.
theorem
Complexity.MathlibTM2.mem_FP_on_dfa_proof
{f : List Bool → List Bool}
(computer : Turing.TM2ComputableAux Bool Bool)
[(k : computer.tm.K) → Fintype (computer.tm.Γ k)]
{σ : Type}
[Fintype σ]
(D : DFA Bool σ)
[DecidablePred fun (x : List Bool) => x ∈ D.accepts]
{p : Polynomial ℕ}
(h :
(w : List Bool) →
w ∈ D.accepts →
Turing.TM2OutputsInTime computer.tm (List.map (⇑computer.inputAlphabet.symm) w)
(some (List.map (⇑computer.outputAlphabet.symm) (f w))) (Polynomial.eval w.length p))
: