proposition: Lemma acyc_dom (r: relation A) d e (E1: r ⊆ (⦗d⦘ ∪ ⦗e⦘) ⨾ r ⨾ (⦗d⦘ ∪ ⦗e⦘)) (E2: ⦗d⦘ ⨾ ⦗e⦘ ⊆ ∅₂) dd (DD: dd = ⦗d⦘ ⨾ r ⨾ ⦗d⦘) de (DE: de = ⦗d⦘ ⨾ r ⨾ ⦗e⦘) ed (ED: ed = ⦗e⦘ ⨾ r ⨾ ⦗d⦘) ee (EE: ee = ⦗e⦘ ⨾ r ⨾ ⦗e⦘) (ACYCd: acyclic dd) (ACYCe: acyclic ee) (ACYCed: acyclic (ed ⨾ dd＊ ⨾ de ⨾ ee＊)) : acyclic r.
proof: Proof. red. eapply irr_dom; try edone. { arewrite (⦗d⦘ ∪ ⦗e⦘ ≡ ⦗fun x => d x \/ e x⦘) by basic_solver. apply domab_helper; split. apply ct_doma; eapply domab_helper with (d':= fun x => d x \/ e x). rewrite E1 at 1; basic_solver. apply ct_domb; eapply domab_helper with (d := fun x => d x \/ e x). rewrite E1 at 1; basic_solver. } sin_rewrite path_dom_same; try edone. { repeat rewrite irreflexive_union; splits; try done. rewrite irreflexive_seqC. arewrite( dd＊ ⨾ (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed) ⁺ ⊆ (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed) ⁺). { by rewrite ct_begin; rewrite !seqA; rels. } assert (acyclic (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed)); try done. rewrite acyclic_seqC; rewrite !seqA. rewrite acyclic_seqC; rewrite !seqA. rewrite acyclic_seqC; rewrite !seqA. done. } rewrite unionC in E1. sin_rewrite path_dom_same; try edone; try by rewrite seq_eqvC. repeat rewrite irreflexive_union; splits; try done. rewrite irreflexive_seqC. arewrite( ee＊ ⨾ (ee ＊ ⨾ ed ⨾ dd ＊ ⨾ de) ⁺ ⊆ (ee ＊ ⨾ ed ⨾ dd ＊ ⨾ de) ⁺). { by rewrite ct_begin; rewrite !seqA; rels. } assert (acyclic(ee ＊ ⨾ ed ⨾ dd ＊ ⨾ de)); try done. rewrite acyclic_seqC; rewrite !seqA. done. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid