Certification Problem
Input (COPS 527)
The rewrite relation of the following conditional TRS is considered.
f
(
cons
(
x
,
nil
))
→
pair
(
x
,
nil
)
f
(
cons
(
x
,
cons
(
y
,
l
)))
→
pair
(
z
,
cons
(
x
,
l1
))
|
f
(
cons
(
y
,
l
)) ≈
pair
(
z
,
l1
)
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.