Require Import Vbase List Relations Classical.
Set Implicit Arguments.

Definition immediate X (rel : relation X) (a b: X) :=
  rel a b ∧ (∀ c (R1: rel a c) (R2: rel c b), False).

Definition irreflexive X (rel : relation X) := ∀ x, rel x x → False.

Definition acyclic X (rel : relation X) := irreflexive (clos_trans rel).

Definition is_total X (cond: X → Prop) (rel: relation X) :=
  ∀ a (IWa: cond a)
         b (IWb: cond b) (NEQ: a ≠ b),
    rel a b ∨ rel b a.

Definition restr_subset X (cond: X → Prop) (rel rel': relation X) :=
  ∀ a (IWa: cond a)
         b (IWb: cond b) (REL: rel a b),
    rel' a b.

Definition restr_rel X (cond : X → Prop) (rel : relation X) : relation X :=
  fun a b ⇒ rel a b ∧ cond a ∧ cond b.

Definition restr_eq_rel A B (f : A → B) rel x y :=
  rel x y ∧ f x = f y.

Definition upward_closed (X: Type) (rel: relation X) (P: X → Prop) :=
  ∀ x y (REL: rel x y) (POST: P y), P x.

Definition max_elt (X: Type) (rel: relation X) (a: X) :=
  ∀ b (REL: rel a b), False.

Notation "r 'UNION1' ( a , b )" :=
  (fun x y ⇒ x = a ∧ y = b ∨ r x y) (at level 100).

Notation "a <-→ b" := (same_relation a b) (at level 110).

Definition seq (X:Type) (r1 r2 : relation X) : relation X :=
  fun x y ⇒ ∃ z, r1 x z ∧ r2 z y.

Definition clos_refl A (R: relation A) x y := x = y ∨ R x y.

Lemma r_refl A (R: relation A) x : clos_refl R x x.

Lemma r_step A (R: relation A) x y : R x y → clos_refl R x y.

Hint Immediate r_refl r_step.

Section BasicProperties.

Variable A : Type.
Variable dom : A → Prop.
Variables r r' r'' : relation A.

Lemma clos_trans_mon a b :
  clos_trans r a b →
  (∀ a b, r a b → r' a b) →
  clos_trans r' a b.

Lemma clos_refl_trans_mon a b :
  clos_refl_trans r a b →
  (∀ a b, r a b → r' a b) →
  clos_refl_trans r' a b.

Lemma clos_refl_transE a b :
  clos_refl_trans r a b ↔ a = b ∨ clos_trans r a b.

Lemma clos_trans_in_rt a b :
  clos_trans r a b → clos_refl_trans r a b.

Lemma rt_t_trans a b c :
  clos_refl_trans r a b → clos_trans r b c → clos_trans r a c.

Lemma t_rt_trans a b c :
  clos_trans r a b → clos_refl_trans r b c → clos_trans r a c.

Lemma t_step_rt x y :
  clos_trans r x y ↔ ∃ z, r x z ∧ clos_refl_trans r z y.

Lemma t_rt_step x y :
  clos_trans r x y ↔ ∃ z, clos_refl_trans r x z ∧ r z y.

Lemma clos_trans_of_transitive (T: transitive r) x y :
  clos_trans r x y → r x y.

Lemma ct_of_transitive (T: transitive r) x y :
  clos_trans r x y ↔ r x y.

Lemma crt_of_transitive (T: transitive r) x y :
  clos_refl_trans r x y ↔ clos_refl r x y.

Lemma clos_trans_eq :
  ∀ B (f : A → B)
    (H: ∀ a b (SB: r a b), f a = f b) a b
    (C: clos_trans r a b),
  f a = f b.

Lemma trans_irr_acyclic :
  irreflexive r → transitive r → acyclic r.

Lemma restr_rel_trans :
  transitive r → transitive (restr_rel dom r).

Lemma upward_clos_trans P :
  upward_closed r P → upward_closed (clos_trans r) P.

Lemma max_elt_clos_trans a b:
  max_elt r a → clos_trans r a b → False.

Lemma is_total_restr :
  is_total dom r →
  is_total dom (restr_rel dom r).

Lemma clos_trans_restrD f x y :
  clos_trans (restr_rel f r) x y → f x ∧ f y.

Lemma clos_trans_restr_eqD B (f: A → B) x y :
  clos_trans (restr_eq_rel f r) x y → f x = f y.

Lemma irreflexive_inclusion:
  inclusion r r' →
  irreflexive r' →
  irreflexive r.

Lemma irreflexive_union :
  irreflexive (union r r') ↔ irreflexive r ∧ irreflexive r'.

Lemma irreflexive_seqC :
  irreflexive (seq r r') ↔ irreflexive (seq r' r).

Lemma clos_trans_inclusion :
  inclusion r (clos_trans r).

Lemma clos_trans_inclusion_clos_refl_trans:
  inclusion (clos_trans r) (clos_refl_trans r).

Lemma clos_trans_monotonic :
  inclusion r r' →
  inclusion (clos_trans r) (clos_trans r').

Lemma inclusion_seq_trans t :
  transitive t →
  inclusion r t →
  inclusion r' t →
  inclusion (seq r r') t.

Lemma inclusion_seq_rt :
  inclusion r (clos_refl_trans r'') →
  inclusion r' (clos_refl_trans r'') →
  inclusion (seq r r') (clos_refl_trans r'').

Lemma inclusion_union_l :
  inclusion r r'' →
  inclusion r' r'' →
  inclusion (union r r') r''.

Lemma inclusion_union_r :
  inclusion r r' ∨ inclusion r r'' →
  inclusion r (union r' r'').

Lemma inclusion_step_rt :
  inclusion r r' →
  inclusion r (clos_refl_trans r').

Lemma inclusion_r_rt :
  inclusion r r' →
  inclusion (clos_refl r) (clos_refl_trans r').

Lemma inclusion_rt_rt :
  inclusion r r' →
  inclusion (clos_refl_trans r) (clos_refl_trans r').

Lemma inclusion_step_t :
  inclusion r r' →
  inclusion r (clos_trans r').

Lemma inclusion_t_t :
  inclusion r r' →
  inclusion (clos_trans r) (clos_trans r').

Lemma inclusion_acyclic :
  inclusion r r' →
  acyclic r' →
  acyclic r.

End BasicProperties.

Lemma clos_trans_of_clos_trans1 A (r r' : relation A) x y :
  clos_trans (fun a b ⇒ clos_trans r a b ∨ r' a b) x y ↔
  clos_trans (fun a b ⇒ r a b ∨ r' a b) x y.

Lemma clos_trans_of_clos_trans A (r : relation A) x y :
  clos_trans (clos_trans r) x y ↔
  clos_trans r x y.

Lemma inclusion_union :
  ∀ {A : Type} (R1 R1' R2 R2' : relation A)
         (HINC1 : inclusion R1' R1)
         (HINC2 : inclusion R2' R2),
    inclusion (union R2' R1') (union R2 R1).

Lemma inclusion_restr_rel_l :
  ∀ {A : Type} (dom : A → Prop) (R1 R1' : relation A)
         (HINC: inclusion R1' R1),
    inclusion (restr_rel dom R1') R1.

Lemma inclusion_seq_refl :
  ∀ (A : Type) (R1 R2 R3 : relation A)
         (INC1: inclusion R1 R3)
         (INC2: inclusion R2 R3)
         (TRANS: transitive R3),
    inclusion (seq R1 (clos_refl R2)) R3.

Lemma inclusion_rt_l X (r r' : relation X) :
   reflexive r' →
   inclusion (seq r r') r' →
   inclusion (clos_refl_trans r) r'.

Lemma inclusion_rt_rt2 :
  ∀ (A : Type) (r t : relation A),
  inclusion r (clos_refl_trans t) →
  inclusion (clos_refl_trans r) (clos_refl_trans t).

Hint Resolve
     inclusion_acyclic inclusion_restr_rel_l
     inclusion_step_t inclusion_union_r inclusion_union
     inclusion_seq_refl : inclusion.

Hint Resolve inclusion_rt_rt inclusion_r_rt inclusion_step_rt : inclusion.

Require Import Setoid.

Lemma same_relation_refl A : reflexive (@same_relation A).

Lemma same_relation_sym A : symmetric (@same_relation A).

Lemma same_relation_trans A : transitive (@same_relation A).

Add Parametric Relation (X : Type) : (relation X) (@same_relation X)
 reflexivity proved by (@same_relation_refl X)
 symmetry proved by (@same_relation_sym X)
 transitivity proved by (@same_relation_trans X)
 as same_rel.

Add Parametric Morphism X : (@inclusion X) with
  signature same_relation ⇒ same_relation ⇒ iff as inclusion_mor.

Add Parametric Morphism X : (@union X) with
  signature same_relation ⇒ same_relation ⇒ same_relation as union_mor.

Add Parametric Morphism X : (@seq X) with
  signature same_relation ⇒ same_relation ⇒ same_relation as seq_mor.

Add Parametric Morphism X P : (@restr_rel X P) with
  signature same_relation ⇒ same_relation as restr_rel_mor.

Add Parametric Morphism X : (@clos_trans X) with
  signature same_relation ⇒ same_relation as clos_trans_mor.

Add Parametric Morphism X : (@clos_refl_trans X) with
  signature same_relation ⇒ same_relation as clos_relf_trans_mor.

Add Parametric Morphism X : (@clos_refl X) with
  signature same_relation ⇒ same_relation as clos_relf_mor.

Add Parametric Morphism X : (@irreflexive X) with
  signature same_relation ⇒ iff as irreflexive_mor.

Add Parametric Morphism X : (@acyclic X) with
  signature same_relation ⇒ iff as acyclic_mor.

Add Parametric Morphism X : (@clos_trans X) with
  signature same_relation ⇒ eq ⇒ eq ⇒ iff
      as clos_trans_mor'.

Add Parametric Morphism X : (@clos_refl_trans X) with
  signature same_relation ⇒ eq ⇒ eq ⇒ iff
      as clos_refl_trans_mor'.

Lemma same_relation_restr X (f : X → Prop) rel rel' :
   (∀ x (CONDx: f x) y (CONDy: f y), rel x y ↔ rel' x y) →
   (restr_rel f rel ↔ restr_rel f rel').

Lemma union_restr X (f : X → Prop) rel rel' :
  union (restr_rel f rel) (restr_rel f rel')
  ↔ restr_rel f (union rel rel').

Lemma clos_trans_restr X (f : X → Prop) rel (UC: upward_closed rel f) :
  clos_trans (restr_rel f rel)
  ↔ restr_rel f (clos_trans rel).

Lemma seq_union_l X (r1 r2 r : relation X) :
  seq (union r1 r2) r ↔ union (seq r1 r) (seq r2 r).

Lemma seq_union_r X (r r1 r2 : relation X) :
  seq r (union r1 r2) ↔ union (seq r r1) (seq r r2).

Lemma seqA X (r1 r2 r3 : relation X) :
  seq (seq r1 r2) r3 ↔ seq r1 (seq r2 r3).

Lemma unionA X (r1 r2 r3 : relation X) :
  union (union r1 r2) r3 ↔ union r1 (union r2 r3).

Lemma unionC X (r1 r2 : relation X) :
  union r1 r2 ↔ union r2 r1.

Lemma rtE_left X (r r' : relation X) :
  seq r (clos_refl_trans r') ↔ union r (seq (seq r r') (clos_refl_trans r')).

Lemma rtE_right X (r r' : relation X) :
  seq (clos_refl_trans r') r ↔ union r (seq (clos_refl_trans r') (seq r' r)).

Lemma t_step_rt2 X (r : relation X) :
  clos_trans r ↔ seq r (clos_refl_trans r).

Lemma seqFr X (r : relation X) :
  seq (fun _ _ ⇒ False) r ↔ (fun _ _ ⇒ False).

Lemma seqrF X (r : relation X) :
  seq r (fun _ _ ⇒ False) ↔ (fun _ _ ⇒ False).

Lemma unionrF X (r : relation X) :
  union r (fun _ _ ⇒ False) ↔ r.

Lemma unionFr X (r : relation X) :
  union (fun _ _ ⇒ False) r ↔ r.

Lemma crt_seq_swap X (r r' : relation X) :
  seq (clos_refl_trans (seq r r')) r ↔
  seq r (clos_refl_trans (seq r' r)).

Lemma crt_double X (r : relation X) :
  clos_refl_trans r ↔
  seq (clos_refl r) (clos_refl_trans (seq r r)).

Hint Rewrite seqFr seqrF unionrF unionFr : samerel.

Lemma min_cycle X (rel rel' : relation X) (dom : X → Prop)
    (TOT: is_total dom rel')
    (T : transitive rel')
    (INCL: inclusion rel' (clos_trans rel))
    (INV: ∀ a b (R: rel a b) (R': rel' b a), False) :
    acyclic rel ↔
    acyclic (restr_rel (fun x ⇒ ¬ dom x) rel) ∧
    (∀ x (CYC: rel x x) (D: dom x), False) ∧
    (∀ c1 b1 (R: rel c1 b1) b2
       (S : clos_refl rel' b1 b2) c2
       (R': rel b2 c2) (S': clos_refl_trans (restr_rel (fun x ⇒ ¬ dom x) rel) c2 c1)
       (D1 : dom b1) (D2: dom b2) (ND1: ¬ dom c1) (ND2: ¬ dom c2), False).

Lemma path_decomp_u1 X (rel : relation X) a b c d :
  clos_trans (rel UNION1 (a, b)) c d →
  clos_trans rel c d ∨
  clos_refl_trans rel c a ∧ clos_refl_trans rel b d.

Lemma cycle_decomp_u1 X (rel : relation X) a b c :
  clos_trans (rel UNION1 (a, b)) c c →
  clos_trans rel c c ∨ clos_refl_trans rel b a.

Lemma path_decomp_u_total :
  ∀ X (rel1 : relation X) dom rel2 (T: is_total dom rel2)
    (D: ∀ a b (REL: rel2 a b), dom a ∧ dom b) x y
    (C: clos_trans (fun a b ⇒ rel1 a b ∨ rel2 a b) x y),
    clos_trans rel1 x y ∨
    (∃ m n,
      clos_refl_trans rel1 x m ∧ clos_trans rel2 m n ∧ clos_refl_trans rel1 n y) ∨
    (∃ m n,
      clos_refl_trans rel1 m n ∧ clos_trans rel2 n m).

Lemma cycle_decomp_u_total :
  ∀ X (rel1 : relation X) dom rel2 (T: is_total dom rel2)
    (D: ∀ a b (REL: rel2 a b), dom a ∧ dom b) x
    (C: clos_trans (fun a b ⇒ rel1 a b ∨ rel2 a b) x x),
    clos_trans rel1 x x ∨
    (∃ m n, clos_refl_trans rel1 m n ∧ clos_trans rel2 n m).

Lemma clos_trans_disj_rel :
  ∀ X (rel rel' : relation X)
    (DISJ: ∀ x y (R: rel x y) z (R': rel' y z), False) x y
    (R: clos_trans rel x y) z
    (R': clos_trans rel' y z),
    False.

Lemma path_decomp_u_1 :
  ∀ X (rel rel' : relation X)
    (DISJ: ∀ x y (R: rel x y) z (R': rel' y z), False) x y
    (T: clos_trans (union rel rel') x y),
    clos_trans rel x y ∨ clos_trans rel' x y
    ∨ ∃ z, clos_trans rel' x z ∧ clos_trans rel z y.

Lemma cycle_decomp_u_1 :
  ∀ X (rel rel' : relation X)
    (DISJ: ∀ x y (R: rel x y) z (R': rel' y z), False) x
    (T: clos_trans (union rel rel') x x),
    clos_trans rel x x ∨ clos_trans rel' x x.

Lemma cycle_disj :
  ∀ X (rel : relation X)
    (DISJ: ∀ x y (R: rel x y) z (R': rel y z), False) x
    (T: clos_trans rel x x), False.

Lemma clos_trans_restr_trans_mid :
  ∀ X (rel rel' : relation X) f x y
    (A : clos_trans (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x y)
    z (B : rel y z) w
    (C : clos_trans (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) z w),
    clos_trans (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x w.

Lemma clos_trans_restr_trans_cycle :
  ∀ X (rel rel' : relation X) f x y
    (A : clos_trans (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x y)
    (B : rel y x),
    clos_trans (restr_rel f (fun x y ⇒ rel x y ∨ rel' x y)) x x.

Lemma path_tur :
  ∀ X (r r' : relation X) (adom bdom : X → Prop)
         (T: transitive r)
         (A: ∀ x y (R: r' x y), adom x)
         (B: ∀ x y (R: r' x y), bdom y) x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    r x y ∨
    ∃ z,
      clos_trans (fun x y ⇒ r x y ∧ adom y ∨ r' x y) x z ∧
      (z = y ∨ r z y ∧ bdom z).

Lemma path_ur :
  ∀ X (r r' : relation X) (adom bdom : X → Prop)
         (A: ∀ x y (R: r' x y), adom x)
         (B: ∀ x y (R: r' x y), bdom y) x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    clos_trans r x y ∨
    ∃ z,
      clos_trans (fun x y ⇒ clos_trans r x y ∧ adom y ∨ r' x y) x z ∧
      (z = y ∨ clos_trans r z y ∧ bdom z).

Lemma path_tur2 :
  ∀ X (r r' : relation X) (adom bdom : X → Prop)
         (T: transitive r')
         (A: ∀ x y (R: r x y), adom x)
         (B: ∀ x y (R: r x y), bdom y) x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    r' x y ∨
    ∃ z,
      (x = z ∨ r' x z ∧ adom z) ∧
      clos_trans (fun x y ⇒ r x y ∨ r' x y ∧ bdom x) z y.

Lemma path_ur2 :
  ∀ X (r r' : relation X) (adom bdom : X → Prop)
         (A: ∀ x y (R: r x y), adom x)
         (B: ∀ x y (R: r x y), bdom y) x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    clos_trans r' x y ∨
    ∃ z,
      (x = z ∨ clos_trans r' x z ∧ adom z) ∧
      clos_trans (fun x y ⇒ r x y ∨ clos_trans r' x y ∧ bdom x) z y.

Lemma cycle_ur :
  ∀ X (r r' : relation X) (adom : X → Prop)
         (A: ∀ x y (R: r x y), adom x)
         (B: ∀ x y (R: r x y), adom y) x
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x x),
    clos_trans r' x x ∨
    ∃ x,
      clos_trans (fun x y ⇒ r x y ∨ clos_trans r' x y ∧ adom x ∧ adom y) x x.

Lemma restr_eq_union :
  ∀ X (rel rel' : relation X) B (f: X → B) x y
         (R: ∀ x y, rel' x y → f x = f y),
   restr_eq_rel f (fun x y ⇒ rel x y ∨ rel' x y) x y ↔
   restr_eq_rel f rel x y ∨ rel' x y.

Lemma clos_trans_restr_eq_union :
  ∀ X (rel rel' : relation X) B (f: X → B)
         (R: ∀ x y, rel' x y → f x = f y),
   clos_trans (restr_eq_rel f (fun x y ⇒ rel x y ∨ rel' x y)) ↔
   clos_trans (fun x y ⇒ restr_eq_rel f rel x y ∨ rel' x y).

Lemma acyclic_mon X (rel rel' : relation X) :
  acyclic rel → inclusion rel' rel → acyclic rel'.

Section one_extension.

  Variable X : Type.
  Variable elem : X.
  Variable rel : relation X.

  Definition one_ext : relation X :=
    fun x y ⇒
      clos_trans rel x y
      ∨ clos_refl_trans rel x elem ∧ ¬ clos_refl_trans rel y elem.

  Lemma one_ext_extends x y : rel x y → one_ext x y.

  Lemma one_ext_trans : transitive one_ext.

  Lemma one_ext_irr : acyclic rel → irreflexive one_ext.

  Lemma one_ext_total_elem :
    ∀ x, x ≠ elem → one_ext elem x ∨ one_ext x elem.

End one_extension.

Fixpoint tot_ext X (dom : list X) (rel : relation X) : relation X :=
  match dom with
    | nil ⇒ clos_trans rel
    | x::l ⇒ one_ext x (tot_ext l rel)
  end.

Lemma tot_ext_extends :
  ∀ X dom (rel : relation X) x y, rel x y → tot_ext dom rel x y.

Lemma tot_ext_trans X dom (rel : relation X) : transitive (tot_ext dom rel).

Lemma tot_ext_irr :
  ∀ X (dom : list X) rel, acyclic rel → irreflexive (tot_ext dom rel).

Lemma tot_ext_total :
  ∀ X (dom : list X) rel, is_total (fun x ⇒ In x dom) (tot_ext dom rel).

Lemma tot_ext_inv :
  ∀ X dom rel (x y : X),
    acyclic rel → tot_ext dom rel x y → ¬ rel y x.

Lemma clos_trans_imm :
  ∀ X (R : relation X) (I: irreflexive R)
         (T: transitive R) L (ND: NoDup L) a b
         (D: ∀ c, R a c → R c b → In c L)
         (REL: R a b),
    clos_trans (immediate R) a b.

Definition pref_union X (r r' : relation X) x y :=
  r x y ∨ r' x y ∧ ¬ r y x.

Lemma acyclic_pref_union :
  ∀ X (r r' : relation X) (dom : X → Prop)
         (IRR: irreflexive r)
         (T: transitive r)
         (TOT: is_total dom r)
         (DL: ∀ x y (R: r' x y), dom x ∧ ¬ dom y),
    acyclic (pref_union r r').

Lemma in_pref_union :
  ∀ X (r r' : relation X) (dom : X → Prop)
         (IRR: irreflexive r)
         (T: transitive r)
         (TOT: is_total dom r)
         (DL: ∀ x y (R: r' x y), dom x ∧ ¬ dom y) x y
         (R: clos_trans (pref_union r r') x y)
         (D: dom y),
    r x y.

Fixpoint undup A dec (l: list A) :=
  match l with nil ⇒ nil
    | x :: l ⇒
      if In_dec dec x l then undup dec l else x :: undup dec l
  end.

Lemma In_undup X dec (x: X) l : In x (undup dec l) ↔ In x l.

Lemma NoDup_undup X dec (l : list X) : NoDup (undup dec l).

Lemma clos_trans_imm2 :
  ∀ X (dec : ∀ x y : X, {x = y} + {x ≠ y})
         (R : relation X) (I: irreflexive R)
         (T: transitive R) L a b
         (D: ∀ c, R a c → R c b → In c L)
         (REL: R a b),
    clos_trans (immediate R) a b.

Lemma total_immediate_unique:
  ∀ X (eq_X_dec: ∀ (x y: X), {x=y} + {x≠y}) (rel: X → X → Prop) (P: X → Prop)
         (Tot: is_total P rel)
         a b c (pa: P a) (pb: P b) (pc: P c)
         (iac: immediate rel a c)
         (ibc: immediate rel b c),
    a = b.

Lemma path_ut :
  ∀ X (r r' : relation X) (T: transitive r') x y
    (P: clos_refl_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    ∃ z w,
      clos_refl_trans r x z ∧
      clos_refl_trans (fun x y ⇒ ∃ z, r' x z ∧ clos_trans r z y) z w ∧
      (w = y ∨ r' w y).

Lemma path_ut2 :
  ∀ X (r r' : relation X) (T: transitive r') x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    clos_trans r x y ∨
    ∃ z w w',
      clos_refl_trans r x z ∧
      clos_refl_trans (fun x y ⇒ ∃ z, r' x z ∧ clos_trans r z y) z w ∧
      r' w w' ∧
      clos_refl_trans r w' y.

Lemma path_utd :
  ∀ X (r r' : relation X) (T: transitive r') dom
         (F: is_total dom r')
         (R: ∀ a b, r' a b → dom a ∧ dom b) x y
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x y),
    clos_trans r x y ∨
    (∃ z w, clos_refl_trans r x z ∧ r' z w ∧ clos_refl_trans r w y) ∨
    (∃ z w, r' z w ∧ clos_refl_trans r w z).

Lemma cycle_utd :
  ∀ X (r: relation X) (A: acyclic r)
         r' (T: transitive r') (IRR: irreflexive r') dom
         (F: is_total dom r')
         (R: ∀ a b, r' a b → dom a ∧ dom b) x
    (P: clos_trans (fun x y ⇒ r x y ∨ r' x y) x x),
  ∃ z w, r' z w ∧ clos_trans r w z.

Notation "P +++ Q" := (union P Q) (at level 50, left associativity).

Lemma acyclic_case_split A (R : relation A) f :
  acyclic R ↔
  acyclic (restr_rel f R) ∧ (∀ x (NEG: ¬ f x) (CYC: clos_trans R x x), False).

Lemma seqA2 X (r r' r'' : relation X) x y :
  seq (seq r r') r'' x y ↔ seq r (seq r' r'') x y.

Lemma path_unc X (r r' : relation X)
  (A: seq r r ↔ (fun x y ⇒ False))
  (B: seq r' r' ↔ (fun x y ⇒ False)) :
  clos_refl_trans (union r r') ↔
  clos_refl_trans (seq r r') +++
  (clos_refl_trans (seq r' r) +++
   (seq r (clos_refl_trans (seq r' r)) +++
    seq r' (clos_refl_trans (seq r r')))).

Lemma pathp_unc X (r r' : relation X)
  (A: seq r r ↔ (fun x y ⇒ False))
  (B: seq r' r' ↔ (fun x y ⇒ False)) :
  clos_trans (union r r') ↔
  clos_trans (seq r r') +++
  (clos_trans (seq r' r) +++
   (seq r (clos_refl_trans (seq r' r)) +++
    seq r' (clos_refl_trans (seq r r')))).

Lemma acyclic_unc X (r r' : relation X)
  (A: seq r r ↔ (fun x y ⇒ False))
  (B: seq r' r' ↔ (fun x y ⇒ False)) :
  acyclic (union r r') ↔ acyclic (seq r r').