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

null(nil) → true
tail(nil) → nil
app(nil, y) → y
reverse(nil) → nil
shuffle(x) → shuff(x, nil)
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(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:

null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Types:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'

Heuristically decided to analyse the following defined symbols:
app', reverse', shuff'

They will be analysed ascendingly in the following order:
app' < reverse'
app' < shuff'
reverse' < shuff'

Rules:
null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Types:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'

Generator Equations:

The following defined symbols remain to be analysed:
app', reverse', shuff'

They will be analysed ascendingly in the following order:
app' < reverse'
app' < shuff'
reverse' < shuff'

Proved the following rewrite lemma:

Induction Base:

Induction Step:

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

Rules:
null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Types:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
reverse', shuff'

They will be analysed ascendingly in the following order:
reverse' < shuff'

Proved the following rewrite lemma:

Induction Base:
nil'

Induction Step:

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

Rules:
null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Types:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:
shuff'

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

Rules:
null'(nil') → true'
tail'(nil') → nil'
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(x) → shuff'(x, nil')
if'(true', x, y, z) → y
if'(false', x, y, z) → shuff'(reverse'(tail'(x)), z)

Types:
true' :: true':false'
false' :: true':false'
_hole_true':false'1 :: true':false'

Lemmas: