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

(0) Obligation:

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

b(f(b(x, z)), y) → f(f(f(b(z, b(y, z)))))
c(f(f(c(x, a, z))), a, y) → b(y, f(b(a, z)))
b(b(c(b(a, a), a, z), f(a)), y) → z

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(f(b(z0, z1)), z2) → f(f(f(b(z1, b(z2, z1)))))
b(b(c(b(a, a), a, z0), f(a)), z1) → z0
c(f(f(c(z0, a, z1))), a, z2) → b(z2, f(b(a, z1)))

Tuples:

B(f(b(z0, z1)), z2) → c1(B(z1, b(z2, z1)), B(z2, z1))
C(f(f(c(z0, a, z1))), a, z2) → c3(B(z2, f(b(a, z1))), B(a, z1))

S tuples:

B(f(b(z0, z1)), z2) → c1(B(z1, b(z2, z1)), B(z2, z1))
C(f(f(c(z0, a, z1))), a, z2) → c3(B(z2, f(b(a, z1))), B(a, z1))

K tuples:none
Defined Rule Symbols:

b, c

Defined Pair Symbols:

B, C

Compound Symbols:

c1, c3

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

B(f(b(z0, z1)), z2) → c1(B(z1, b(z2, z1)), B(z2, z1))
C(f(f(c(z0, a, z1))), a, z2) → c3(B(z2, f(b(a, z1))), B(a, z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

b(f(b(z0, z1)), z2) → f(f(f(b(z1, b(z2, z1)))))
b(b(c(b(a, a), a, z0), f(a)), z1) → z0
c(f(f(c(z0, a, z1))), a, z2) → b(z2, f(b(a, z1)))

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

b, c

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))