CookLevin.transitionClauseEmitter_polyTime_core_reduction_child

import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.transitionClauseEmitter_polyTime_core_reduction_child (Mv : Machine) (k G cw dw ct dt : Nat)
    (hwf : TuringMachine k G Mv) :
    IsPolyTimeComputable (fun x =>
      encodeFormula (transitionClauses
        ⟨k, G, Mv.length, tabWidth cw dw ct dt x⟩ Mv)) := by sorry