proposition: Fact mma2_linstr_enc_app i l m : ⟪i,l++m⟫ₗ = ⟪i,l⟫ₗ ++ ⟪length l+i,m⟫ₗ.
proof: Proof. revert i; induction l as [ | ? l IHl ]; intros ?; simpl; auto. rewrite <- app_assoc, IHl; do 3 f_equal; auto. Qed.
imports: List Arith Lia Relations Undecidability.MinskyMachines(MMA mma_defs ndMM2) Undecidability.Shared.Libs.DLW(utils Vec.pos Vec.vec Code.subcode Code.sss) Undecidability.Synthetic(Definitions ReducibilityFacts)