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

h(e(x), y) → h(d(x, y), s(y))
d(g(g(0, x), y), s(z)) → g(e(x), d(g(g(0, x), y), z))
d(g(g(0, x), y), 0) → e(y)
d(g(0, x), y) → e(x)
d(g(x, y), z) → g(d(x, z), e(y))
g(e(x), e(y)) → e(g(x, y))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: e':s':0' → e':s':0' → h'
e' :: e':s':0' → e':s':0'
d' :: e':s':0' → e':s':0' → e':s':0'
s' :: e':s':0' → e':s':0'
g' :: e':s':0' → e':s':0' → e':s':0'
0' :: e':s':0'
_hole_h'1 :: h'
_hole_e':s':0'2 :: e':s':0'
_gen_e':s':0'3 :: Nat → e':s':0'

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

They will be analysed ascendingly in the following order:
d' < h'
g' < d'

Rules:
h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: e':s':0' → e':s':0' → h'
e' :: e':s':0' → e':s':0'
d' :: e':s':0' → e':s':0' → e':s':0'
s' :: e':s':0' → e':s':0'
g' :: e':s':0' → e':s':0' → e':s':0'
0' :: e':s':0'
_hole_h'1 :: h'
_hole_e':s':0'2 :: e':s':0'
_gen_e':s':0'3 :: Nat → e':s':0'

Generator Equations:
_gen_e':s':0'3(0) ⇔ 0'
_gen_e':s':0'3(+(x, 1)) ⇔ e'(_gen_e':s':0'3(x))

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

They will be analysed ascendingly in the following order:
d' < h'
g' < d'

Proved the following rewrite lemma:
g'(_gen_e':s':0'3(+(1, _n5)), _gen_e':s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)

Induction Base:
g'(_gen_e':s':0'3(+(1, 0)), _gen_e':s':0'3(+(1, 0)))

Induction Step:
g'(_gen_e':s':0'3(+(1, +(_\$n6, 1))), _gen_e':s':0'3(+(1, +(_\$n6, 1)))) →RΩ(1)
e'(g'(_gen_e':s':0'3(+(1, _\$n6)), _gen_e':s':0'3(+(1, _\$n6)))) →IH
e'(_*4)

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

Rules:
h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: e':s':0' → e':s':0' → h'
e' :: e':s':0' → e':s':0'
d' :: e':s':0' → e':s':0' → e':s':0'
s' :: e':s':0' → e':s':0'
g' :: e':s':0' → e':s':0' → e':s':0'
0' :: e':s':0'
_hole_h'1 :: h'
_hole_e':s':0'2 :: e':s':0'
_gen_e':s':0'3 :: Nat → e':s':0'

Lemmas:
g'(_gen_e':s':0'3(+(1, _n5)), _gen_e':s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_e':s':0'3(0) ⇔ 0'
_gen_e':s':0'3(+(x, 1)) ⇔ e'(_gen_e':s':0'3(x))

The following defined symbols remain to be analysed:
d', h'

They will be analysed ascendingly in the following order:
d' < h'

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

Rules:
h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: e':s':0' → e':s':0' → h'
e' :: e':s':0' → e':s':0'
d' :: e':s':0' → e':s':0' → e':s':0'
s' :: e':s':0' → e':s':0'
g' :: e':s':0' → e':s':0' → e':s':0'
0' :: e':s':0'
_hole_h'1 :: h'
_hole_e':s':0'2 :: e':s':0'
_gen_e':s':0'3 :: Nat → e':s':0'

Lemmas:
g'(_gen_e':s':0'3(+(1, _n5)), _gen_e':s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_e':s':0'3(0) ⇔ 0'
_gen_e':s':0'3(+(x, 1)) ⇔ e'(_gen_e':s':0'3(x))

The following defined symbols remain to be analysed:
h'

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

Rules:
h'(e'(x), y) → h'(d'(x, y), s'(y))
d'(g'(g'(0', x), y), s'(z)) → g'(e'(x), d'(g'(g'(0', x), y), z))
d'(g'(g'(0', x), y), 0') → e'(y)
d'(g'(0', x), y) → e'(x)
d'(g'(x, y), z) → g'(d'(x, z), e'(y))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: e':s':0' → e':s':0' → h'
e' :: e':s':0' → e':s':0'
d' :: e':s':0' → e':s':0' → e':s':0'
s' :: e':s':0' → e':s':0'
g' :: e':s':0' → e':s':0' → e':s':0'
0' :: e':s':0'
_hole_h'1 :: h'
_hole_e':s':0'2 :: e':s':0'
_gen_e':s':0'3 :: Nat → e':s':0'

Lemmas:
g'(_gen_e':s':0'3(+(1, _n5)), _gen_e':s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)

Generator Equations:
_gen_e':s':0'3(0) ⇔ 0'
_gen_e':s':0'3(+(x, 1)) ⇔ e'(_gen_e':s':0'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
g'(_gen_e':s':0'3(+(1, _n5)), _gen_e':s':0'3(+(1, _n5))) → _*4, rt ∈ Ω(n5)