proposition: Lemma modular_termination_indep_lift : forall (V0 V1 : variable), V0 <> V1 -> forall pi R2 R3, 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 _ R2 (Pi pi V0 V1))) -> well_founded (ddp_step (@union _ R3 (Pi pi V0 V1))) -> well_founded (ddp_step (@union _ (@union _ R2 R3) (Pi pi V0 V1))).
proof: Proof. intros V0 V1 V0_diff_V1 pi R2 R3 rule_list2 Equiv2 R2_var R2_reg P2 rule_list3 Equiv3 R3_var R3_reg P3 Indep2 Indep3 W12 W3. apply wf_incl with (ddp_step (@union term (@union _ Empty_R R2) (@union term R3 (Pi pi V0 V1)))). intros t1 t2; apply ddp_step_incl; clear t1 t2. intros t1 t2 [[H2 | H3] | Hpi]. left; right; trivial. right; left; trivial. do 2 right; trivial. apply (modular_termination_lift _ _ V0_diff_V1 pi Empty_R R2 R3 (module_empty R2) (module_empty R3)) with (@nil (term * term)) rule_list2 rule_list3; trivial. apply list_rules_empty. intros s t H; case H. intros s t H; case H. intros s t H; case H. apply wf_incl with (ddp_step (@union term R2 (Pi pi V0 V1))); trivial. assert (H : @inclusion term (@union term (@union term Empty_R R2) (Pi pi V0 V1)) (@union term R2 (Pi pi V0 V1))). intros t1 t2 [[HE | H2] | Hpi]. case HE. left; trivial. right; trivial. apply ddp_step_incl; trivial. apply wf_incl with (rdp_step (axiom (ddp (@union term R3 (Pi pi V0 V1)))) (@union term R3 (Pi pi V0 V1))); trivial. clear; intros s t H; inversion H; clear H; subst. apply Rdp_step with l2. refine (refl_trans_incl (one_step_list_incl _ (one_step_incl _ _ _)) H0). clear; intros t1 t2 [[HE | H3] | Hpi]. case HE. left; trivial. right; trivial. inversion H1; apply instance. destruct H3 as [H3 Sub]. inversion H3; clear H3; subst. split; [apply Dp with t3 p | idtac]; trivial. left; assumption. inversion H6; clear H6; subst. apply (Def _ f2 l t); left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)