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

f(nil) → nil
f(.(nil, y)) → .(nil, f(y))
f(.(.(x, y), z)) → f(.(x, .(y, z)))
g(nil) → nil
g(.(x, nil)) → .(g(x), nil)
g(.(x, .(y, z))) → g(.(.(x, y), z))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))

Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

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

Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))

Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))

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

Proved the following rewrite lemma:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)

Induction Base:
f'(_gen_nil':.'2(0)) →RΩ(1)
nil'

Induction Step:
f'(_gen_nil':.'2(+(_\$n5, 1))) →RΩ(1)
.'(nil', f'(_gen_nil':.'2(_\$n5))) →IH
.'(nil', _gen_nil':.'2(_\$n5))

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

Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))

Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Lemmas:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))

The following defined symbols remain to be analysed:
g'

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

The following conjecture could not be proven:

g'(_gen_nil':.'2(+(2, _n334))) →? _*3

Rules:
f'(nil') → nil'
f'(.'(nil', y)) → .'(nil', f'(y))
f'(.'(.'(x, y), z)) → f'(.'(x, .'(y, z)))
g'(nil') → nil'
g'(.'(x, nil')) → .'(g'(x), nil')
g'(.'(x, .'(y, z))) → g'(.'(.'(x, y), z))

Types:
f' :: nil':.' → nil':.'
nil' :: nil':.'
.' :: nil':.' → nil':.' → nil':.'
g' :: nil':.' → nil':.'
_hole_nil':.'1 :: nil':.'
_gen_nil':.'2 :: Nat → nil':.'

Lemmas:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_nil':.'2(0) ⇔ nil'
_gen_nil':.'2(+(x, 1)) ⇔ .'(nil', _gen_nil':.'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_nil':.'2(_n4)) → _gen_nil':.'2(_n4), rt ∈ Ω(1 + n4)