Prove2Me

CookLevin.DecidesIn_mono_bools_v2

Proved

by junyihjy · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

A Boolean-input computation that decides a verdict within t steps has the same verdict at every later time bound T. This is the Boolean-list specialization of the established monotonicity lemma.

Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin

theorem CookLevin.DecidesIn_mono_bools_v2
    {M : Machine} {k : Nat} {x w : List Bool}
    {t T : Nat} {b : Bool}
    (h : DecidesIn M k (boolsToSymbols x) (boolsToSymbols w) t b) (hle : t ≤ T) :
    DecidesIn M k (boolsToSymbols x) (boolsToSymbols w) T b := by
  sorry

View graph