proposition: Lemma MTM_TM_iff {sig n} {M : TM sig n} {ts : Vector.t (tape sig) n} : HaltsTM M ts <-> HaltsTM (MTM_TM.M' M) (MTM_TM.ts' ts).
proof: Proof. by apply: MTM_TM.MTM_to_stM_correct. Qed.
imports: Undecidability(TM.UTM TM.TM LambdaCalculus.Krivine MinskyMachines.MMA Shared.Libs.PSL.FiniteTypes.FinTypesDef) Coq(Vector ssreflect ssrbool ssrfun)