NO Non-Confluence Proof

Non-Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

h(1(1(x))) 1(h(x))
1(1(h(b(x)))) 1(1(s(b(x))))
1(s(x)) s(1(x))
b(s(x)) b(h(x))
h(1(b(x))) t(1(1(b(x))))
1(t(x)) t(1(1(1(x))))
b(t(x)) b(h(x))

Proof

1 Non-Joinable Fork

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

t0 = h(1(1(h(b(x288)))))
1 h(1(1(s(b(x288)))))
1.1 h(1(s(1(b(x288)))))
1 h(s(1(1(b(x288)))))
= t3

t0 = h(1(1(h(b(x288)))))
ε 1(h(h(b(x288))))
= t1

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

Tool configuration

csi