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

max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(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:


max'(L'(x)) → x
max'(N'(L'(0'), L'(y))) → y
max'(N'(L'(s'(x)), L'(s'(y)))) → s'(max'(N'(L'(x), L'(y))))
max'(N'(L'(x), N'(y, z))) → max'(N'(L'(x), L'(max'(N'(y, z)))))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
max'(L'(x)) → x
max'(N'(L'(0'), L'(y))) → y
max'(N'(L'(s'(x)), L'(s'(y)))) → s'(max'(N'(L'(x), L'(y))))
max'(N'(L'(x), N'(y, z))) → max'(N'(L'(x), L'(max'(N'(y, z)))))

Types:
max' :: L':N' → 0':s'
L' :: 0':s' → L':N'
N' :: L':N' → L':N' → L':N'
0' :: 0':s'
s' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_L':N'2 :: L':N'
_gen_0':s'3 :: Nat → 0':s'
_gen_L':N'4 :: Nat → L':N'

Heuristically decided to analyse the following defined symbols:
max'

Rules:
max'(L'(x)) → x
max'(N'(L'(0'), L'(y))) → y
max'(N'(L'(s'(x)), L'(s'(y)))) → s'(max'(N'(L'(x), L'(y))))
max'(N'(L'(x), N'(y, z))) → max'(N'(L'(x), L'(max'(N'(y, z)))))

Types:
max' :: L':N' → 0':s'
L' :: 0':s' → L':N'
N' :: L':N' → L':N' → L':N'
0' :: 0':s'
s' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_L':N'2 :: L':N'
_gen_0':s'3 :: Nat → 0':s'
_gen_L':N'4 :: Nat → L':N'

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_L':N'4(0) ⇔ L'(0')
_gen_L':N'4(+(x, 1)) ⇔ N'(L'(0'), _gen_L':N'4(x))

The following defined symbols remain to be analysed:
max'

Proved the following rewrite lemma:
max'(_gen_L':N'4(+(1, _n6))) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)

Induction Base:
max'(_gen_L':N'4(+(1, 0))) →RΩ(1)
0'

Induction Step:
max'(_gen_L':N'4(+(1, +(_$n7, 1)))) →RΩ(1)
max'(N'(L'(0'), L'(max'(N'(L'(0'), _gen_L':N'4(_$n7)))))) →IH
max'(N'(L'(0'), L'(_gen_0':s'3(0)))) →RΩ(1)
_gen_0':s'3(0)

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

Rules:
max'(L'(x)) → x
max'(N'(L'(0'), L'(y))) → y
max'(N'(L'(s'(x)), L'(s'(y)))) → s'(max'(N'(L'(x), L'(y))))
max'(N'(L'(x), N'(y, z))) → max'(N'(L'(x), L'(max'(N'(y, z)))))

Types:
max' :: L':N' → 0':s'
L' :: 0':s' → L':N'
N' :: L':N' → L':N' → L':N'
0' :: 0':s'
s' :: 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_L':N'2 :: L':N'
_gen_0':s'3 :: Nat → 0':s'
_gen_L':N'4 :: Nat → L':N'

Lemmas:
max'(_gen_L':N'4(+(1, _n6))) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))
_gen_L':N'4(0) ⇔ L'(0')
_gen_L':N'4(+(x, 1)) ⇔ N'(L'(0'), _gen_L':N'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
max'(_gen_L':N'4(+(1, _n6))) → _gen_0':s'3(0), rt ∈ Ω(1 + n6)