CookLevin.structuralClauseEmitters_polyTime_core_reduction_child

import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.structuralClauseEmitters_polyTime_core_reduction_child (k G Q cw dw ct dt : Nat) :
    ∀ family ∈ ([cellClauses, headClauses, stateClauses, readClauses,
      linkClauses, inertiaClauses, haltClauses, acceptClauses,
      fun sh => blankSuffixClauses sh 1] : List (Shape → Formula)),
      IsPolyTimeComputable (fun x =>
        encodeFormula (family ⟨k, G, Q, tabWidth cw dw ct dt x⟩)) := by sorry