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

f(f(x)) → f(c(f(x)))
f(f(x)) → f(d(f(x)))
g(c(x)) → x
g(d(x)) → x
g(c(h(0))) → g(d(1))
g(c(1)) → g(d(h(0)))
g(h(x)) → g(x)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(f'(x)) → f'(c'(f'(x)))
f'(f'(x)) → f'(d'(f'(x)))
g'(c'(x)) → x
g'(d'(x)) → x
g'(c'(h'(0'))) → g'(d'(1'))
g'(c'(1')) → g'(d'(h'(0')))
g'(h'(x)) → g'(x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(f'(x)) → f'(c'(f'(x)))
f'(f'(x)) → f'(d'(f'(x)))
g'(c'(x)) → x
g'(d'(x)) → x
g'(c'(h'(0'))) → g'(d'(1'))
g'(c'(1')) → g'(d'(h'(0')))
g'(h'(x)) → g'(x)

Types:
f' :: c':d':0':h':1' → c':d':0':h':1'
c' :: c':d':0':h':1' → c':d':0':h':1'
d' :: c':d':0':h':1' → c':d':0':h':1'
g' :: c':d':0':h':1' → c':d':0':h':1'
h' :: c':d':0':h':1' → c':d':0':h':1'
0' :: c':d':0':h':1'
1' :: c':d':0':h':1'
_hole_c':d':0':h':1'1 :: c':d':0':h':1'
_gen_c':d':0':h':1'2 :: Nat → c':d':0':h':1'

Heuristically decided to analyse the following defined symbols:
f', g'

Generator Equations:
_gen_c':d':0':h':1'2(0) ⇔ 1'
_gen_c':d':0':h':1'2(+(x, 1)) ⇔ c'(_gen_c':d':0':h':1'2(x))

The following defined symbols remain to be analysed:
f', g'

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

Generator Equations:
_gen_c':d':0':h':1'2(0) ⇔ 1'
_gen_c':d':0':h':1'2(+(x, 1)) ⇔ c'(_gen_c':d':0':h':1'2(x))

The following defined symbols remain to be analysed:
g'

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

Generator Equations:
_gen_c':d':0':h':1'2(0) ⇔ 1'
_gen_c':d':0':h':1'2(+(x, 1)) ⇔ c'(_gen_c':d':0':h':1'2(x))

No more defined symbols left to analyse.