proposition: Lemma TM_loopM_canonize_tape (oq : TM.state M') t1 t2 k q' t'1 : canonize_tape t1 = canonize_tape t2 -> TM_facts.loopM (TM_facts.mk_mconfig oq (| t1 |)) k = Some (TM_facts.mk_mconfig q' t'1) -> { t'2 | TM_facts.loopM (TM_facts.mk_mconfig oq (| t2 |)) k = Some (TM_facts.mk_mconfig q' t'2) }.
proof: Proof. elim: k oq t1 t2. { move=> > _ /=. case: (halt' _) => [|]; last done. move=> [] /= -> _. by eexists. } move=> k IH oq t1 t2 Ht1t2 /=. case: (halt' _) => [|] /=. { move=> [] -> _. by eexists. } move E1: (TM_step _) => [q1 ts1]. move E2: (TM_step _) => [q2 ts2]. move: E1 E2. rewrite (Vector.eta ts1). move: (VectorDef.tl ts1). apply: Vector.case0. rewrite (Vector.eta ts2). move: (VectorDef.tl ts2). apply: Vector.case0. move: (Ht1t2) => /TM_step_canonize_tape /[apply] /[apply]. move=> [<-] /IH. by apply. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun