proposition: Theorem ndmm2_imsell_complete p x y : ⟬Σ,x,y⟭ ⊢ ⌊p⌋ -> Σ //ₙ x ⊕ y ⊦ p.
proof: Proof. Proof using Hba Hb Hab Ha. intros Hxy; apply imsell_tps_sound with (s := sem) (K := K) in Hxy; eauto. specialize (Hxy (x##y##vec_nil)). rewrite vec_add_comm, vec_zero_plus in Hxy. apply Hxy; clear Hxy. unfold ndmm2_imsell_ctx. apply imsell_tps_app. exists ⦳, (x##y##ø). rewrite vec_zero_plus; msplit 2; auto. + rewrite map_map; apply sem_Σ_zero; auto. + apply imsell_tps_app. exists (x##0##ø), (0##y##ø); msplit 2; auto. * rewrite pair_plus; f_equal; lia. * generalize x; clear x y; intros n. induction n as [ | n IHn ]; simpl; auto. exists (1##0##ø), (n##0##ø); simpl; msplit 2; auto. rewrite HKa; auto. * generalize y; clear x y; intros n. induction n as [ | n IHn ]; simpl; auto. exists (0##1##ø), (0##n##ø); simpl; msplit 2; auto. rewrite HKb; 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)