Multi-tape decider for conjunction of poly-time decidable relations
ProvedCookLevin.polyTimeDecidable_and_corecomplexitycook-levindecidable
If binary relations f and g are decidable in polynomial time by multi-tape Turing machines, then so is their conjunction (f and g).
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.polyTimeDecidable_and_core (f g : List Bool → List Bool → Bool)
(hf : PolyTimeDecidable f) (hg : PolyTimeDecidable g) :
∃ M k G c d, TuringMachine k G M ∧ ∀ x w : List Bool, DecidesIn M k (boolsToSymbols x) (boolsToSymbols w) (polyBound c d (x.length + w.length)) (f x w && g x w) := by sorry
Source