proposition: Theorem reduction : TM.HaltTM 1 ⪯ KOSBTM.HaltKOSBTM.
proof: Proof. eapply reduces_transitive. eapply Arbitrary_to_Binary.reduction. unshelve eexists. { intros [M t]. refine (_, conv_tape t). refine (KOSBTM.Build_KOSBTM (num_states M) (@trans M)). } intros [M t]. split. - intros [q' [t' H]]. eapply red_correct1 in H. exists (conv_state q'), (conv_tape t'). econstructor. cbn. reflexivity. eapply H. - intros [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