Certification Problem
Input (COPS 354)
The rewrite relation of the following conditional TRS is considered.
|
pos(s(0)) |
→ |
true |
|
pos(0) |
→ |
false |
|
pos(s(x)) |
→ |
true |
| pos(x) ≈ true
|
|
pos(p(x)) |
→ |
false |
| pos(x) ≈ false
|
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.