proposition: Lemma ma_relative_top_termination : let E_ge := partition part_succeq E in let R_gt := partition part_succ R in let R_ge := partition part_succeq R in snd R_ge = nil -> snd E_ge = nil -> WF (hd_red_mod E (snd R_gt)) -> WF (hd_red_mod E R).
proof: Proof. intros. unfold hd_red_mod. set (Rgt := fst R_gt) in *. set (Rge := snd R_gt) in *. apply WF_incl with (red E # @ (hd_red Rgt U hd_red Rge)). comp. incl_trans (hd_red Rgt U hd_red Rge). apply hd_rule_partition_complete. apply wf_rel_mod_simpl. fold (red_mod E Rge). hyp. apply WF_incl with (hd_red_mod (Rge ++ E) Rgt). unfold hd_red_mod. comp. apply rtc_incl. incl_trans (red Rge U red E). union. apply hd_red_incl_red. apply red_union_inv. apply ma_compat_hd_red_mod; trivial. unfold Rgt, R_gt, part_succ. apply partition_succ_compat. apply compat_app. unfold Rge, R_gt. apply partition_succeq_compat_snd. hyp. apply incl_compat with (fst E_ge ++ snd E_ge). unfold incl. intros. apply in_or_app. unfold E_ge. apply partition_complete. exact H2. rewrite H0, <- app_nil_end. unfold E_ge. apply partition_succeq_compat_fst. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)