Well-formedness of the composite reduction emitter machine
ProvedCookLevin.reductionEmitM_wfcook-levinreductionwell-formedness
The composite reduction emitter machine is a well-formed Turing machine for tapes and alphabet size .
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_wf (Mv : Machine) (k G : Nat) (hwf : TuringMachine k G Mv) :
∃ M : Machine, TuringMachine k G M := by sorry
Source