Section Rstar.

Variable A : Type.
Variable R : A → A → Prop.

Definition Rstar (x y:A) :=
  ∀ P:A → A → Prop,
    (∀ u:A, P u u) → (∀ u v w:A, R u v → P v w → P u w) → P x y.

Theorem Rstar_reflexive : ∀ x:A, Rstar x x.
 Proof
   fun (x:A) (P:A → A → Prop) (h1:∀ u:A, P u u)
     (h2:∀ u v w:A, R u v → P v w → P u w) ⇒
     h1 x.

Theorem Rstar_R : ∀ x y z:A, R x y → Rstar y z → Rstar x z.
 Proof
   fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:A → A → Prop)
     (h1:∀ u:A, P u u) (h2:∀ u v w:A, R u v → P v w → P u w) ⇒
     h2 x y z t1 (t2 P h1 h2).

Theorem Rstar_transitive :
 ∀ x y z:A, Rstar x y → Rstar y z → Rstar x z.
 Proof
   fun (x y z:A) (h:Rstar x y) ⇒
     h (fun u v:A ⇒ Rstar v z → Rstar u z) (fun (u:A) (t:Rstar u z) ⇒ t)
       (fun (u v w:A) (t1:R u v) (t2:Rstar w z → Rstar v z)
          (t3:Rstar w z) ⇒ Rstar_R u v z t1 (t2 t3)).

Definition Rstar' (x y:A) :=
  ∀ P:A → A → Prop,
    P x x → (∀ u:A, R x u → Rstar u y → P x y) → P x y.

Theorem Rstar'_reflexive : ∀ x:A, Rstar' x x.
 Proof
   fun (x:A) (P:A → A → Prop) (h:P x x)
     (h':∀ u:A, R x u → Rstar u x → P x x) ⇒ h.

Theorem Rstar'_R : ∀ x y z:A, R x z → Rstar z y → Rstar' x y.
 Proof
   fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:A → A → Prop)
     (h1:P x x) (h2:∀ u:A, R x u → Rstar u y → P x y) ⇒
     h2 z t1 t2.

Theorem Rstar'_Rstar : ∀ x y:A, Rstar' x y → Rstar x y.
 Proof
   fun (x y:A) (h:Rstar' x y) ⇒
     h Rstar (Rstar_reflexive x) (fun u:A ⇒ Rstar_R x u y).

Theorem Rstar_Rstar' : ∀ x y:A, Rstar x y → Rstar' x y.
 Proof
   fun (x y:A) (h:Rstar x y) ⇒
     h Rstar' (fun u:A ⇒ Rstar'_reflexive u)
       (fun (u v w:A) (h1:R u v) (h2:Rstar' v w) ⇒
          Rstar'_R u w v h1 (Rstar'_Rstar v w h2)).

Definition commut (A:Set) (R1 R2:A → A → Prop) :=
  ∀ x y:A,
    R1 y x → ∀ z:A, R2 z y → exists2 y' : A, R2 y' x & R1 z y'.

End Rstar.