Polynomial-time pairing with the original input

Main result

• mem_FP_pairWithInput — if f ∈ FP, then x ↦ pair (f x) x is in FP

theorem Complexity.mem_FP_pairWithInput {f : List Bool → List Bool} (hf : f ∈ FP) : (fun (x : List Bool) => pair (f x) x) ∈ FP

A polynomial-time function can be evaluated and paired with its unchanged original input in polynomial time.