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.