proposition: Lemma ma_relative_termination : let E_gt := partition part_succ E in let E_ge := partition part_succeq E in let R_gt := partition part_succ R in let R_ge := partition part_succeq R in monotone I succ -> snd R_ge = nil -> snd E_ge = nil -> WF (red_mod (snd E_gt) (snd R_gt)) -> WF (red_mod E R).
proof: Proof. intros. unfold red_mod. set (Egt := fst E_gt) in *. set (Ege := snd E_gt) in *. set (Rgt := fst R_gt) in *. set (Rge := snd R_gt) in *. apply WF_incl with ((red Egt U red Ege)# @ (red Rgt U red Rge)). comp. apply rtc_incl. apply rule_partition_complete. apply rule_partition_complete. apply wf_rel_mod. fold (red_mod Ege Rge). hyp. apply WF_incl with (red_mod (Rge ++ Ege) (Rgt ++ Egt)). unfold red_mod. comp. apply rtc_incl. apply red_union_inv. apply red_union_inv. apply ma_compat_red_mod; trivial. apply compat_app. unfold Rgt, R_gt, part_succ. apply partition_succ_compat. unfold Egt, E_gt, part_succ. apply partition_succ_compat. apply compat_app. unfold Rge, R_gt. apply partition_succeq_compat. hyp. unfold Ege, E_gt. apply partition_succeq_compat. hyp. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)