Certification Problem
Input (COPS 266)
The rewrite relation of the following conditional TRS is considered.
|
App(App(App(S,a),b),c) |
→ |
App(App(a,c),App(b,c)) |
| a ≈ I, b ≈ I, c ≈ I
|
|
App(App(K,a),b) |
→ |
a |
| a ≈ I, b ≈ I
|
|
App(I,a) |
→ |
a |
| a ≈ I
|
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.