NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

0(1(2(3(4(5(1(x)))))))	→	1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(x)))))))))))))))))))
0(1(2(3(4(5(1(x)))))))	→	1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(x)))))))))))))))))))))))))

The system is not confluent due to the following forking derivations.

t₀ = 0(1(2(3(4(5(1(y1)))))))

→_ε 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(0(1(2(3(4(5(y1)))))))))))))))))))))))))

= t₁

t₀ = 0(1(2(3(4(5(1(y1)))))))

→_ε 1(2(3(4(5(1(1(0(1(2(3(4(5(0(1(2(3(4(5(y1)))))))))))))))))))

= t₁

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.

Hakusan