proposition: Lemma modular_termination_lift : forall (V0 V1 : variable), V0 <> V1 -> forall pi R1 R2 R3, module R1 R2 -> module R1 R3 -> forall rule_list1, (forall l r, R1 r l <-> In (l,r) rule_list1) -> (forall l r, In (l,r) rule_list1 -> forall v, l <> Var v) -> (forall l r, In (l,r) rule_list1 -> forall v, In v (var_list r) -> In v (var_list l)) -> (forall l r, In (l,r) rule_list1 -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) -> forall rule_list2, (forall l r, R2 r l <-> In (l,r) rule_list2) -> (forall l r, In (l,r) rule_list2 -> forall v, l <> Var v) -> (forall l r, In (l,r) rule_list2 -> forall v, In v (var_list r) -> In v (var_list l)) -> (forall l r, In (l,r) rule_list2 -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) -> forall rule_list3, (forall l r, R3 r l <-> In (l,r) rule_list3) -> (forall l r, In (l,r) rule_list3 -> forall v, l <> Var v) -> (forall l r, In (l,r) rule_list3 -> forall v, In v (var_list r) -> In v (var_list l)) -> (forall l r, In (l,r) rule_list3 -> (forall f, ((symb_in_term f r = true -> f <> pi) /\ (symb_in_term f l = true -> f <> pi)))) -> (forall s t f, defined R2 f -> R3 s t -> symb_in_term_list f (s :: t :: nil) = false) -> (forall s t f, defined R3 f -> R2 s t -> symb_in_term_list f (s :: t :: nil) = false) -> well_founded (ddp_step (@union _ (@union _ R1 R2) (Pi pi V0 V1))) -> well_founded (rdp_step (axiom (ddp R3)) (@union _ (@union _ R1 R3) (Pi pi V0 V1))) -> well_founded (ddp_step (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1)))).
proof: Proof. intros V0 V1 V0_diff_V1 pi R1 R2 R3 M12 M13 rule_list1 Equiv1 R1_var R1_reg P1 rule_list2 Equiv2 R2_var R2_reg P2 rule_list3 Equiv3 R3_var R3_reg P3 Indep2 Indep3 W12 W3. apply (modular_termination _ _ V0_diff_V1 pi pi R1 R2 R3 (def_dec_rules _ _ Equiv1) (def_dec_rules _ _ Equiv2) (def_dec_rules _ _ Equiv3) _ _ _ (fun s t => iff_sym (compute_red_is_correct _ R1_reg _ Equiv1 s t)) (fun s t => iff_sym (compute_red_is_correct _ R2_reg _ Equiv2 s t)) (fun s t => iff_sym (compute_red_is_correct _ R3_reg _ Equiv3 s t))); trivial. intros s t H1; apply R1_reg; rewrite <- Equiv1; trivial. intros s t H2; apply R2_reg; rewrite <- Equiv2; trivial. intros s t H3; apply R3_reg; rewrite <- Equiv3; trivial. intros x t H1; rewrite Equiv1 in H1; apply (R1_var _ _ H1 x); trivial. intros x t H2; rewrite Equiv2 in H2; apply (R2_var _ _ H2 x); trivial. intros x t H3; rewrite Equiv3 in H3; apply (R3_var _ _ H3 x); trivial. intros s t H1; apply (P1 t s); rewrite <- Equiv1; trivial. intros s t H2; apply (P2 t s); rewrite <- Equiv2; trivial. intros s t H3; apply (P3 t s); rewrite <- Equiv3; trivial. apply ddp_criterion; trivial. apply R12_var'. intros x t H1; rewrite Equiv1 in H1; apply (R1_var _ _ H1 x); trivial. intros x t H2; rewrite Equiv2 in H2; apply (R2_var _ _ H2 x); trivial. intros s t [[H1 | H2] | Hpi]. apply R1_reg; rewrite <- Equiv1; trivial. apply R2_reg; rewrite <- Equiv2; trivial. inversion Hpi; subst. intros x [x_eq_v1 | x_in_nil]; [left; trivial | contradiction]. intros x [x_eq_v2 | x_in_nil]; [right; left; trivial | contradiction]. intros f; destruct (def_dec_rules _ _ Equiv1 f) as [D1 | C1]. right; inversion D1 as [f' l u H1]. subst f'; apply (Def (@union _ (@union _ R1 R2) (Pi pi V0 V1)) f l u); left; left; trivial. destruct (def_dec_rules _ _ Equiv2 f) as [D2 | C2]. right; inversion D2 as [f' l u H2]. subst f'; apply (Def (@union _ (@union _ R1 R2) (Pi pi V0 V1)) f l u); left; right; trivial. generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst f; right; apply (Def (@union _ (@union _ R1 R2) (Pi pi V0 V1)) pi (Var V0 :: Var V1 :: nil) (Var V0)). right; apply Pi1. left; apply Const; intros l u [[H1 | H2] | Hpi]. apply C1; apply (Def R1 f l u H1). apply C2; apply (Def R2 f l u H2). inversion Hpi; subst f; apply f_diff_pi; trivial. refine (wf_incl _ _ _ _ W12). intros u1 u2 [H _]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)