NO
Non-Confluence Proof
Non-Confluence Proof
by Hakusan
Input
The rewrite relation of the following TRS is considered.
b
→
f
(
h
(
f
(
f
(
b
)),
c
))
h
(
h
(
c
,
c
),
b
)
→
c
h
(
f
(
a
),
b
)
→
b
Proof
1 Non-Joinable Fork
The system is not confluent due to the following forking derivations.
t
0
=
h
(
h
(
c
,
c
),
b
)
→
2
h
(
h
(
c
,
c
),
f
(
h
(
f
(
f
(
b
)),
c
)))
=
t
1
t
0
=
h
(
h
(
c
,
c
),
b
)
→
ε
c
=
t
1
The two resulting terms cannot be joined for the following reason:
When applying the cap-function on both terms (where variables may be treated like constants) then the resulting terms do not unify.
Tool configuration
Hakusan
version: 0.10