CookLevin.satVerifierMachine_decides_eval_core_leaf_child

import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.satVerifierMachine_decides_eval_core_leaf_child :
    ∀ (M : Machine), TuringMachine 6 4 M → ∀ x w : List Bool, DecidesIn M 6 (boolsToSymbols x) (boolsToSymbols w) (polyBound 1 2 (x.length + w.length)) (satVerifier x w) := by sorry