Certification Problem
Input (COPS 441)
The rewrite relation of the following conditional TRS is considered.
f
(
c
(
x
),
c
(
c
(
y
)))
→
a
(
a
(
x
))
|
c
(
f
(
x
,
y
)) ≈
c
(
a
(
b
))
f
(
c
(
c
(
c
(
x
))),
y
)
→
a
(
y
)
|
c
(
f
(
c
(
x
),
c
(
c
(
y
)))) ≈
c
(
a
(
a
(
b
)))
a
(
x
)
→
b
a
(
x
)
→
f
(
x
,
x
)
Property / Task
Prove or disprove confluence.
Answer / Result
No.
Proof (by ConCon @ CoCo 2020)
1 Non-Joinable Fork
The system is not confluent due to the following forking derivations.
a
(
z
)
→
*
b
a
(
z
)
→
*
f
(
z
,
z
)
The two resulting terms cannot be joined for the following reason:
The terms are distinct normal forms.