proposition: Lemma red_correct2 q t q'_ t'_ : KOSBTM.eval (KOSBTM.Build_KOSBTM num_states trans) (conv_state q) (conv_tape t) q'_ t'_ -> exists q' t', q'_ = conv_state q' /\ t'_ = conv_tape t' /\ TM.eval M q t q' t'.
proof: Proof. intros H. remember (conv_state q) as q_. remember (conv_tape t) as t_. induction H in q, t, Heqq_, Heqt_ |- *; subst. + exists q, t. repeat split. econstructor. unfold KOSBTM.trans, trans in H. revert H. generalize (eq_refl (conv_state q)). pattern (conv_state q) at 1 3. eapply Fin.caseS'; cbn. -- intros ? [=]. -- intros ? ? ?. destruct TM.halt eqn:E. ++ unfold conv_state in H. eapply Fin.FS_inj in H as ->. now rewrite Hg in E. ++ now destruct TM.trans, Vector.hd. + unfold KOSBTM.trans, trans in H. revert H. generalize (eq_refl (conv_state q)). pattern (conv_state q) at 1 3. eapply Fin.caseS'; cbn. * intros ? [=]. unfold conv_state in *. inv H. * intros ? ?. unfold conv_state in *. eapply Fin.FS_inj in H; subst. rewrite Hg. destruct TM.halt eqn:E. -- intros [=]. -- rewrite (destruct_vector_single t) in *. destruct TM.trans as [? to] eqn:Et. cbn in *. destruct (Vector.hd to) eqn:E't. intros [=]; subst. rewrite current_red in Et. edestruct IHeval as (q''' & t''' & ? & ? & ?). ++ reflexivity. ++ rewrite wr_red, mv_red. reflexivity. ++ rewrite (destruct_vector_single t), (destruct_vector_single t''') in *. cbn in *. subst. repeat esplit; [eassumption..|]. econstructor; [eassumption..|]. now rewrite (destruct_vector_single to), E't. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors