proposition: Theorem ndmm2_imsell_weak c Σ x y A : c ∊ Σ -> ⟬Σ,x,y⟭ ⊢ A <-> ![∞]⟬c⟭ :: ⟬Σ,x,y⟭ ++ nil ⊢ A.
proof: Proof. Proof using Hi. intros H; rewrite app_nil_r. apply S_imsell_extract; auto. apply in_app_iff; left. apply in_map_iff. exists ⟬c⟭ ; split; auto. apply in_map_iff; eauto. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)