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

f(a) → b
f(c) → d
f(g(x, y)) → g(f(x), f(y))
f(h(x, y)) → g(h(y, f(x)), h(x, f(y)))
g(x, x) → h(e, 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'(a') → b'
f'(c') → d'
f'(g'(x, y)) → g'(f'(x), f'(y))
f'(h'(x, y)) → g'(h'(y, f'(x)), h'(x, f'(y)))
g'(x, x) → h'(e', x)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(a') → b'
f'(c') → d'
f'(g'(x, y)) → g'(f'(x), f'(y))
f'(h'(x, y)) → g'(h'(y, f'(x)), h'(x, f'(y)))
g'(x, x) → h'(e', x)

Types:
f' :: a':b':c':d':h':e' → a':b':c':d':h':e'
a' :: a':b':c':d':h':e'
b' :: a':b':c':d':h':e'
c' :: a':b':c':d':h':e'
d' :: a':b':c':d':h':e'
g' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
h' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
e' :: a':b':c':d':h':e'
_hole_a':b':c':d':h':e'1 :: a':b':c':d':h':e'
_gen_a':b':c':d':h':e'2 :: Nat → a':b':c':d':h':e'

Heuristically decided to analyse the following defined symbols:
f'

Rules:
f'(a') → b'
f'(c') → d'
f'(g'(x, y)) → g'(f'(x), f'(y))
f'(h'(x, y)) → g'(h'(y, f'(x)), h'(x, f'(y)))
g'(x, x) → h'(e', x)

Types:
f' :: a':b':c':d':h':e' → a':b':c':d':h':e'
a' :: a':b':c':d':h':e'
b' :: a':b':c':d':h':e'
c' :: a':b':c':d':h':e'
d' :: a':b':c':d':h':e'
g' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
h' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
e' :: a':b':c':d':h':e'
_hole_a':b':c':d':h':e'1 :: a':b':c':d':h':e'
_gen_a':b':c':d':h':e'2 :: Nat → a':b':c':d':h':e'

Generator Equations:
_gen_a':b':c':d':h':e'2(0) ⇔ a'
_gen_a':b':c':d':h':e'2(+(x, 1)) ⇔ h'(a', _gen_a':b':c':d':h':e'2(x))

The following defined symbols remain to be analysed:
f'

Proved the following rewrite lemma:
f'(_gen_a':b':c':d':h':e'2(_n4)) → _*3, rt ∈ Ω(n4)

Induction Base:
f'(_gen_a':b':c':d':h':e'2(0))

Induction Step:
f'(_gen_a':b':c':d':h':e'2(+(_$n5, 1))) →RΩ(1)
g'(h'(_gen_a':b':c':d':h':e'2(_$n5), f'(a')), h'(a', f'(_gen_a':b':c':d':h':e'2(_$n5)))) →RΩ(1)
g'(h'(_gen_a':b':c':d':h':e'2(_$n5), b'), h'(a', f'(_gen_a':b':c':d':h':e'2(_$n5)))) →IH
g'(h'(_gen_a':b':c':d':h':e'2(_$n5), b'), h'(a', _*3))

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

Rules:
f'(a') → b'
f'(c') → d'
f'(g'(x, y)) → g'(f'(x), f'(y))
f'(h'(x, y)) → g'(h'(y, f'(x)), h'(x, f'(y)))
g'(x, x) → h'(e', x)

Types:
f' :: a':b':c':d':h':e' → a':b':c':d':h':e'
a' :: a':b':c':d':h':e'
b' :: a':b':c':d':h':e'
c' :: a':b':c':d':h':e'
d' :: a':b':c':d':h':e'
g' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
h' :: a':b':c':d':h':e' → a':b':c':d':h':e' → a':b':c':d':h':e'
e' :: a':b':c':d':h':e'
_hole_a':b':c':d':h':e'1 :: a':b':c':d':h':e'
_gen_a':b':c':d':h':e'2 :: Nat → a':b':c':d':h':e'

Lemmas:
f'(_gen_a':b':c':d':h':e'2(_n4)) → _*3, rt ∈ Ω(n4)

Generator Equations:
_gen_a':b':c':d':h':e'2(0) ⇔ a'
_gen_a':b':c':d':h':e'2(+(x, 1)) ⇔ h'(a', _gen_a':b':c':d':h':e'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_a':b':c':d':h':e'2(_n4)) → _*3, rt ∈ Ω(n4)