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

norm(nil) → 0
norm(g(x, y)) → s(norm(x))
f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
rem(nil, y) → nil
rem(g(x, y), 0) → g(x, y)
rem(g(x, y), s(z)) → rem(x, z)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

norm'(nil') → 0'
norm'(g'(x, y)) → s'(norm'(x))
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
rem'(nil', y) → nil'
rem'(g'(x, y), 0') → g'(x, y)
rem'(g'(x, y), s'(z)) → rem'(x, z)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
g'/1
f'/0

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

norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'

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

Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))

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

Proved the following rewrite lemma:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)

Induction Base:
norm'(_gen_nil':g'4(0)) →RΩ(1)
0'

Induction Step:
norm'(_gen_nil':g'4(+(_\$n7, 1))) →RΩ(1)
s'(norm'(_gen_nil':g'4(_\$n7))) →IH
s'(_gen_0':s'3(_\$n7))

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

Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'

Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))

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

Proved the following rewrite lemma:
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)

Induction Base:
f'(_gen_nil':g'4(0)) →RΩ(1)
g'(nil')

Induction Step:
f'(_gen_nil':g'4(+(_\$n229, 1))) →RΩ(1)
g'(f'(_gen_nil':g'4(_\$n229))) →IH
g'(_gen_nil':g'4(+(1, _\$n229)))

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

Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'

Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))

The following defined symbols remain to be analysed:
rem'

Proved the following rewrite lemma:
rem'(_gen_nil':g'4(_n525), _gen_0':s'3(_n525)) → _gen_nil':g'4(0), rt ∈ Ω(1 + n525)

Induction Base:
rem'(_gen_nil':g'4(0), _gen_0':s'3(0)) →RΩ(1)
nil'

Induction Step:
rem'(_gen_nil':g'4(+(_\$n526, 1)), _gen_0':s'3(+(_\$n526, 1))) →RΩ(1)
rem'(_gen_nil':g'4(_\$n526), _gen_0':s'3(_\$n526)) →IH
_gen_nil':g'4(0)

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

Rules:
norm'(nil') → 0'
norm'(g'(x)) → s'(norm'(x))
f'(nil') → g'(nil')
f'(g'(y)) → g'(f'(y))
rem'(nil', y) → nil'
rem'(g'(x), 0') → g'(x)
rem'(g'(x), s'(z)) → rem'(x, z)

Types:
norm' :: nil':g' → 0':s'
nil' :: nil':g'
0' :: 0':s'
g' :: nil':g' → nil':g'
s' :: 0':s' → 0':s'
f' :: nil':g' → nil':g'
rem' :: nil':g' → 0':s' → nil':g'
_hole_0':s'1 :: 0':s'
_hole_nil':g'2 :: nil':g'
_gen_0':s'3 :: Nat → 0':s'
_gen_nil':g'4 :: Nat → nil':g'

Lemmas:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)
f'(_gen_nil':g'4(_n228)) → _gen_nil':g'4(+(1, _n228)), rt ∈ Ω(1 + n228)
rem'(_gen_nil':g'4(_n525), _gen_0':s'3(_n525)) → _gen_nil':g'4(0), rt ∈ Ω(1 + n525)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
norm'(_gen_nil':g'4(_n6)) → _gen_0':s'3(_n6), rt ∈ Ω(1 + n6)