CookLevin.reductionEmitM_exists_core_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_exists_core_reduction_child (Mv : Machine) (k G : Nat) :
    ∃ M : Machine, TuringMachine k G M := by sorry