Polynomial-time closure under appending one bit
ProvedCookLevin.polyTime_append_truecook-levinpolynomial-time
Appending a fixed final bit to the output of a polynomial-time computable bit-string function preserves polynomial-time computability.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin
Formal statement
theorem CookLevin.polyTime_append_true (u : List Bool → List Bool) (hu : IsPolyTimeComputable u) : IsPolyTimeComputable (fun x => u x ++ [true]) := by sorry