proposition: Lemma split_dp : forall s t, axiom (ddp (@union _ (@union _ (@union _ R1 R2) R3) (Pi pi V0 V1))) s t -> (axiom (ddp (@union _ R1 R2)) s t \/ axiom (ddp R3) s t \/ (exists t3, exists t1, exists p, exists f1, exists l1, exists sigma, R3 t1 t3 /\ subterm_at_pos t1 p = Some (Term f1 l1) /\ defined R1 f1 /\ t = apply_subst sigma t3 /\ s = apply_subst sigma (Term f1 l1))).
proof: Proof. inversion module_R1_R2 as [M2]. inversion module_R1_R3 as [M3]. intros _s _t _H; inversion _H as [s t sigma H]; clear _H; subst. destruct H as [H Sub']; inversion H as [s' t' p f l H' Sub Df]; clear H; subst. destruct H' as [H123 | HPi]. destruct H123 as [H12 | H3]. inversion Df as [f' l' u K]; clear Df; subst. destruct K as [K123 | KPi]. destruct K123 as [K12 | K3]. left; apply instance; split; [apply Dp with t' p |idtac]; trivial. apply (Def _ _ _ _ K12). destruct H12 as [H1 | H2]. generalize (M3 f t' _ (Def R3 f l' u K3) H1). simpl; rewrite (symb_in_subterm f _ _ Sub). simpl; intro; discriminate. simpl; rewrite eq_symb_bool_refl; apply eq_refl. assert (F := Indep3 _ _ _ (Def _ _ _ _ K3) H2). simpl in F; destruct (symb_in_term f t). destruct (symb_in_term f t'); discriminate. rewrite (symb_in_subterm f _ _ Sub) in F. discriminate. simpl; rewrite eq_symb_bool_refl; trivial. inversion KPi; subst f u l'. 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; rewrite eq_symb_bool_refl; 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; rewrite eq_symb_bool_refl; 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; rewrite eq_symb_bool_refl; 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; rewrite eq_symb_bool_refl; trivial. inversion Df as [f' l' u K]; clear Df; subst. destruct K as [K123 | KPi]. destruct K123 as [K12 | K3]. destruct K12 as [K1 | K2]. right; right; trivial. exists t; exists t'; exists p; exists f; exists l; exists sigma; split; trivial. split; trivial. split. apply (Def _ _ _ _ K1). split; trivial. assert (F := Indep2 _ _ _ (Def _ _ _ _ K2) H3). simpl in F; destruct (symb_in_term f t). destruct (symb_in_term f t'); discriminate. rewrite (symb_in_subterm f _ _ Sub) in F. discriminate. simpl; rewrite eq_symb_bool_refl; trivial. right; left; apply instance; split; [apply Dp with t' p | idtac]; trivial. apply (Def _ _ _ _ K3). inversion KPi; subst f 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; rewrite eq_symb_bool_refl; 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; rewrite eq_symb_bool_refl; 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)