proposition: Lemma vec_list_encode_bsm Σ n1 n2 v1 v2 : vec_list v1 = vec_list v2 -> vec_list (@encode_bsm Σ n1 v1) = vec_list (@encode_bsm Σ n2 v2).
proof: Proof. intros H. assert (n1 = n2). 1: eapply (f_equal (@length _)) in H. 1: rewrite !vec_list_length in H. 1: assumption. subst. apply vec_list_inj in H. now subst. 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)