proposition: Theorem ndmm2_imsell_sound Σ x y p : Σ //ₙ x ⊕ y ⊦ p -> ⟬Σ,x,y⟭ ⊢ ⌊p⌋.
proof: Proof. Proof using Hi Hbi Hai. induction 1 as [ p H1 | x y p q H1 H2 IH2 | x y p q H1 H2 IH2 | x y p q H1 H2 IH2 | x y p q H1 H2 IH2 | y p q H1 H2 IH2 | x p q H1 H2 IH2 ]. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l, in_imsell_limp_l; auto. apply in_imsell_limp_r. apply in_imsell_perm with (1 := Permutation_sym (Permutation_cons_append _ _)). unfold ndmm2_imsell_ctx; simpl; rewrite app_nil_r. apply S_imsell_gen_weak; auto. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l, in_imsell_limp_l; auto. apply in_imsell_limp_r. revert IH2; apply in_imsell_perm; auto. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l, in_imsell_limp_l; auto. apply in_imsell_limp_r. revert IH2; apply in_imsell_perm; auto. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l. apply in_imsell_perm with (Γ := α⊸⌊q⌋⊸⌊p⌋ :: (α::nil) ++ ⟬Σ,x,y⟭). * apply Permutation_sym, perm_skip; rewrite app_nil_r; simpl; auto. * apply in_imsell_limp_l; auto. rewrite <- app_nil_r with (l := ⟬_,_,_⟭). apply in_imsell_limp_l; auto. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l. apply in_imsell_perm with (Γ := β⊸⌊q⌋⊸⌊p⌋ :: (β::nil) ++ ⟬Σ,x,y⟭). * apply Permutation_sym, perm_skip; rewrite app_nil_r; simpl; auto. * apply in_imsell_limp_l; auto. rewrite <- app_nil_r with (l := ⟬_,_,_⟭). apply in_imsell_limp_l; auto. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l, in_imsell_limp_l; auto. rewrite ndmm2_imsell_eq2 in IH2 |- *. apply in_imsell_bang_r; auto. intros (v,A); simpl. rewrite in_app_iff, in_map_iff. intros [ (? & HvA & ?) | HvA ]. * now inversion HvA; subst. * now apply repeat_spec in HvA; inversion HvA. + apply ndmm2_imsell_weak with (1 := H1); simpl. apply in_imsell_bang_l, in_imsell_limp_l; auto. rewrite ndmm2_imsell_eq2 in IH2 |- *. apply in_imsell_bang_r; auto. intros (v,A); simpl. rewrite app_nil_r, in_app_iff, in_map_iff. intros [ (? & HvA & ?) | HvA ]. * now inversion HvA; subst. * now apply repeat_spec in HvA; inversion HvA. Qed.
imports: List Permutation Arith Lia Undecidability.MinskyMachines(ndMM2) Undecidability.ILL(IMSELL imsell) Undecidability.Shared.Libs.DLW(utils pos vec) Undecidability.Synthetic(Definitions ReducibilityFacts)