proposition: Lemma vec'_change_app_right {X : Type} (n m : nat) (v1 : vec X n) (v2 : vec X m) (p : pos m) (x : X) : vec_change (v1 +++ v2) (pos_right n p) x = v1 +++ (vec_change v2 p x).
proof: Proof. rewrite <- !vec_app_spec. apply vec_change_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)