YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the arctic semiring over the integers
[b(x1)] =
0 -∞
0 -∞
· x1 +
-∞ -∞
-∞ -∞
[a(x1)] =
0 0
0 1
· x1 +
-∞ -∞
-∞ -∞
[c(x1)] =
0 0
1 1
· x1 +
-∞ -∞
-∞ -∞
the rules
a(a(x0)) c(b(a(b(a(x0)))))
b(a(b(x0))) b(x0)
a(a(a(x0))) c(c(a(x0)))
a(c(a(x0))) c(c(a(x0)))
c(a(c(x0))) a(a(c(x0)))
remain.

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(a(x0)) a(b(a(b(c(x0)))))
b(a(b(x0))) b(x0)
a(a(a(x0))) a(c(c(x0)))
a(c(a(x0))) a(c(c(x0)))
c(a(c(x0))) c(a(a(x0)))

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[b(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[c(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
the rules
a(a(x0)) a(b(a(b(c(x0)))))
a(a(a(x0))) a(c(c(x0)))
a(c(a(x0))) a(c(c(x0)))
c(a(c(x0))) c(a(a(x0)))
remain.

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(a(x0)) c(b(a(b(a(x0)))))
a(a(a(x0))) c(c(a(x0)))
a(c(a(x0))) c(c(a(x0)))
c(a(c(x0))) a(a(c(x0)))

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[b(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[c(x1)] =
1 0 1
0 0 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
the rules
a(a(a(x0))) c(c(a(x0)))
a(c(a(x0))) c(c(a(x0)))
c(a(c(x0))) a(a(c(x0)))
remain.

1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
a#(a(a(x0))) c#(a(x0))
a#(a(a(x0))) c#(c(a(x0)))
a#(c(a(x0))) c#(c(a(x0)))
c#(a(c(x0))) a#(a(c(x0)))

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers
[c#(x1)] = 3 · x1 + 5
[a#(x1)] = 3 · x1 + 0
[a(x1)] = 4 · x1 + 1
[c(x1)] = 4 · x1 + 5
together with the usable rules
a(a(a(x0))) c(c(a(x0)))
a(c(a(x0))) c(c(a(x0)))
c(a(c(x0))) a(a(c(x0)))
(w.r.t. the implicit argument filter of the reduction pair), the pairs
a#(a(a(x0))) c#(c(a(x0)))
a#(c(a(x0))) c#(c(a(x0)))
c#(a(c(x0))) a#(a(c(x0)))
remain.

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the arctic semiring over the integers
[c#(x1)] =
0 -∞
-∞ -∞
· x1 +
-∞ -∞
-∞ -∞
[a#(x1)] =
0 0
-∞ -∞
· x1 +
3 -∞
-∞ -∞
[a(x1)] =
0 3
1 0
· x1 +
-∞ -∞
0 -∞
[c(x1)] =
0 -∞
1 0
· x1 +
-∞ -∞
2 -∞
together with the usable rules
a(a(a(x0))) c(c(a(x0)))
a(c(a(x0))) c(c(a(x0)))
c(a(c(x0))) a(a(c(x0)))
(w.r.t. the implicit argument filter of the reduction pair), the pair
c#(a(c(x0))) a#(a(c(x0)))
remains.

1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.