Polynomial-time machine for appending one fixed output bit

import Definitions.Def_CookLevin_Complexity
open CookLevin

namespace CookLevin

/-- A low-level output postprocessor: after a well-formed machine computes a
bit string within a polynomial bound, one may rewind/scan its output tape,
write one fixed bit at the first non-bit cell, and halt. The constants in the
new polynomial absorb the original run, rewind, scan, and final write. -/
theorem appendBit_machine
    (M : Machine) (k G c d : Nat) (u : List Bool → List Bool)
    (hwf : TuringMachine k G M)
    (hcomp : ComputesInTime M k (polyBound c d) u)
    (b : Bool) :
    ∃ (M' : Machine) (k' G' c' d' : Nat),
      TuringMachine k' G' M' ∧
      ComputesInTime M' k' (polyBound c' d') (fun x => u x ++ [b]) := by
  sorry

end CookLevin