proposition: Lemma split_dp_top : forall f g ls lt, axiom (ddp (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1)))) (Term g lt) (Term f ls) -> ( (defined (@union _ R1 R2) f /\ defined (@union _ R1 R2) g) \/ (defined R3 f /\ defined R3 g) \/ (defined R3 f /\ defined (@union _ R1 R2) g)).
proof: Proof. destruct module_R1_R2 as [M2]. destruct module_R1_R3 as [M3]. intros f g ls lt H. inversion H as [_t _s sigma K]; clear H. destruct K as [K Sub']; inversion K as [s' t' p h l H' Sub Dh]; clear K; subst _s _t; subst. destruct s' as [x' | f' ls']. apply False_rect; apply (R123_var' _ _ H'). simpl in H1; injection H1; clear H1; intros; subst. injection H0; clear H0; intros; subst. destruct H' as [H12 | [ H3 | HPi]]. inversion Dh as [h' l' u [K12 | [K3 | KPi]]]; clear Dh; subst. left; split. apply (Def _ _ _ _ H12). apply (Def _ _ _ _ K12). destruct H12 as [H1 | H2]. generalize (M3 g _ _ (Def R3 g l' u K3) H1). simpl; rewrite (symb_in_subterm g _ _ Sub). simpl; intro; discriminate. simpl; generalize (F.Symb.eq_bool_ok g g); case (F.Symb.eq_bool g g); [intros _ | intros g_diff_g; absurd (g=g)]; trivial. assert (F := Indep3 _ _ _ (Def _ _ _ _ K3) H2). simpl in F; rewrite (symb_in_subterm g _ _ Sub) in F. discriminate. simpl; generalize (F.Symb.eq_bool_ok g g); case (F.Symb.eq_bool g g); [intros _ | intros g_diff_g; absurd (g=g)]; trivial. inversion KPi; subst g l' u. destruct H12 as [H1 | H2]. assert (H := P1 _ _ H1). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. assert (H := P2 _ _ H2). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. destruct H12 as [H1 | H2]. assert (H := P1 _ _ H1). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. assert (H := P2 _ _ H2). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. inversion Dh as [h' l' u K]; clear Dh; subst. destruct K as [K12 | [K3 | KPi]]. destruct K12 as [K1 | K2]. right; right; split. apply (Def _ _ _ _ H3). apply (Def (@union _ R1 R2) g l' u); left; trivial. assert (F := Indep2 _ _ _ (Def _ _ _ _ K2) H3). simpl in F; rewrite (symb_in_subterm g _ _ Sub) in F. discriminate. simpl; generalize (F.Symb.eq_bool_ok g g); case (F.Symb.eq_bool g g); [intros _ | intros g_diff_g; absurd (g=g)]; trivial. right; left; split. apply (Def _ _ _ _ H3). apply (Def _ _ _ _ K3). inversion KPi; subst g u l'. assert (H := P3 _ _ H3). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. assert (H := P3 _ _ H3). destruct (H pi) as [F _]. rewrite (symb_in_subterm pi _ _ Sub) in F. absurd (pi=pi); trivial; apply F; trivial. simpl; generalize (F.Symb.eq_bool_ok pi pi); case (F.Symb.eq_bool pi pi); [intros _ | intros pi_diff_pi; absurd (pi = pi)]; trivial. inversion HPi; subst; destruct p; discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)