Certification Problem

Input (COPS 948)

We consider the TRS containing the following rules:

The underlying signature is as follows:

{a/1, s/1, b/1, c/1}

Prove or disprove confluence.

Yes.

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

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

Confluence is proven using the following terminating critical-pair-closing-system R:

Using the linear polynomial interpretation over the naturals

all of the following rules can be deleted.

c(s(x))

→

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

(4)

Using the linear polynomial interpretation over the naturals

all of the following rules can be deleted.

b(a(b(s(x))))	→	a(b(s(a(x))))	(2)
a(s(x))	→	s(a(x))	(1)

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a(x₁)]

· x₁ +

[b(x₁)]

· x₁ +

all of the following rules can be deleted.

a(b(a(a(x))))	→	b(a(b(a(x))))	(5)
b(a(b(b(x))))	→	a(b(a(b(x))))	(6)

There are no rules in the TRS. Hence, it is terminating.