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