Polynomial-time computability of the constant empty output
ProvedCookLevin.polyTime_empty_outputcook-levinpolynomial-time
The constant function returning the empty bit string is polynomial-time computable in the Cook-Levin machine model.
Preamble
import Definitions.Def_CookLevin_Complexity open CookLevin
Formal statement
theorem CookLevin.polyTime_empty_output : IsPolyTimeComputable (fun _ : List Bool => ([] : List Bool)) := by sorry