proposition: Lemma almost_eq_tape_step_Some M q q1 q2 t1 t'1 t2 t'2 : almost_eq_tape t1 t2 -> step M (q, t1) = Some (q1, t'1) -> step M (q, t2) = Some (q2, t'2) -> q1 = q2 /\ almost_eq_tape t'1 t'2.
proof: Proof. have ? := almost_eq_false 0 0. have ? := almost_eq_false 0 _. have ? := almost_eq_false _ 0. case=> a ???? [] => [????|n1 n2] []. - move=> ????. rewrite /step /=. case: (trans' M _); last done. move=> [[? ?] []] [] <- <- [] <- <- /=; by do ? constructor. - move=> n'1 n'2. rewrite /step /=. case: (trans' M _); last done. move=> [[? ?] []] [] <- <- [] <- <- /=; first by do ? constructor. move: n'1 n'2 => [|?] [|?] /=; by do ? constructor. - move=> ????. rewrite /step /=. case: (trans' M _); last done. move=> [[? ?] []] [] <- <- [] <- <- /=; last by do ? constructor. move: n1 n2 => [|?] [|?] /=; by do ? constructor. - move=> n'1 n'2. rewrite /step /=. case: (trans' M _); last done. move=> [[? ?] []] [] <- <- [] <- <- /=. + move: n1 n2 => [|?] [|?] /=; by do ? constructor. + move: n'1 n'2 => [|?] [|?] /=; by do ? constructor. Qed.
imports: Undecidability(TM.SBTM) PeanoNat Lia List ssreflect ssrbool ssrfun