Deterministic preprocessing before a nondeterministic decider

NTM.compositionNTM_decidesInTime: if tmF computes f in time TF and N decides L within a monotone bound TG, then the composite decides the preimage f ⁻¹' L within 4·TF(n) + 11 + TG(TF(n)) — the same coarse pipeline bound as the deterministic composition, with the decider's budget evaluated at the output-length bound TF(n).

The hypothesis N.qstart ≠ N.qhalt excludes the degenerate machine that starts halted; such a machine accepts nothing, so a client can decide the preimage of its (empty) language without running the composite at all.

theorem Complexity.NTM.compositionNTM_decidesInTime {nf ng : ℕ} {tmF : TM nf} {N : NTM ng} {f : List Bool → List Bool} {L : Language} {TF TG : ℕ → ℕ} (hF : tmF.ComputesInTime f TF) (hN : N.DecidesInTime L TG) (hmono : Monotone TG) (hne : N.qstart ≠ N.qhalt) : (compositionNTM tmF N).DecidesInTime (f ⁻¹' L) fun (n : ℕ) => 4 * TF n + 11 + TG (TF n)

Preprocessing before a nondeterministic decider. The composite decides the preimage language within the composed budget.