The rewrite relation of the following conditional TRS is considered.
last(cons(x,y))
→
x
| y ≈ nil
last(cons(x,y))
→
z
| y ≈ cons(u,v), last(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.
last(cons(x,y))
→
x
| y ≈ nil
last(cons(x,y))
→
last(y)
| y ≈ cons(u,v)
1.1 Almost-orthogonal modulo infeasibility
The given (extended) properly oriented, right-stable, oriented 3-CTRS
is almost-orthogonal modulo infeasibility,
since all its conditional critical pairs are infeasible.
The
1st
CCP contains
the condition $2 ≈ cons(z,x')
from the first rule
and
the condition $2 ≈ nil
from the second rule.
1.1.1 Equal Left-Hand Sides
There are two conditions with left-hand side
$2
and respective right-hand sides
cons(z,x')
and
nil.
1.1.1.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.
The
2nd
CCP contains
the condition $2 ≈ nil
from the first rule
and
the condition $2 ≈ cons(y',z')
from the second rule.
1.1.2 Equal Left-Hand Sides
There are two conditions with left-hand side
$2
and respective right-hand sides
nil
and
cons(y',z').
1.1.2.1 Non-joinability by TCAP
Non-joinability is shown by the TCAP approximation.