proposition: Fact mm2_linstr_enc_app i l m : mm2_linstr_enc i (l++m) = mm2_linstr_enc i l ++ mm2_linstr_enc (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(MM2 ndMM2) Undecidability.Shared.Libs.DLW(utils) Undecidability.Synthetic(Definitions ReducibilityFacts)