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

f(x, x) → f(i(x), g(g(x)))
f(x, y) → x
g(x) → i(x)
f(x, i(x)) → f(x, x)
f(i(x), i(g(x))) → a

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'

Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'

Heuristically decided to analyse the following defined symbols:
f'

Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'

Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'

Generator Equations:
_gen_i':a'2(0) ⇔ a'
_gen_i':a'2(+(x, 1)) ⇔ i'(_gen_i':a'2(x))

The following defined symbols remain to be analysed:
f'

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

Rules:
f'(x, x) → f'(i'(x), g'(g'(x)))
f'(x, y) → x
g'(x) → i'(x)
f'(x, i'(x)) → f'(x, x)
f'(i'(x), i'(g'(x))) → a'

Types:
f' :: i':a' → i':a' → i':a'
i' :: i':a' → i':a'
g' :: i':a' → i':a'
a' :: i':a'
_hole_i':a'1 :: i':a'
_gen_i':a'2 :: Nat → i':a'

Generator Equations:
_gen_i':a'2(0) ⇔ a'
_gen_i':a'2(+(x, 1)) ⇔ i'(_gen_i':a'2(x))

No more defined symbols left to analyse.