Library Coq.Sets.Relations_3_facts
Require
Export
Relations_1
.
Require
Export
Relations_1_facts
.
Require
Export
Relations_2
.
Require
Export
Relations_2_facts
.
Require
Export
Relations_3
.
Theorem
Rstar_imp_coherent
:
forall
(
U
:
Type
) (
R
:
Relation
U
) (
x
y
:
U
),
Rstar
U
R
x
y
->
coherent
U
R
x
y
.
Hint Resolve
Rstar_imp_coherent
:
core
.
Theorem
coherent_symmetric
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Symmetric
U
(
coherent
U
R
).
Theorem
Strong_confluence
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Strongly_confluent
U
R
->
Confluent
U
R
.
Theorem
Strong_confluence_direct
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Strongly_confluent
U
R
->
Confluent
U
R
.
Theorem
Noetherian_contains_Noetherian
:
forall
(
U
:
Type
) (
R
R'
:
Relation
U
),
Noetherian
U
R
->
contains
U
R
R'
->
Noetherian
U
R'
.
Theorem
Newman
:
forall
(
U
:
Type
) (
R
:
Relation
U
),
Noetherian
U
R
->
Locally_confluent
U
R
->
Confluent
U
R
.