Pair a computed value with the original input

This module exposes a generic deterministic fanout combinator. If tmF computes f, then pairWithInputTM tmF computes x ↦ pair (f x) x while retaining a concrete polynomial-preserving time bound.

Main result

• TM.pairWithInputTM_computesInTime — computation paired with original input

theorem Complexity.TM.pairWithInputTM_computesInTime {nf : ℕ} {tmF : TM nf} {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : tmF.ComputesInTime f T) : tmF.pairWithInputTM.ComputesInTime (fun (x : List Bool) => pair (f x) x) (pairWithInputTime T)

Pairing a computed string with the unchanged original input costs at most five source-time budgets, one linear input scan, and constant seam overhead.