proposition: Lemma acyclic_pref_union : forall X (r r' : relation X) (dom : X -> Prop) (IRR: irreflexive r) (T: transitive r) (TOT: is_total dom r) (DL: forall x y (R: r' x y), dom x /\ ~ dom y), acyclic (pref_union r r').
proof: Proof. ins; unfold pref_union. assert (EQ: restr_rel (fun x => ~ dom x) (fun x y => r x y \/ r' x y /\ ~ r y x) ≡ restr_rel (fun x => ~ dom x) r). unfold restr_rel; split; red; ins; desf; eauto. by specialize_full DL; eauto; ins; desf. apply min_cycle with (dom := dom) (r' := r); repeat split; repeat red; ins; desf; eauto using t_step; try hahn_rewrite EQ in H; try hahn_rewrite EQ in S'; repeat match goal with | H : clos_trans _ _ _ |- _ => rewrite (clos_trans_of_transitive (transitive_restr T)) in H | H : clos_refl_trans _ _ _ |- _ => rewrite (clos_refl_trans_of_transitive (transitive_restr T)) in H | H : r' _ _ |- _ => apply DL in H; desf end; unfold restr_rel, clos_refl, seq in *; desf; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath