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

app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
shuffle(nil) → nil

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

app'(nil', y) → y
app'(add'(n, x), y) → add'(n, app'(x, y))
reverse'(nil') → nil'
shuffle'(nil') → nil'

Rewrite Strategy: INNERMOST

Sliced the following arguments:

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

app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Rewrite Strategy: INNERMOST

Infered types.

Rules:
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Types:

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

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

Rules:
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Types:

Generator Equations:

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

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

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

Induction Base:

Induction Step:

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

Rules:
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Types:

Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:

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

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

Proved the following rewrite lemma:
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)

Induction Base:
nil'

Induction Step:

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

Rules:
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Types:

Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)

Generator Equations:

The following defined symbols remain to be analysed:
shuffle'

Proved the following rewrite lemma:
shuffle'(_gen_nil':add'2(_n738)) → _gen_nil':add'2(_n738), rt ∈ Ω(1 + n738 + n7382 + n7383)

Induction Base:
nil'

Induction Step:

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

Rules:
app'(nil', y) → y
reverse'(nil') → nil'
shuffle'(nil') → nil'

Types:

Lemmas:
app'(_gen_nil':add'2(_n4), _gen_nil':add'2(b)) → _gen_nil':add'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_nil':add'2(_n395)) → _gen_nil':add'2(_n395), rt ∈ Ω(1 + n395 + n3952)
shuffle'(_gen_nil':add'2(_n738)) → _gen_nil':add'2(_n738), rt ∈ Ω(1 + n738 + n7382 + n7383)

Generator Equations: