proposition: Lemma vec_change_app_left {X} (n m : nat) v1 v2 p x: vec_change (@vec_app X n m v1 v2) (pos_left m p) x = vec_app (vec_change v1 p x) v2.
proof: Proof. eapply vec_pos_ext. eapply pos_left_right_rect. - intros. rewrite !vec_pos_app_left. destruct (pos_eq_dec p p0). + subst. rewrite vec_change_eq. 2: reflexivity. now rewrite vec_change_eq. + rewrite vec_change_neq. 2: intros ? % pos_left_inj; congruence. rewrite vec_pos_app_left. rewrite vec_change_neq; auto. - intros p0. rewrite !vec_pos_app_right. rewrite vec_change_neq; auto. now rewrite vec_pos_app_right. 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)