Certification Problem
Input (COPS 333)
The rewrite relation of the following conditional TRS is considered.
f
(
x
)
→
g
(
x
,
y
,
z
)
|
h
(
a
,
x
) ≈
i
(
y
),
h
(
a
,
y
) ≈
i
(
z
)
h
(
a
,
a
)
→
i
(
b
)
h
(
a
,
b
)
→
i
(
c
)
h
(
b
,
b
)
→
i
(
d
)
Property / Task
Prove or disprove confluence.
Answer / Result
Yes.
Proof (by ConCon @ CoCo 2020)
1 Almost-orthogonal
The given (extended) properly oriented, right-stable, oriented 3-CTRS is almost-orthogonal, since there are no conditional critical pairs.