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.
#[global]
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.