proposition: Fact ndmm2_imsell_perm1 Σ x y : ⟬Σ,1+x,y⟭ ~p α::⟬Σ,x,y⟭ .
proof: Proof. unfold ndmm2_imsell_ctx. apply Permutation_sym, perm_trans with (1 := Permutation_cons_append _ _). rewrite <- !app_assoc; apply Permutation_app; auto. simpl; apply Permutation_sym, perm_trans with (1 := Permutation_cons_append _ _). now rewrite <- app_assoc. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)