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.