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 (ComplexityIfPolyImplication, 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 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
↳17 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳18 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

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

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

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

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

a, c, b

Defined Pair Symbols:

A, C

Compound Symbols:

c1, c2

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

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

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

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(z0, c(z1))) → c2(C(c(b(a(0, 0), z0))), C(b(a(0, 0), z0)), B(a(0, 0), z0), A(0, 0))
A(x0, b(z0, c(z1))) → c1(B(x0, b(0, c(c(b(a(0, 0), z0))))), B(0, c(b(z0, c(z1)))), C(b(z0, c(z1))))
A(x0, x1) → c1
S tuples:

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

a, c, b

Defined Pair Symbols:

C, A

Compound Symbols:

c2, c1, c1

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

A(x0, b(z0, c(z1))) → c1(B(x0, b(0, c(c(b(a(0, 0), z0))))), B(0, c(b(z0, c(z1)))), C(b(z0, c(z1))))
Removed 1 trailing nodes:

A(x0, x1) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(z0, c(z1))) → c2(C(c(b(a(0, 0), z0))), C(b(a(0, 0), z0)), B(a(0, 0), z0), A(0, 0))
S tuples:

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

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2

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

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

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(x0, c(x1))) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(x0, c(x1))) → c2
S tuples:

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(x0, c(x1))) → c2
K tuples:none
Defined Rule Symbols:

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

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

Removed 1 trailing nodes:

C(b(x0, c(x1))) → c2

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
S tuples:

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
K tuples:none
Defined Rule Symbols:

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2

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

Use narrowing to replace C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), a(0, 0))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0)) by

C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
S tuples:

C(b(0, c(x1))) → c2(C(c(a(0, 0))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
K tuples:none
Defined Rule Symbols:

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

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

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

C(b(0, c(x0))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(0, c(x0))) → c2(C(b(a(0, 0), 0)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
C(b(0, c(x0))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(0, c(x0))) → c2(C(b(a(0, 0), 0)))
S tuples:

C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
C(b(0, c(x0))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(0, c(x0))) → c2(C(b(a(0, 0), 0)))
K tuples:none
Defined Rule Symbols:

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2, c2

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

Use narrowing to replace C(b(x0, c(x1))) → c2(C(c(b(b(0, b(0, c(0))), x0))), C(b(a(0, 0), x0)), B(a(0, 0), x0), A(0, 0)) by

C(b(c(z1), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(z1))), B(a(0, 0), c(z1)), A(0, 0))
C(b(0, c(x1))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(x0, c(x1))) → c2(C(b(a(0, 0), x0)), B(a(0, 0), x0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
C(b(0, c(x0))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(0, c(x0))) → c2(C(b(a(0, 0), 0)))
C(b(x0, c(x1))) → c2(C(b(a(0, 0), x0)), B(a(0, 0), x0))
S tuples:

C(b(c(x0), c(x1))) → c2(C(c(c(b(a(0, 0), b(0, b(0, c(0))))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(c(c(b(b(0, b(0, c(0))), a(0, 0))))), C(b(a(0, 0), c(x0))), B(a(0, 0), c(x0)), A(0, 0))
C(b(c(x0), c(x1))) → c2(C(b(a(0, 0), c(x0))))
C(b(0, c(x0))) → c2(C(c(b(0, b(0, c(0))))), C(b(a(0, 0), 0)), B(a(0, 0), 0), A(0, 0))
C(b(0, c(x0))) → c2(C(b(a(0, 0), 0)))
C(b(x0, c(x1))) → c2(C(b(a(0, 0), x0)), B(a(0, 0), x0))
K tuples:none
Defined Rule Symbols:

a, c, b

Defined Pair Symbols:

C

Compound Symbols:

c2, c2, c2

(17) 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:
00() → 0
a0(0, 0) → 1
c0(0) → 2
b0(0, 0) → 3
01() → 5
c1(0) → 6
b1(5, 6) → 4
b1(0, 4) → 1
0 → 3

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