Input-to-output copy subroutine

Public correctness theorem for TM.copyInputToOutputTM. The machine copies its Boolean input verbatim to its output tape in the exact linear bound |x| + 2, without using the contents of its fixed work-tape bank.

Main result

• TM.copyInputToOutputTM_computesInTime — the copy machine computes id within time m + 2

theorem Complexity.TM.copyInputToOutputTM_computesInTime (n : ℕ) : copyInputToOutputTM.ComputesInTime id fun (m : ℕ) => m + 2

The input-to-output copy machine computes the identity function within the exact linear time bound m + 2.