NO Non-Confluence Proof

Non-Confluence Proof

by csi

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(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(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(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(1(0(1(0(1(0(1(0(0(1(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(1(0(0(0(0(1(0(0(1(1(1(1(1(1(1(1(0(0(1(0(0(0(0(0(1(0(1(0(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(1(1(1(1(1(1(1(1(1(1(0(1(1(0(0(0(0(0(0(1(1(0(1(1(1(1(0(1(1(0(1(1(1(1(1(1(0(0(0(1(1(0(1(0(0(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(0(1(0(1(1(1(0(1(1(0(1(0(0(0(1(0(0(1(1(1(0(1(1(0(0(1(0(1(1(0(0(1(1(1(1(0(1(0(1(0(1(1(0(0(1(1(0(0(0(1(0(1(0(0(0(1(1(0(1(1(0(1(0(1(0(1(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(1(0(0(1(0(1(1(1(1(0(0(0(1(0(1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(1(1(0(0(1(1(1(1(0(0(0(0(1(1(0(0(1(0(0(1(0(0(0(1(0(1(0(1(1(1(1(1(0(0(1(1(0(0(1(0(0(1(0(0(1(0(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(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(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 Persistent Decomposition (Many-Sorted)

Non-confluence is proven, because a system induced by the sorts in the following many-sorted sort attachment is not confluent.
0 : 2 → 2
1 : 2 → 2
3 : 0 → 0
4 : 0 → 0
5 : 1 → 0
2 : 2 → 2
The subsystem is

(1.1)

0(x) 1(x)
0(0(x)) 0(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(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(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(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(1(0(1(0(1(0(1(0(0(1(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(1(0(0(0(0(1(0(0(1(1(1(1(1(1(1(1(0(0(1(0(0(0(0(0(1(0(1(0(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(1(1(1(1(1(1(1(1(1(1(0(1(1(0(0(0(0(0(0(1(1(0(1(1(1(1(0(1(1(0(1(1(1(1(1(1(0(0(0(1(1(0(1(0(0(0(x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(0(1(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(1(1(0(1(1(0(1(0(0(0(1(0(0(0(1(1(0(1(0(1(1(1(0(1(1(1(0(0(0(0(0(0(0(0(1(1(0(0(0(1(0(1(1(1(0(1(1(0(1(0(0(0(1(0(0(1(1(1(0(1(1(0(0(1(0(1(1(0(0(1(1(1(1(0(1(0(1(0(1(1(0(0(1(1(0(0(0(1(0(1(0(0(0(1(1(0(1(1(0(1(0(1(0(1(1(1(1(1(1(1(1(0(1(0(0(0(1(0(1(0(1(0(0(1(0(1(1(1(1(0(0(0(1(0(1(1(1(1(0(1(0(0(1(1(1(1(0(1(0(0(0(1(1(1(0(0(1(1(0(0(1(1(1(1(0(0(0(0(1(1(0(0(1(0(0(1(0(0(0(1(0(1(0(1(1(1(1(1(0(0(1(1(0(0(1(0(0(1(0(0(1(0(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(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(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 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(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(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(x1791))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1 2(1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(1(0(1(0(1(0(1(0(0(1(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(1(0(0(0(0(1(0(0(1(1(1(1(1(1(1(1(0(0(1(0(0(0(0(0(1(0(1(0(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(1(1(1(1(1(1(1(1(1(1(0(1(1(0(0(0(0(0(0(1(1(0(1(1(1(1(0(1(1(0(1(1(1(1(1(1(0(0(0(1(1(0(1(0(0(0(x1791)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
= 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(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(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(x1791))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
ε 1(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(1(1(0(0(0(1(1(1(1(0(0(1(0(0(0(1(1(0(1(0(0(0(0(1(0(1(0(1(0(1(0(1(0(0(1(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(0(0(0(1(0(0(0(0(1(0(0(1(1(1(1(1(1(1(1(0(0(1(0(0(0(0(0(1(0(1(0(1(1(1(0(1(1(1(1(0(0(0(1(0(0(0(0(1(0(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(0(0(0(0(1(1(0(1(1(0(1(0(0(1(1(1(1(1(1(0(0(1(0(0(0(0(0(0(1(1(1(1(1(1(1(1(1(1(1(1(0(1(1(0(0(0(0(0(0(1(1(0(1(1(1(1(0(1(1(0(1(1(1(1(1(1(0(0(0(1(1(0(1(0(0(0(2(x1791)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
= t1

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

Tool configuration

csi