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

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

Rewrite Strategy: INNERMOST


Renamed function symbols to avoid clashes with predefined symbol.


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


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

Rewrite Strategy: INNERMOST


Infered types.


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

Types:
g' :: f' → f'
f' :: f' → f' → f'
_hole_f'1 :: f'
_gen_f'2 :: Nat → f'


Heuristically decided to analyse the following defined symbols:
g'


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

Types:
g' :: f' → f'
f' :: f' → f' → f'
_hole_f'1 :: f'
_gen_f'2 :: Nat → f'

Generator Equations:
_gen_f'2(0) ⇔ _hole_f'1
_gen_f'2(+(x, 1)) ⇔ f'(_hole_f'1, _gen_f'2(x))

The following defined symbols remain to be analysed:
g'


Proved the following rewrite lemma:
g'(_gen_f'2(+(1, _n4))) → _*3, rt ∈ Ω(2n)

Induction Base:
g'(_gen_f'2(+(1, 0)))

Induction Step:
g'(_gen_f'2(+(1, +(_$n5, 1)))) →RΩ(1)
f'(f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5))))), f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5)))))) →IH
f'(f'(g'(g'(_hole_f'1)), g'(_*3)), f'(g'(g'(_hole_f'1)), g'(g'(_gen_f'2(+(1, _$n5)))))) →IH
f'(f'(g'(g'(_hole_f'1)), g'(_*3)), f'(g'(g'(_hole_f'1)), g'(_*3)))

We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)