proposition: Lemma acyclic_seq_union_incompat A (r r' r'' : relation A) (DISJ: r' ⨾ r'' ⊆ ∅₂) (DISJ': r'' ⨾ r' ⊆ ∅₂) (ACYC: acyclic (r ⨾ r'＊)) (ACYC': acyclic (r''⁺ ⨾ (r ⨾ r'＊)⁺)) : acyclic (r ⨾ (r' ∪ r'')＊).
proof: Proof. ins; desf. arewrite ((r' ∪ r'')＊ <<= r'＊ ∪ r''⁺). apply inclusion_rt_ind_left; ins; vauto. relsf; unionL; rels. by rewrite rt_begin at 1; relsf; sin_rewrite DISJ'; relsf. by rewrite ct_begin at 1; relsf; sin_rewrite DISJ; relsf. by arewrite (r'' <<= r''^*) at 1; relsf. relsf. red; rewrite <- ct_of_union_ct_r. apply acyclic_ut; splits; ins. apply acyclic_seqC. arewrite (r <<= (r ⨾ r'＊)⁺) by (unfolder; eauto using rt_refl, t_step). arewrite (r <<= (r ⨾ r'＊)⁺) at 1 by (unfolder; eauto using rt_refl, t_step). apply acyclic_seqC. rewrite ct_begin with (r := _ ;; r''^+); rewrite !seqA. sin_rewrite ct_ct; rewrite <- seqA, <- ct_begin; red; rels. by apply acyclic_seqC. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath