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
(
x
:
U
) :
Prop
:=
definition_of_noetherian
:
(
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
.