The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
↳27 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳28 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

c(c(c(b(x)))) → a(1, b(c(x)))
b(c(b(c(x)))) → a(0, a(1, x))
a(0, x) → c(c(x))
a(1, x) → c(b(x))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, a(1, z0)), A(1, z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
S tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, a(1, z0)), A(1, z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

C, B, A

Compound Symbols:

c1, c2, c3, c4

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B(c(b(c(z0)))) → c2(A(0, a(1, z0)), A(1, z0)) by

B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
B(c(b(c(x0)))) → c2

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
B(c(b(c(x0)))) → c2
S tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
B(c(b(c(x0)))) → c2
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

C, A, B

Compound Symbols:

c1, c3, c4, c2, c2

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

B(c(b(c(x0)))) → c2

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
S tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
A(1, z0) → c4(C(b(z0)), B(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

C, A, B

Compound Symbols:

c1, c3, c4, c2

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(1, z0) → c4(C(b(z0)), B(z0)) by

A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, x0) → c4

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, x0) → c4
S tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, x0) → c4
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

C, A, B

Compound Symbols:

c1, c3, c2, c4, c4

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(1, x0) → c4

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
S tuples:

C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0))
A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

C, A, B

Compound Symbols:

c1, c3, c2, c4

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(b(z0)))) → c1(A(1, b(c(z0))), B(c(z0)), C(z0)) by

C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))), C(b(c(z0))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(x0)))) → c1

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))), C(b(c(z0))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(x0)))) → c1
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))), C(b(c(z0))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(x0)))) → c1
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c4, c1, c1

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

C(c(c(b(x0)))) → c1

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))), C(b(c(z0))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))), C(b(c(z0))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c4, c1

(15) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c4, c1, c1

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A(1, c(b(c(z0)))) → c4(C(a(0, a(1, z0))), B(c(b(c(z0))))) by

A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c1, c1, c4, c4

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

A(1, c(b(c(x0)))) → c4

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c1, c1, c4

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(b(c(c(b(z0))))))) → c1(A(1, b(a(1, b(c(z0))))), B(c(c(c(b(z0))))), C(c(c(b(z0))))) by

C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0)))))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c1, c4, c1, c1

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, a(1, z0))), B(c(b(c(z0))))) by

C(c(c(b(b(c(x0)))))) → c1(A(1, c(c(a(1, x0)))), B(c(b(c(x0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(b(c(x0)))))) → c1

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
C(c(c(b(b(c(x0)))))) → c1(A(1, c(c(a(1, x0)))), B(c(b(c(x0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(b(c(x0)))))) → c1
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
C(c(c(b(b(c(x0)))))) → c1(A(1, c(c(a(1, x0)))), B(c(b(c(x0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(b(c(x0)))))) → c1
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c4, c1, c1, c1, c1

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

C(c(c(b(b(c(x0)))))) → c1

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

c(c(c(b(z0)))) → a(1, b(c(z0)))
b(c(b(c(z0)))) → a(0, a(1, z0))
a(0, z0) → c(c(z0))
a(1, z0) → c(b(z0))
Tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
C(c(c(b(b(c(x0)))))) → c1(A(1, c(c(a(1, x0)))), B(c(b(c(x0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, c(b(z0)))), B(c(b(c(z0)))))
S tuples:

A(0, z0) → c3(C(c(z0)), C(z0))
B(c(b(c(z0)))) → c2(A(0, c(b(z0))), A(1, z0))
A(1, c(b(c(x0)))) → c4(C(c(c(a(1, x0)))), B(c(b(c(x0)))))
A(1, c(b(c(z0)))) → c4(C(a(0, c(b(z0)))), B(c(b(c(z0)))))
C(c(c(b(c(c(b(x0))))))) → c1(A(1, b(c(b(b(c(x0)))))), B(c(c(c(b(x0))))), C(c(c(b(x0)))))
C(c(c(b(c(c(b(b(c(z0))))))))) → c1(A(1, b(a(1, a(0, a(1, z0))))), B(c(c(c(b(b(c(z0))))))), C(c(c(b(b(c(z0)))))))
C(c(c(b(c(c(b(c(c(b(z0)))))))))) → c1(A(1, b(a(1, b(a(1, b(c(z0))))))), B(c(c(c(b(c(c(b(z0)))))))), C(c(c(b(c(c(b(z0))))))))
C(c(c(b(c(c(b(x0))))))) → c1(B(c(c(c(b(x0))))))
C(c(c(b(b(c(x0)))))) → c1(A(1, c(c(a(1, x0)))), B(c(b(c(x0)))))
C(c(c(b(b(c(z0)))))) → c1(A(1, a(0, c(b(z0)))), B(c(b(c(z0)))))
K tuples:none
Defined Rule Symbols:

c, b, a

Defined Pair Symbols:

A, B, C

Compound Symbols:

c3, c2, c4, c1, c1, c1

(27) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3]
transitions:
10() → 0
00() → 0
c0(0) → 1
b0(0) → 2
a0(0, 0) → 3
c1(0) → 4
c1(4) → 3
b1(0) → 5
c1(5) → 3

(28) BOUNDS(O(1), O(n^1))