Certification Problem
Input (COPS 343)
The rewrite relation of the following conditional TRS is considered.
|
add(x,0) |
→ |
x |
|
add(x,s(y)) |
→ |
s(z) |
| add(x,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)) |
1.1 Almost-orthogonal
The given (extended) properly oriented, right-stable, oriented 3-CTRS
is almost-orthogonal,
since there are no conditional critical pairs.