proposition: Lemma TM_step_canonize_tape oq oq1 t1 t'1 oq2 t2 t'2 : canonize_tape t1 = canonize_tape t2 -> TM_step (TM_facts.mk_mconfig oq (| t1 |)) = TM_facts.mk_mconfig oq1 (| t'1 |) -> TM_step (TM_facts.mk_mconfig oq (| t2 |)) = TM_facts.mk_mconfig oq2 (| t'2 |) -> oq1 = oq2 /\ canonize_tape t'1 = canonize_tape t'2.
proof: Proof. move=> Ht1t2. rewrite /TM_facts.step /= -(get_symbol_canonize_tape Ht1t2). case: oq => [q|]. - move: (trans' M _) => [[[q' a'] d']|] /=. + move=> [] <- <- [] <- <-. split; first done. by apply: doAct_canonize_tape. + by move=> [] <- <- [] <- <-. - by move=> [] <- <- [] <- <-. Qed.
imports: Undecidability(TM.SBTM TM.Util.SBTM_facts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes PeanoNat Lia List ssreflect ssrbool ssrfun