proposition: Lemma TM_eval_iff (Σ : finType) n (M : TM Σ n) q t q' t' : TM.eval M q t q' t' <-> exists n, loopM (M := M) (mk_mconfig q t) n = Some (mk_mconfig q' t').
proof: Proof. split. - induction 1 as [ | q t q' a q'' t' H0 H1 H2 [m IH]]. + exists 0. cbn. unfold haltConf. cbn. now rewrite H. + exists (S m). cbn. unfold haltConf. cbn. rewrite H0. unfold step. cbn. unfold current_chars. rewrite H1. erewrite Vector_map2_ext. * now rewrite IH. * intros [] [[] []]; reflexivity. - intros [k H]. induction k in q, t, H, q', t' |- *; cbn in H; unfold haltConf in H; cbn in H. + destruct halt eqn:E; inv H. now econstructor. + destruct halt eqn:E; inv H. * now econstructor. * unfold step in H1. cbn in H1. destruct trans eqn:E2. econstructor; [ eassumption .. | ]. eapply IHk. erewrite Vector_map2_ext. -- now rewrite H1. -- intros [] [[] []]; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM