Library Coq.Sets.Relations_2_facts

Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Relations_2.

Theorem Rstar_reflexive :
 forall (U:Type) (R:Relation U), Reflexive U (Rstar U R).

Theorem Rplus_contains_R :
 forall (U:Type) (R:Relation U), contains U (Rplus U R) R.

Theorem Rstar_contains_R :
 forall (U:Type) (R:Relation U), contains U (Rstar U R) R.

Theorem Rstar_contains_Rplus :
 forall (U:Type) (R:Relation U), contains U (Rstar U R) (Rplus U R).

Theorem Rstar_transitive :
 forall (U:Type) (R:Relation U), Transitive U (Rstar U R).

Theorem Rstar_cases :
 forall (U:Type) (R:Relation U) (x y:U),
   Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y).

Theorem Rstar_equiv_Rstar1 :
 forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).

Theorem Rsym_imp_Rstarsym :
 forall (U:Type) (R:Relation U), Symmetric U R -> Symmetric U (Rstar U R).

Theorem Sstar_contains_Rstar :
 forall (U:Type) (R S:Relation U),
   contains U (Rstar U S) R -> contains U (Rstar U S) (Rstar U R).

Theorem star_monotone :
 forall (U:Type) (R S:Relation U),
   contains U S R -> contains U (Rstar U S) (Rstar U R).

Theorem RstarRplus_RRstar :
 forall (U:Type) (R:Relation U) (x y z:U),
   Rstar U R x y -> Rplus U R y z -> exists u : _, R x u /\ Rstar U R u z.

Theorem Lemma1 :
 forall (U:Type) (R:Relation U),
   Strongly_confluent U R ->
   forall x b:U,
     Rstar U R x b ->
     forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z.