proposition: Lemma path_dom (E1: r ⊆ (⦗d⦘ ∪ ⦗d'⦘) ⨾ r ⨾ (⦗d⦘ ∪ ⦗d'⦘)) (E2: ⦗d⦘ ⨾ ⦗d'⦘ ⊆ ∅₂) dd (DD: dd = ⦗d⦘ ⨾ r ⨾ ⦗d⦘) de (DE: de = ⦗d⦘ ⨾ r ⨾ ⦗d'⦘) ed (ED: ed = ⦗d'⦘ ⨾ r ⨾ ⦗d⦘) ee (EE: ee = ⦗d'⦘ ⨾ r ⨾ ⦗d'⦘) : r⁺ ⊆ (dd⁺ ∪ (dd＊ ⨾ de ⨾ ee＊ ⨾ ed)⁺ ⨾ dd＊ ) ∪ (ee⁺ ∪ (ee＊ ⨾ ed ⨾ dd＊ ⨾ de)⁺ ⨾ ee＊ ) ∪ (ee＊ ⨾ ed ⨾ dd＊ ⨾ de)＊ ⨾ ee＊ ⨾ ed ⨾ dd＊ ∪ (dd＊ ⨾ de ⨾ ee＊ ⨾ ed)＊ ⨾ dd＊ ⨾ de ⨾ ee＊.
proof: Proof. apply inclusion_t_ind_right. { rewrite step_dom at 1; try eassumption. repeat apply inclusion_union_l; rewrite ?seqA. 1,4: sin_rewrite !ct_end. all: try (repeat (apply inclusion_union_r; constructor); basic_solver 14). } rewrite step_dom at 1; try eassumption. relsf. assert (E2': ⦗d'⦘ ⨾ ⦗d⦘ ⊆ (fun _ _ : A => False)). { by rewrite seq_eqvC in E2. } assert (X17: ed ⨾ ed ⊆ ∅₂). { rewrite ?DD, ?ED, ?DE, ?EE; generalize E2; basic_solver. } assert (X18: ed ⨾ ee ⊆ ∅₂). { rewrite ?DD, ?ED, ?DE, ?EE; generalize E2; basic_solver. } assert (X19: de ⨾ dd ⊆ ∅₂). { rewrite ?DD, ?ED, ?DE, ?EE; generalize E2; basic_solver. } assert (X20: de ⨾ de ⊆ ∅₂). { by rewrite ?DD, ?ED, ?DE, ?EE; generalize E2; basic_solver. } assert (X1: dd ＊ ⨾ ed ⊆ ed). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X2: dd ＊ ⨾ dd ⊆ dd＊ ). { by rewrite rt_end at 2; relsf. } assert (X3: dd ＊ ⨾ ee ⊆ ee). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X4: ee ＊ ⨾ de ⊆ de). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X5: ee ＊ ⨾ ee ⊆ ee＊ ). { by rewrite rt_end at 2; relsf. } assert (X6: ee ＊ ⨾ dd ⊆ dd). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X7: dd ⁺ ⨾ dd ⊆ dd⁺). { by rewrite ct_end at 2; rewrite inclusion_t_rt. } assert (X8: dd ⁺ ⨾ ed ⊆ ∅₂). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X9: dd ⁺ ⨾ ee ⊆ ∅₂). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X10: (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed) ⁺ ⨾ ed ⊆ ∅₂). { by rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X11: (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed) ⁺ ⨾ ee ⊆ ∅₂). { by rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X12: ee ⁺ ⨾ dd ⊆ ∅₂). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X13: ee ⁺ ⨾ de ⊆ ∅₂). { by rewrite ?rtE; relsf; rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X14: ee ⁺ ⨾ ee ⊆ ee⁺). { by rewrite ct_end at 2; rewrite inclusion_t_rt. } assert (X15: (ee ＊ ⨾ ed ⨾ dd ＊ ⨾ de) ⁺ ⨾ dd ⊆ ∅₂). { by rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } assert (X16: (ee ＊ ⨾ ed ⨾ dd ＊ ⨾ de) ⁺ ⨾ de ⊆ ∅₂). { by rewrite ct_end, ?seqA, ?DD, ?ED, ?DE, ?EE, ?seqA; try sin_rewrite E2; try sin_rewrite E2'; relsf. } repeat apply inclusion_union_l; rewrite ?seqA. all: rewrite ?X1, ?X2, ?X3, ?X4, ?X5, ?X6, ?X7, ?X8, ?X9, ?X10, ?X11, ?X12, ?X13, ?X14, ?X15, ?X16, ?X17, ?X18, ?X19, ?X20. all: rels. all: try (repeat (apply inclusion_union_r; constructor); basic_solver 5). all: try (repeat (apply inclusion_union_r; constructor); basic_solver 20). Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid