Library Coq.Sets.Relations_3


Require Export Relations_1.

Require Export Relations_2.




Section Relations_3.

      Variable U : Type.

      Variable R : Relation U.

   

   Definition coherent (x y:U) : Prop :=

      exists z : _, Rstar U R x z /\ Rstar U R y z.

   

   Definition locally_confluent (x:U) : Prop :=

     forall y z:U, R x y -> R x z -> coherent y z.

   

   Definition Locally_confluent : Prop := forall x:U, locally_confluent x.

   

   Definition confluent (x:U) : Prop :=

     forall y z:U, Rstar U R x y -> Rstar U R x z -> coherent y z.

   

   Definition Confluent : Prop := forall x:U, confluent x.

   

   Inductive noetherian : U -> Prop :=

       definition_of_noetherian :

         forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x.

   

   Definition Noetherian : Prop := forall x:U, noetherian x.

   

End Relations_3.

Hint Unfold coherent: sets v62.

Hint Unfold locally_confluent: sets v62.

Hint Unfold confluent: sets v62.

Hint Unfold Confluent: sets v62.

Hint Resolve definition_of_noetherian: sets v62.

Hint Unfold Noetherian: sets v62.
Index
This page has been generated by coqdoc