proposition: Lemma acyclic_du r r' adom bdom (A: doma r adom) (B: domb r bdom) : acyclic r' -> acyclic (r ∪ ⦗bdom⦘ ⨾ r'⁺ ⨾ ⦗adom⦘) -> acyclic (r ∪ r').
proof: Proof. unfold acyclic; ins. rewrite path_ur2; eauto. rewrite (unionC r), path_ur, <- (unionC r); eauto. rewrite seq_union_r, !irreflexive_union; repeat split; ins. eapply irreflexive_inclusion, H. rewrite inclusion_seq_eqv_l, inclusion_seq_eqv_r, ct_of_ct, cr_of_ct, rt_ct; auto with hahn. rewrite irreflexive_seqC, seqA, inclusion_ct_seq_eqv_l, !seqA. seq_rewrite seq_eqvK; do 2 rewrite ct_of_ct at 1. rewrite !crE, !seq_union_l, !seq_id_l, !seq_union_r, !seq_id_r. rewrite !irreflexive_union; repeat split; ins. rewrite ct_end, seqA, !seq_union_l, !seqA. rewrite <- rt_ct in H0; eapply irreflexive_inclusion, H0. eapply inclusion_seq_mon, inclusion_union_l; ins. assert (EQ: r ≡ r ⨾ eqv_rel bdom). by split; rewrite seq_eqv_r; red; ins; desf; eauto. by rewrite EQ at 1; rewrite seqA; eauto using inclusion_step2_ct with hahn. rewrite (inclusion_seq_eqv_l (dom:=adom)). by sin_rewrite ct_ct; eauto with hahn. rewrite ct_begin, irreflexive_seqC, <- !seqA, !seq_union_r, !seqA. rewrite <- ct_rt in H0; eapply irreflexive_inclusion, H0. apply inclusion_seq_mon; ins. apply inclusion_union_l; ins. assert (EQ: r ≡ eqv_rel adom ⨾ r). by split; rewrite seq_eqv_l; red; ins; desf; eauto. by rewrite EQ at 1; rewrite <- !seqA; eauto using inclusion_step2_ct with hahn. rewrite <- inclusion_union_r2. apply inclusion_step_t, inclusion_seq_mon; ins. by rewrite inclusion_seq_eqv_l; sin_rewrite ct_ct. rewrite seqA; sin_rewrite ct_ct. eapply irreflexive_inclusion, H0; eauto using inclusion_t_r_t with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath