proposition: Lemma encode_bsm_ext Σ n v : @encode_bsm Σ n v = [] ::: [false] ::: (encode_bsm v @[Fin2]) ::: [] ::: vec_nil.
proof: Proof. eapply vec_pos_ext. eapply Fin4_cases. - now rewrite vec_pos_spec, encode_bsm_at0. - now rewrite vec_pos_spec, encode_bsm_at1. - reflexivity. - now rewrite vec_pos_spec, encode_bsm_at3. Qed.
imports: Undecidability.StackMachines.BSM Undecidability.StackMachines.Util.BSM_computable Undecidability.TM.TM Undecidability.TM.Util.TM_facts Undecidability.TM.Util.TM_computable Undecidability.TM(TM Arbitrary_to_Binary mTM_to_TM HaltTM_1_to_HaltKOSBTM HaltKOSBTM_to_HaltBSM) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Undecidability(bsm_utils bsm_defs) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes)