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

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

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

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

Rewrite Strategy: INNERMOST

Infered types.

Rules:
c'(c'(b'(c'(x)))) → b'(a'(0', c'(x)))
c'(c'(x)) → b'(c'(b'(c'(x))))
a'(0', x) → c'(c'(x))

Types:
c' :: b' → b'
b' :: b' → b'
a' :: 0' → b' → b'
0' :: 0'
_hole_b'1 :: b'
_hole_0'2 :: 0'
_gen_b'3 :: Nat → b'

Heuristically decided to analyse the following defined symbols:
c'

Rules:
c'(c'(b'(c'(x)))) → b'(a'(0', c'(x)))
c'(c'(x)) → b'(c'(b'(c'(x))))
a'(0', x) → c'(c'(x))

Types:
c' :: b' → b'
b' :: b' → b'
a' :: 0' → b' → b'
0' :: 0'
_hole_b'1 :: b'
_hole_0'2 :: 0'
_gen_b'3 :: Nat → b'

Generator Equations:
_gen_b'3(0) ⇔ _hole_b'1
_gen_b'3(+(x, 1)) ⇔ b'(_gen_b'3(x))

The following defined symbols remain to be analysed:
c'

Could not prove a rewrite lemma for the defined symbol c'.

Rules:
c'(c'(b'(c'(x)))) → b'(a'(0', c'(x)))
c'(c'(x)) → b'(c'(b'(c'(x))))
a'(0', x) → c'(c'(x))

Types:
c' :: b' → b'
b' :: b' → b'
a' :: 0' → b' → b'
0' :: 0'
_hole_b'1 :: b'
_hole_0'2 :: 0'
_gen_b'3 :: Nat → b'

Generator Equations:
_gen_b'3(0) ⇔ _hole_b'1
_gen_b'3(+(x, 1)) ⇔ b'(_gen_b'3(x))

No more defined symbols left to analyse.