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

shuffle(Cons(x, xs)) → Cons(x, shuffle(reverse(xs)))
reverse(Cons(x, xs)) → append(reverse(xs), Cons(x, Nil))
append(Cons(x, xs), ys) → Cons(x, append(xs, ys))
shuffle(Nil) → Nil
reverse(Nil) → Nil
append(Nil, ys) → ys
goal(xs) → shuffle(xs)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


shuffle'(Cons'(x, xs)) → Cons'(x, shuffle'(reverse'(xs)))
reverse'(Cons'(x, xs)) → append'(reverse'(xs), Cons'(x, Nil'))
append'(Cons'(x, xs), ys) → Cons'(x, append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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


shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Types:
shuffle' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
reverse' :: Cons':Nil' → Cons':Nil'
append' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

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

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

Rules:
shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Types:
shuffle' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
reverse' :: Cons':Nil' → Cons':Nil'
append' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

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

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

Proved the following rewrite lemma:
append'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Induction Base:
append'(_gen_Cons':Nil'2(0), _gen_Cons':Nil'2(b)) →RΩ(1)
_gen_Cons':Nil'2(b)

Induction Step:
append'(_gen_Cons':Nil'2(+(_$n5, 1)), _gen_Cons':Nil'2(_b139)) →RΩ(1)
Cons'(append'(_gen_Cons':Nil'2(_$n5), _gen_Cons':Nil'2(_b139))) →IH
Cons'(_gen_Cons':Nil'2(+(_$n5, _b139)))

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

Rules:
shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Types:
shuffle' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
reverse' :: Cons':Nil' → Cons':Nil'
append' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
append'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

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_Cons':Nil'2(_n438)) → _gen_Cons':Nil'2(_n438), rt ∈ Ω(1 + n438 + n4382)

Induction Base:
reverse'(_gen_Cons':Nil'2(0)) →RΩ(1)
Nil'

Induction Step:
reverse'(_gen_Cons':Nil'2(+(_$n439, 1))) →RΩ(1)
append'(reverse'(_gen_Cons':Nil'2(_$n439)), Cons'(Nil')) →IH
append'(_gen_Cons':Nil'2(_$n439), Cons'(Nil')) →LΩ(1 + $n439)
_gen_Cons':Nil'2(+(_$n439, +(0, 1)))

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

Rules:
shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Types:
shuffle' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
reverse' :: Cons':Nil' → Cons':Nil'
append' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
append'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_Cons':Nil'2(_n438)) → _gen_Cons':Nil'2(_n438), rt ∈ Ω(1 + n438 + n4382)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
shuffle'

Proved the following rewrite lemma:
shuffle'(_gen_Cons':Nil'2(_n823)) → _gen_Cons':Nil'2(_n823), rt ∈ Ω(1 + n823 + n8232 + n8233)

Induction Base:
shuffle'(_gen_Cons':Nil'2(0)) →RΩ(1)
Nil'

Induction Step:
shuffle'(_gen_Cons':Nil'2(+(_$n824, 1))) →RΩ(1)
Cons'(shuffle'(reverse'(_gen_Cons':Nil'2(_$n824)))) →LΩ(1 + $n824 + $n8242)
Cons'(shuffle'(_gen_Cons':Nil'2(_$n824))) →IH
Cons'(_gen_Cons':Nil'2(_$n824))

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

Rules:
shuffle'(Cons'(xs)) → Cons'(shuffle'(reverse'(xs)))
reverse'(Cons'(xs)) → append'(reverse'(xs), Cons'(Nil'))
append'(Cons'(xs), ys) → Cons'(append'(xs, ys))
shuffle'(Nil') → Nil'
reverse'(Nil') → Nil'
append'(Nil', ys) → ys
goal'(xs) → shuffle'(xs)

Types:
shuffle' :: Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
reverse' :: Cons':Nil' → Cons':Nil'
append' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
append'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) → _gen_Cons':Nil'2(+(_n4, b)), rt ∈ Ω(1 + n4)
reverse'(_gen_Cons':Nil'2(_n438)) → _gen_Cons':Nil'2(_n438), rt ∈ Ω(1 + n438 + n4382)
shuffle'(_gen_Cons':Nil'2(_n823)) → _gen_Cons':Nil'2(_n823), rt ∈ Ω(1 + n823 + n8232 + n8233)

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n3) was proven with the following lemma:
shuffle'(_gen_Cons':Nil'2(_n823)) → _gen_Cons':Nil'2(_n823), rt ∈ Ω(1 + n823 + n8232 + n8233)