proposition: Lemma TM_BTM_iff {sig} {M : TM sig 1} {ts : Vector.t (tape sig) 1} : HaltsTM M ts <-> HaltsTM (TM_BTM.M' M) (cons _ (hd (TM_BTM.ts' ts)) 0 (nil _)).
proof: Proof. have -> (A) (v : Vector.t A 1) : cons _ (hd v) 0 (nil _) = v by rewrite (vec.vec_head_tail v) (vec.vec_0_nil (vec.vec_tail v)). by apply: TM_BTM.HaltTM_Σ_to_HaltTM_bool_correct. Qed.
imports: Undecidability(TM.UTM TM.TM LambdaCalculus.Krivine MinskyMachines.MMA Shared.Libs.PSL.FiniteTypes.FinTypesDef) Coq(Vector ssreflect ssrbool ssrfun)