proposition: Fact ndmm2_imsell_eq2 Σ x y : ⟬Σ,x,y⟭ = ‼(map (fun c => (∞,⟬c⟭)) Σ ++ repeat (a,£0) x ++ repeat (b,£1) y).
proof: Proof. unfold ndmm2_imsell_ctx. rewrite map_map, ndmm2_imsell_eq1. unfold imsell_lban; rewrite !map_app, !map_map; f_equal. induction x; simpl; f_equal; auto. induction y; simpl; f_equal; auto. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)