proposition: Lemma update_app_right {X} (x : X) l1 l2 i : i >= length l1 -> update i (l1 ++ l2) x = l1 ++ update (i - length l1) l2 x.
proof: Proof. induction l1 in i |- *; cbn. - now rewrite Nat.sub_0_r. - intros Hi. destruct i. 1: lia. cbn. rewrite IHl1. 1: reflexivity. lia. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)