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

f(x, nil) → g(nil, x)
f(x, g(y, z)) → g(f(x, y), z)
++(x, nil) → x
++(x, g(y, z)) → g(++(x, y), z)
null(nil) → true
null(g(x, y)) → false
mem(nil, y) → false
mem(g(x, y), z) → or(=(y, z), mem(x, z))
mem(x, max(x)) → not(null(x))
max(g(g(nil, x), y)) → max'(x, y)
max(g(g(g(x, y), z), u)) → max'(max(g(g(x, y), z)), u)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(='(y, z), mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x, y)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)), u')

Rewrite Strategy: INNERMOST

Sliced the following arguments:
or'/0
='/0
='/1
max'''/1

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

f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Heuristically decided to analyse the following defined symbols:
f', ++', mem', max''

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))

The following defined symbols remain to be analysed:
f', ++', mem', max''

Proved the following rewrite lemma:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)

Induction Base:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, 0)))

Induction Step:
f'(_gen_max''':u'5(_a548903), _gen_nil':g'4(+(1, +(_\$n9, 1)))) →RΩ(1)
g'(f'(_gen_max''':u'5(_a548903), _gen_nil':g'4(+(1, _\$n9))), u') →IH
g'(_*7, u')

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

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)

Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))

The following defined symbols remain to be analysed:
++', mem', max''

Proved the following rewrite lemma:
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)

Induction Base:
++'(_gen_nil':g'4(a), _gen_nil':g'4(0)) →RΩ(1)
_gen_nil':g'4(a)

Induction Step:
++'(_gen_nil':g'4(_a549713), _gen_nil':g'4(+(_\$n549441, 1))) →RΩ(1)
g'(++'(_gen_nil':g'4(_a549713), _gen_nil':g'4(_\$n549441)), u') →IH
g'(_gen_nil':g'4(+(_\$n549441, _a549713)), u')

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

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)

Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))

The following defined symbols remain to be analysed:
mem', max''

Proved the following rewrite lemma:
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)

Induction Base:
mem'(_gen_nil':g'4(+(1, 0)), _gen_max''':u'5(b))

Induction Step:
mem'(_gen_nil':g'4(+(1, +(_\$n550447, 1))), _gen_max''':u'5(_b554002)) →RΩ(1)
or'(mem'(_gen_nil':g'4(+(1, _\$n550447)), _gen_max''':u'5(_b554002))) →IH
or'(_*7)

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

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)

Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))

The following defined symbols remain to be analysed:
max''

Proved the following rewrite lemma:
max''(_gen_nil':g'4(+(2, _n554614))) → _gen_max''':u'5(+(1, _n554614)), rt ∈ Ω(1 + n554614)

Induction Base:
max''(_gen_nil':g'4(+(2, 0))) →RΩ(1)
max'''(u')

Induction Step:
max''(_gen_nil':g'4(+(2, +(_\$n554615, 1)))) →RΩ(1)
max'''(max''(g'(g'(_gen_nil':g'4(_\$n554615), u'), u'))) →IH
max'''(_gen_max''':u'5(+(1, _\$n554615)))

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

Rules:
f'(x, nil') → g'(nil', x)
f'(x, g'(y, z)) → g'(f'(x, y), z)
++'(x, nil') → x
++'(x, g'(y, z)) → g'(++'(x, y), z)
null'(nil') → true'
null'(g'(x, y)) → false'
mem'(nil', y) → false'
mem'(g'(x, y), z) → or'(mem'(x, z))
mem'(x, max''(x)) → not'(null'(x))
max''(g'(g'(nil', x), y)) → max'''(x)
max''(g'(g'(g'(x, y), z), u')) → max'''(max''(g'(g'(x, y), z)))

Types:
f' :: max''':u' → nil':g' → nil':g'
nil' :: nil':g'
g' :: nil':g' → max''':u' → nil':g'
++' :: nil':g' → nil':g' → nil':g'
null' :: nil':g' → true':false':or':not'
true' :: true':false':or':not'
false' :: true':false':or':not'
mem' :: nil':g' → max''':u' → true':false':or':not'
or' :: true':false':or':not' → true':false':or':not'
max'' :: nil':g' → max''':u'
not' :: true':false':or':not' → true':false':or':not'
max''' :: max''':u' → max''':u'
u' :: max''':u'
_hole_nil':g'1 :: nil':g'
_hole_max''':u'2 :: max''':u'
_hole_true':false':or':not'3 :: true':false':or':not'
_gen_nil':g'4 :: Nat → nil':g'
_gen_max''':u'5 :: Nat → max''':u'
_gen_true':false':or':not'6 :: Nat → true':false':or':not'

Lemmas:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)
++'(_gen_nil':g'4(a), _gen_nil':g'4(_n549440)) → _gen_nil':g'4(+(_n549440, a)), rt ∈ Ω(1 + n549440)
mem'(_gen_nil':g'4(+(1, _n550446)), _gen_max''':u'5(b)) → _*7, rt ∈ Ω(n550446)
max''(_gen_nil':g'4(+(2, _n554614))) → _gen_max''':u'5(+(1, _n554614)), rt ∈ Ω(1 + n554614)

Generator Equations:
_gen_nil':g'4(0) ⇔ nil'
_gen_nil':g'4(+(x, 1)) ⇔ g'(_gen_nil':g'4(x), u')
_gen_max''':u'5(0) ⇔ u'
_gen_max''':u'5(+(x, 1)) ⇔ max'''(_gen_max''':u'5(x))
_gen_true':false':or':not'6(0) ⇔ true'
_gen_true':false':or':not'6(+(x, 1)) ⇔ or'(_gen_true':false':or':not'6(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
f'(_gen_max''':u'5(a), _gen_nil':g'4(+(1, _n8))) → _*7, rt ∈ Ω(n8)