Existence of multi-tape decider machine for satVerifier
ProvedCookLevin.satVerifierMachine_existscook-levindecider-machineverifier
There exists a 6-tape, 4-symbol multi-tape Turing machine that parses and verifies CNF formula assignments.
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.satVerifierMachine_exists :
∃ M : Machine, TuringMachine 6 4 M := by sorry
Source