NO Non-Confluence Proof

Non-Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

a(b(x)) → b(c(x))
a(c(x)) → c(a(x))
b(b(x)) → a(c(x))
c(b(x)) → b(c(x))
c(b(x)) → c(c(x))
c(c(x)) → c(b(x))
P(x) → Q(Q(p(x)))
p(p(x)) → q(q(x))
p(Q(Q(x))) → Q(Q(p(x)))
Q(p(q(x))) → q(p(Q(x)))
q(q(p(x))) → p(q(q(x)))
q(Q(x)) → x
Q(q(x)) → x
p(P(x)) → x
P(p(x)) → 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.
a : 1 → 1
b : 1 → 1
c : 1 → 1
P : 0 → 0
Q : 0 → 0
p : 0 → 0
q : 0 → 0
The subsystem is

(1.1)

a(b(x)) → b(c(x))
a(c(x)) → c(a(x))
b(b(x)) → a(c(x))
c(b(x)) → b(c(x))
c(b(x)) → c(c(x))
c(c(x)) → c(b(x))

1.1 Non-Joinable Fork

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

t0 = a(b(b(x1845)))
→1 a(a(c(x1845)))
→1 a(c(a(x1845)))
→ε c(a(a(x1845)))
= t3

t0 = a(b(b(x1845)))
→ε b(c(b(x1845)))
→1 b(b(c(x1845)))
→ε a(c(c(x1845)))
→ε c(a(c(x1845)))
→1 c(c(a(x1845)))
→ε c(b(a(x1845)))
→ε b(c(a(x1845)))
= t7

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

Tool configuration

csi