Certification Problem
Input (COPS 799)
The rewrite relation of the following conditional TRS is considered.
|
g(a) |
→ |
c(b) |
| b |
→ |
f(a) |
|
f(x) |
→ |
x |
| g(x) ≈ c(y) |
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.