proposition: Lemma modular_termination_indep_list_lift : forall (V0 V1 : variable), V0 <> V1 -> forall pi (list_rel : list (rwr_rel pi)) R', (forall R1 R2 L' L'' L''', list_rel = L' ++ R1 :: L'' ++ R2 :: L''' -> ident pi R1 <> ident pi R2) -> well_founded (ddp_step (@union _ (Rel pi R') (Pi pi V0 V1))) -> (forall R, In R list_rel -> module (Rel pi R') (Rel pi R)) -> (forall R, In R list_rel -> well_founded (rdp_step (axiom (ddp (Rel pi R))) (@union _ (@union _ (Rel pi R) (Rel pi R')) (Pi pi V0 V1)))) -> (forall R1 R2, In R1 list_rel -> In R2 list_rel -> ident pi R1 <> ident pi R2 -> (forall s t f, defined (Rel pi R1) f -> (Rel pi R2) s t -> symb_in_term_list f (s :: t :: nil) = false)) -> well_founded (ddp_step (fold_left (fun acc Rr => @union _ (Rel pi Rr) acc) list_rel (@union _ (Rel pi R') (Pi pi V0 V1)))).
proof: Proof. intros V0 V1 V0_diff_V1 pi L R' U W' ML WL IL. assert (fold_incl : forall (L0 : list (rwr_rel pi)) (P0 P1 : term -> term -> Prop), @inclusion term P0 P1 -> @inclusion term (fold_left (fun (acc : relation term) (Rr : rwr_rel pi) => @union term (Rel pi Rr) acc) L0 P0) (fold_left (fun (acc : relation term) (Rr : rwr_rel pi) => @union term (Rel pi Rr) acc) L0 P1)). intro L'; induction L' as [ | R'' L'']; simpl; intros P1 P2 P1_in_P2; trivial. apply IHL''. intros t1 t2 [H'' | H1]. left; trivial. right; apply P1_in_P2; trivial. assert (Gen : forall (R0 : rwr_rel pi), module (Rel pi R') (Rel pi R0) -> (well_founded (rdp_step (axiom (ddp (Rel pi R0))) (@union _ (@union _ (Rel pi R') (Rel pi R0)) (Pi pi V0 V1)))) -> (forall R2, In R2 L -> (forall s t f, defined (Rel pi R0) f -> (Rel pi R2) s t -> symb_in_term_list f (s :: t :: nil) = false)) -> (forall R1, In R1 L -> (forall s t f, defined (Rel pi R1) f -> (Rel pi R0) s t -> symb_in_term_list f (s :: t :: nil) = false)) -> well_founded (ddp_step (fold_left (fun acc Rr => @union _ (Rel pi Rr) acc) L (@union _ (@union _ (Rel pi R') (Rel pi R0)) (Pi pi V0 V1))))). induction L as [ | R L]; intros R0 M0 W0 I1 I2; simpl; trivial. apply (modular_termination_hierarch_lift V0 V1 V0_diff_V1) with (rules pi R') (rules pi R0); trivial. apply (REquiv pi R'). apply (RR_var pi R'). apply (RR_reg pi R'). apply (RP pi R'). apply (REquiv pi R0). apply (RR_var pi R0). apply (RR_reg pi R0). apply (RP pi R0). apply wf_incl with (ddp_step (fold_left (fun (acc : relation term) (Rr : rwr_rel pi) => @union term (Rel pi Rr) acc) L (@union term (@union term (Rel pi R') (Rel pi (rwr_rel_comb pi R R0))) (Pi pi V0 V1)))). apply ddp_step_incl. apply fold_incl. intros t1 t2 [H | [[H' | H0] | Hpi]]. left; right; left; trivial. do 2 left; trivial. left; do 2 right; trivial. right; trivial. apply IHL. intros R1 R2 L' L'' L''' H; apply (U R1 R2 (R :: L') L'' L'''); simpl; rewrite H; trivial. intros R1 R1_in_L; apply ML; right; trivial. intros R1 R1_in_L; apply WL; right; trivial. intros R1 R2 R1_in_L R2_in_L; apply IL; right; trivial. simpl; apply Mod. intros f s t Df H'; destruct Df as [f' l u [H | H0]]. destruct (ML R (or_introl _ (eq_refl _))) as [M']. apply (M' f' s t (Def (Rel pi R) f' l u H)); trivial. destruct M0 as [M0]. apply (M0 f' s t (Def (Rel pi R0) f' l u H0)); trivial. simpl; assert (M := modular_termination_lift _ _ V0_diff_V1 pi (Rel pi R') (Rel pi R) (Rel pi R0) (ML _ (or_introl _ (eq_refl _))) M0 _ (REquiv pi R') (RR_var pi R') (RR_reg pi R') (RP pi R') _ (REquiv pi R) (RR_var pi R) (RR_reg pi R) (RP pi R) _ (REquiv pi R0) (RR_var pi R0) (RR_reg pi R0) (RP pi R0) (I2 R (or_introl _ (eq_refl _))) (I1 R (or_introl _ (eq_refl _)))). apply wf_incl with (ddp_step (@union term (@union term (Rel pi R') (Rel pi R)) (@union term (Rel pi R0) (Pi pi V0 V1)))). apply rddp_step_incl. intros t1 t2 [H | H0]. left; right; trivial. right; left; trivial. intros t1 t2 [[H' | [H | H0]] | Hpi]. do 2 left; trivial. left; right; trivial. right; left; trivial. do 2 right; trivial. apply M; trivial. apply (modular_termination_hierarch_lift V0 V1 V0_diff_V1) with (rules pi R') (rules pi R); trivial. apply ML; left; trivial. apply (REquiv pi R'). apply (RR_var pi R'). apply (RR_reg pi R'). apply (RP pi R'). apply (REquiv pi R). apply (RR_var pi R). apply (RR_reg pi R). apply (RP pi R). apply wf_incl with (rdp_step (axiom (ddp (Rel pi R))) (@union term (@union term (Rel pi R) (Rel pi R')) (Pi pi V0 V1))). apply rddp_step_incl. intros t1 t2; trivial. intros t1 t2 [[H | H'] | Hpi]. left; right; trivial. do 2 left; trivial. right; trivial. apply WL; left; trivial. intros R2 R2_in_L. intros s t f Df H2; simpl in Df; destruct Df as [f' l u [H | H0]]. apply IL with R R2; trivial. left; trivial. right; trivial. destruct (In_split _ _ R2_in_L) as [L'' [L''' H']]. apply (U R R2 nil L'' L'''); simpl; subst L; trivial. apply (Def (Rel pi R) f' l u H). apply I1 with R2; trivial. right; trivial. apply (Def (Rel pi R0) f' l u H0). intros R1 R1_in_L. intros s t f Df [H | H0]. apply IL with R1 R; trivial. right; trivial. left; trivial. destruct (In_split _ _ R1_in_L) as [L'' [L''' H']]. intro H'''; refine (U R R1 nil L'' L''' _ _); simpl; subst; symmetry; trivial. apply I2 with R1; trivial; right; trivial. apply wf_incl with (ddp_step (fold_left (fun (acc : relation term) (Rr : rwr_rel pi) => @union term (Rel pi Rr) acc) L (@union term (@union term (Rel pi R') (Rel pi (rwr_rel_empty pi))) (Pi pi V0 V1)))). apply rddp_step_incl. apply fold_incl. intros t1 t2 [H' | Hpi]. do 2 left; trivial. right; trivial. apply fold_incl. intros t1 t2 [H' | Hpi]. do 2 left; trivial. right; trivial. apply Gen. apply Mod; intros f s t Df; inversion Df as [f' l u H]; case H. simpl; intro s; apply Acc_intro; intros _t H. inversion H as [g k l' s'' l_R_l' _Hm]; clear H; subst. inversion _Hm as [t s sigma Hm K1 K2]; clear _Hm; subst. destruct Hm as [Hm _Sub]. inversion Hm as [s' t' p g'' k'' t_R_s Sub Df'' H1 H']; case t_R_s. intros R2 _ s t f Df; inversion Df as [f' l u H]; case H. intros R1 _ s t f _ H; case H. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)