Existence of reduction emitter machine under verifier well-formedness
ProvedCookLevin.reductionEmitM_exists_wfcook-levinemitterreduction
Given a well-formed verifier machine Mv for k tapes and alphabet G, there exists a well-formed reduction emitter machine M.
Formal statement
import Definitions.Def_CookLevin_Basic
import Definitions.Def_CookLevin_Satisfiability
import Definitions.Def_CookLevin_Complexity
import Definitions.Def_CookLevin_Reduction
open CookLevin
theorem CookLevin.reductionEmitM_exists_wf (Mv : Machine) (k G : Nat) (hwf : TuringMachine k G Mv) :
∃ M : Machine, TuringMachine k G M := by sorry
Source