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

g(x, 0) → 0
g(d, s(x)) → s(s(g(d, x)))
g(h, s(0)) → 0
g(h, s(s(x))) → s(g(h, x))
double(x) → g(d, x)
half(x) → g(h, x)
f(s(x), y) → f(half(s(x)), double(y))
f(s(0), y) → y
id(x) → f(x, s(0))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))

Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'

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

Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))

Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'

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

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

Proved the following rewrite lemma:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)

Induction Base:
g'(h', _gen_0':s'3(*(2, 0))) →RΩ(1)
0'

Induction Step:
g'(h', _gen_0':s'3(*(2, +(_\$n6, 1)))) →RΩ(1)
s'(g'(h', _gen_0':s'3(*(2, _\$n6)))) →IH
s'(_gen_0':s'3(_\$n6))

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

Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))

Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)

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

The following defined symbols remain to be analysed:
f'

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

Rules:
g'(x, 0') → 0'
g'(d', s'(x)) → s'(s'(g'(d', x)))
g'(h', s'(0')) → 0'
g'(h', s'(s'(x))) → s'(g'(h', x))
double'(x) → g'(d', x)
half'(x) → g'(h', x)
f'(s'(x), y) → f'(half'(s'(x)), double'(y))
f'(s'(0'), y) → y
id'(x) → f'(x, s'(0'))

Types:
g' :: d':h' → 0':s' → 0':s'
0' :: 0':s'
d' :: d':h'
s' :: 0':s' → 0':s'
h' :: d':h'
double' :: 0':s' → 0':s'
half' :: 0':s' → 0':s'
f' :: 0':s' → 0':s' → 0':s'
id' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_d':h'2 :: d':h'
_gen_0':s'3 :: Nat → 0':s'

Lemmas:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)

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

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
g'(h', _gen_0':s'3(*(2, _n5))) → _gen_0':s'3(_n5), rt ∈ Ω(1 + n5)