CookLevin.isFormulaStringB_machine_composed_fixed_child_reduction_child_leaf_child

Open

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

Child lemma for open leaf CookLevin.isFormulaStringB_machine_composed_fixed_child_reduction_child

Formal statement

import Definitions.Def_CookLevin_Verifier

open CookLevin

theorem CookLevin.isFormulaStringB_machine_composed_fixed_child_reduction_child_leaf_child :
    ∃ (M : Machine) (k G : Nat) (c1 c2 : Nat),
      TuringMachine k G M ∧
      ∀ x w : List Bool,
        DecidesIn M k (boolsToSymbols x) (boolsToSymbols w)
          (c1 * (x.length + 1) ^ 2 + c2 * (x.length + 1))
          (isFormulaStringB x) := by sorry

View graph