Library Coq.Sets.Relations_2
Require
Export
Relations_1
.
Section
Relations_2
.
Variable
U
:
Type
.
Variable
R
:
Relation
U
.
Inductive
Rstar
(
x
:
U
) :
U
->
Prop
:=
|
Rstar_0
:
Rstar
x
x
|
Rstar_n
:
forall
y
z
:
U
,
R
x
y
->
Rstar
y
z
->
Rstar
x
z
.
Inductive
Rstar1
(
x
:
U
) :
U
->
Prop
:=
|
Rstar1_0
:
Rstar1
x
x
|
Rstar1_1
:
forall
y
:
U
,
R
x
y
->
Rstar1
x
y
|
Rstar1_n
:
forall
y
z
:
U
,
Rstar1
x
y
->
Rstar1
y
z
->
Rstar1
x
z
.
Inductive
Rplus
(
x
:
U
) :
U
->
Prop
:=
|
Rplus_0
:
forall
y
:
U
,
R
x
y
->
Rplus
x
y
|
Rplus_n
:
forall
y
z
:
U
,
R
x
y
->
Rplus
y
z
->
Rplus
x
z
.
Definition
Strongly_confluent
:
Prop
:=
forall
x
a
b
:
U
,
R
x
a
->
R
x
b
->
ex
(
fun
z
:
U
=>
R
a
z
/\
R
b
z
).
End
Relations_2
.
Hint Resolve
Rstar_0
:
sets
.
Hint Resolve
Rstar1_0
:
sets
.
Hint Resolve
Rstar1_1
:
sets
.
Hint Resolve
Rplus_0
:
sets
.