Certification Problem
Input (COPS 388)
The rewrite relation of the following conditional TRS is considered.
add
(
x
,
0
)
→
x
add
(
x
,
s
(
y
))
→
s
(
add
(
x
,
y
))
quad
(
x
)
→
z
|
add
(
x
,
x
) ≈
y
,
add
(
y
,
y
) ≈
z
Property / Task
Prove or disprove confluence.
Answer / Result
Yes.
Proof (by ConCon @ CoCo 2020)
1 Inlining of Conditions
Inlining of conditions results in the following transformed CTRS having the same multistep rewrite relation.
add
(
x
,
0
)
→
x
add
(
x
,
s
(
y
))
→
s
(
add
(
x
,
y
))
quad
(
x
)
→
add
(
add
(
x
,
x
),
add
(
x
,
x
))
1.1 Almost-orthogonal
The given (extended) properly oriented, right-stable, oriented 3-CTRS is almost-orthogonal, since there are no conditional critical pairs.