proposition: Lemma modular_termination_hierarch_lift : forall (V0 V1 : variable), V0 <> V1 -> forall pi R1 R3, 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_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)))) -> well_founded (ddp_step (@union _ R1 (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 R3) (Pi pi V0 V1))).
proof: Proof. intros V0 V1 V0_diff_V1 pi R1 R3 M13 rule_list1 Equiv1 R1_var R1_reg P1 rule_list3 Equiv3 R3_var R3_reg P3 W12 W3. apply wf_incl with (ddp_step (@union term (@union _ R1 Empty_R) (@union term R3 (Pi pi V0 V1)))). intros t1 t2; apply ddp_step_incl; clear t1 t2. intros t1 t2 [[H1 | H3] | Hpi]. do 2 left; trivial. right; left; trivial. do 2 right; trivial. apply (modular_termination_lift _ _ V0_diff_V1 pi R1 Empty_R R3) with rule_list1 (@nil (term * term)) rule_list3; trivial. apply Mod; intros f s t [f' l u HE]; case HE. apply list_rules_empty. intros s t H; case H. intros s t H; case H. intros s t H; case H. intros s t f [f' l u HE]; case HE. intros s t f _ HE; case HE. apply wf_incl with (ddp_step (@union term R1 (Pi pi V0 V1))); trivial. apply ddp_step_incl. intros t1 t2 [[H1 | HE] | Hpi]. left; trivial. case HE. right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)