proposition: Lemma KOSBTM_simulation (M : TM.TM (finType_CS bool) 1) : {M' : KOSBTM.KOSBTM | (forall q t t', TM.eval M (TM.start M) t q t' -> exists q', KOSBTM.eval M' Fin.F1 (conv_tape t) q' (conv_tape t')) /\ (forall t, (exists q' t', KOSBTM.eval M' Fin.F1 (conv_tape t) q' t') -> (exists q' t', TM.eval M (TM.start M) t q' t'))}.
proof: Proof. exists (KOSBTM.Build_KOSBTM (num_states M) (@trans M)). split. - intros q t t' H % red_correct1. eexists. econstructor. cbn. reflexivity. eapply H. - intros t (q' & t' & H). inversion H; subst; clear H. cbn in H0. inv H0. cbn in *. inv H0. eapply red_correct2 in H1 as (? & ? & -> & -> & H). eexists. eexists. eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts