NO Non-Confluence Proof

Non-Confluence Proof

by Hakusan

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Non-Joinable Fork

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

t0 = 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
→1 2(1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1(0(0(0(0(1(0(1(1(0(0(1(1(1(1(0(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(1(1(0(1(1(0(1(1(0(0(0(0(0(0(1(1(1(0(0(1(0(1(0(0(0(1(1(1(0(0(0(1(1(1(0(0(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(0(0(1(0(1(0(0(1(0(1(0(1(1(1(0(1(0(0(0(0(1(1(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(1(1(1(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(0(0(0(1(1(1(0(0(1(0(1(1(0(1(1(1(0(1(0(0(1(1(0(0(1(0(1(0(1(1(1(1(1(0(1(1(1(1(0(0(0(0(0(0(1(0(0(1(0(0(1(0(0(0(1(1(0(1(1(0(1(0(0(0(0(1(1(1(1(0(0(0(1(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
= t1

t0 = 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
→ε 1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1(0(0(0(0(1(0(1(1(0(0(1(1(1(1(0(1(0(1(1(1(1(1(1(1(0(1(0(1(0(0(1(1(0(1(1(0(1(1(0(0(0(0(0(0(1(1(1(0(0(1(0(1(0(0(0(1(1(1(0(0(0(1(1(1(0(0(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(0(0(1(0(1(0(0(1(0(1(0(1(1(1(0(1(0(0(0(0(1(1(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(1(1(1(0(0(1(1(0(0(0(0(1(0(1(0(1(1(0(1(1(0(1(1(0(0(1(1(1(1(0(1(0(0(1(0(1(0(1(0(1(0(0(1(0(0(0(0(0(0(1(0(0(1(0(1(0(1(1(0(0(0(1(1(1(0(0(1(0(1(1(0(1(1(1(0(1(0(0(1(1(0(0(1(0(1(0(1(1(1(1(1(0(1(1(1(1(0(0(0(0(0(0(1(0(0(1(0(0(1(0(0(0(1(1(0(1(1(0(1(0(0(0(0(1(1(1(1(0(0(0(1(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
= t1

The two resulting terms cannot be joined for the following reason:

Tool configuration

Hakusan