YES Confluence Proof

Confluence Proof

by csi

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

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

All redundant rules that were added or removed can be simulated in 1 steps .

1.1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

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

All redundant rules that were added or removed can be simulated in 2 steps .

1.1.1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

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

All redundant rules that were added or removed can be simulated in 1 steps .

1.1.1.1 Redundant Rules Transformation

To prove that the TRS is (non-)confluent, we show (non-)confluence of the following modified system:

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

All redundant rules that were added or removed can be simulated in 2 steps .

1.1.1.1.1 Strongly closed

Confluence is proven since the TRS is strongly closed. The joins can be performed within 7 step(s).

Tool configuration

csi