Prove2Me

CookLevin.satisfiesB_machine_quad_core_leaf_child

Open

by Rizwan · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

Child lemma for open leaf CookLevin.satisfiesB_machine_quad_core

Formal statement
import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.satisfiesB_machine_quad_core_leaf_child :
    ∃ (M : Machine) (c0 : Nat),
      TuringMachine 6 4 M ∧
      ∀ x w : List Bool,
        DecidesIn M 6 (boolsToSymbols x) (boolsToSymbols w)
          (c0 * (x.length + w.length + 1) ^ 2)
          (satisfiesB (decodeAssignment w) (decodeFormula x)) := by sorry

View graph