Polynomial-time closure under dropping the final output bit
ProvedCookLevin.polyTime_dropLastcomplexitycook-levinturing-machines
If a bit-string function is computed by a polynomial-time multitape Turing machine, then the function obtained by deleting its final output bit is also polynomial-time computable. This isolates the output-trimming transducer used by polyTime_dropLast_append.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin
Formal statement
namespace CookLevin
/-- Polynomial-time computability is closed under removing the final output bit. -/
theorem polyTime_dropLast
(u : List Bool → List Bool)
(hu : IsPolyTimeComputable u) :
IsPolyTimeComputable (fun x => (u x).dropLast) := by sorry
end CookLevin
Source
Machine-construction decomposition of https://prove2.me/theorems/9dfa5b11-e968-4a25-995d-f22d77d35dbd under the CookLevinLean cost model: https://github.com/Rizvonium/cook_levin_lean_v1/blob/main/CookLevinLean/Complexity.lean