Complete decoded output from a marked-input machine

After marked input copying, the existing source simulation and output emitter run without modification. Input preparation and output emission have linear cost, and every source transition takes one target transition.

theorem Complexity.MathlibTM0.MarkedMachine.computes_proof (M : MarkedMachine) {input output : List Bool} {time : ℕ} (h : M.OutputsWithin input output time) : M.machine.ComputesInTimeAndSpace input output (2 * input.length + time + output.length + 4) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg input) (2 * input.length + time + output.length + 4))