proposition: Lemma red_correct1 q q' t t' : TM.eval M q t q' t' -> KOSBTM.eval (KOSBTM.Build_KOSBTM num_states trans) (conv_state q) (conv_tape t) (conv_state q') (conv_tape t').
proof: Proof. induction 1. + eapply KOSBTM.eval_halt. cbn. now rewrite Hg, H. + rewrite (destruct_vector_single t), (destruct_vector_single a) in *. cbn in *. rewrite <- current_red in H0. destruct TM.trans eqn:E. inv H0. destruct (Vector.hd a) as (w, m). eapply KOSBTM.eval_step with (q' := conv_state q') (w := w) (m := conv_move m). * cbn. rewrite Hg, H, E. reflexivity. * now rewrite wr_red, mv_red. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors