CookLevin.reductionEmitM_computesInTime_core_machine_reduction_child

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction

open CookLevin

theorem CookLevin.reductionEmitM_computesInTime_core_machine_reduction_child (Mv : Machine) (k G cw dw ct dt : Nat)
    (hwf : TuringMachine k G Mv) :
    ∃ M, TuringMachine k G M ∧ ComputesInTime M k (polyBound (1 + cw + dw + ct + dt) 1) (cookLevinReduction Mv k G cw dw ct dt) := by sorry