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

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

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
h' :: c' → e':0' → h'
e' :: e':0' → e':0'
c' :: c' → c'
d' :: c' → e':0' → e':0'
g' :: e':0' → e':0' → e':0'
0' :: e':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_e':0'3 :: e':0'
_gen_c'4 :: Nat → c'
_gen_e':0'5 :: Nat → e':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'(z, e'(x)) → h'(c'(z), d'(z, x))
d'(z, g'(0', 0')) → e'(0')
d'(z, g'(x, y)) → g'(e'(x), d'(z, y))
d'(c'(z), g'(g'(x, y), 0')) → g'(d'(c'(z), g'(x, y)), d'(z, g'(x, y)))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: c' → e':0' → h'
e' :: e':0' → e':0'
c' :: c' → c'
d' :: c' → e':0' → e':0'
g' :: e':0' → e':0' → e':0'
0' :: e':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_e':0'3 :: e':0'
_gen_c'4 :: Nat → c'
_gen_e':0'5 :: Nat → e':0'

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(_gen_c'4(x))
_gen_e':0'5(0) ⇔ 0'
_gen_e':0'5(+(x, 1)) ⇔ e'(_gen_e':0'5(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':0'5(+(1, _n7)), _gen_e':0'5(+(1, _n7))) → _*6, rt ∈ Ω(n7)

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

Induction Step:
g'(_gen_e':0'5(+(1, +(_\$n8, 1))), _gen_e':0'5(+(1, +(_\$n8, 1)))) →RΩ(1)
e'(g'(_gen_e':0'5(+(1, _\$n8)), _gen_e':0'5(+(1, _\$n8)))) →IH
e'(_*6)

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

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

Types:
h' :: c' → e':0' → h'
e' :: e':0' → e':0'
c' :: c' → c'
d' :: c' → e':0' → e':0'
g' :: e':0' → e':0' → e':0'
0' :: e':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_e':0'3 :: e':0'
_gen_c'4 :: Nat → c'
_gen_e':0'5 :: Nat → e':0'

Lemmas:
g'(_gen_e':0'5(+(1, _n7)), _gen_e':0'5(+(1, _n7))) → _*6, rt ∈ Ω(n7)

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(_gen_c'4(x))
_gen_e':0'5(0) ⇔ 0'
_gen_e':0'5(+(x, 1)) ⇔ e'(_gen_e':0'5(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'(z, e'(x)) → h'(c'(z), d'(z, x))
d'(z, g'(0', 0')) → e'(0')
d'(z, g'(x, y)) → g'(e'(x), d'(z, y))
d'(c'(z), g'(g'(x, y), 0')) → g'(d'(c'(z), g'(x, y)), d'(z, g'(x, y)))
g'(e'(x), e'(y)) → e'(g'(x, y))

Types:
h' :: c' → e':0' → h'
e' :: e':0' → e':0'
c' :: c' → c'
d' :: c' → e':0' → e':0'
g' :: e':0' → e':0' → e':0'
0' :: e':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_e':0'3 :: e':0'
_gen_c'4 :: Nat → c'
_gen_e':0'5 :: Nat → e':0'

Lemmas:
g'(_gen_e':0'5(+(1, _n7)), _gen_e':0'5(+(1, _n7))) → _*6, rt ∈ Ω(n7)

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(_gen_c'4(x))
_gen_e':0'5(0) ⇔ 0'
_gen_e':0'5(+(x, 1)) ⇔ e'(_gen_e':0'5(x))

The following defined symbols remain to be analysed:
h'

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

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

Types:
h' :: c' → e':0' → h'
e' :: e':0' → e':0'
c' :: c' → c'
d' :: c' → e':0' → e':0'
g' :: e':0' → e':0' → e':0'
0' :: e':0'
_hole_h'1 :: h'
_hole_c'2 :: c'
_hole_e':0'3 :: e':0'
_gen_c'4 :: Nat → c'
_gen_e':0'5 :: Nat → e':0'

Lemmas:
g'(_gen_e':0'5(+(1, _n7)), _gen_e':0'5(+(1, _n7))) → _*6, rt ∈ Ω(n7)

Generator Equations:
_gen_c'4(0) ⇔ _hole_c'2
_gen_c'4(+(x, 1)) ⇔ c'(_gen_c'4(x))
_gen_e':0'5(0) ⇔ 0'
_gen_e':0'5(+(x, 1)) ⇔ e'(_gen_e':0'5(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
g'(_gen_e':0'5(+(1, _n7)), _gen_e':0'5(+(1, _n7))) → _*6, rt ∈ Ω(n7)