YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

The following set of initial dependency pairs has been identified.

The dependency pairs are split into 1 component.

The 1^st component contains the pairs

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the arctic semiring over the integers

[b(x₁)]

· x₁ +

[a^#(x₁)]

· x₁ +

[a(x₁)]

· x₁ +

[c(x₁)]

· x₁ +

together with the usable rules

(w.r.t. the implicit argument filter of the reduction pair), the pairs

a^#(a(b(x0)))	→	a^#(x0)
a^#(a(b(x0)))	→	a^#(a(x0))

remain.

Using the linear polynomial interpretation over the arctic semiring over the integers

together with the usable rules

a(x0)	→	x0
a(a(b(x0)))	→	c(a(b(b(a(a(x0))))))

(w.r.t. the implicit argument filter of the reduction pair), all pairs could be removed.

There are no pairs anymore.