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

mul0(Cons(x, xs), y) → add0(mul0(xs, y), y)
mul0(Nil, y) → Nil
goal(xs, ys) → mul0(xs, ys)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

mul0'(Cons'(x, xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

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

mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Types:
mul0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
add0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → 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:

They will be analysed ascendingly in the following order:

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Types:
mul0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
add0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → 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:

They will be analysed ascendingly in the following order:

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

The following conjecture could not be proven:

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Types:
mul0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
add0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → 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:
mul0'

Proved the following rewrite lemma:
mul0'(_gen_Cons':Nil'2(_n898), _gen_Cons':Nil'2(0)) → _gen_Cons':Nil'2(0), rt ∈ Ω(1 + n898)

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

Induction Step:
mul0'(_gen_Cons':Nil'2(+(_\$n899, 1)), _gen_Cons':Nil'2(0)) →RΩ(1)
_gen_Cons':Nil'2(0)

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

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
mul0'(Nil', y) → Nil'
goal'(xs, ys) → mul0'(xs, ys)

Types:
mul0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
add0' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Lemmas:
mul0'(_gen_Cons':Nil'2(_n898), _gen_Cons':Nil'2(0)) → _gen_Cons':Nil'2(0), rt ∈ Ω(1 + n898)

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 Ω(n) was proven with the following lemma:
mul0'(_gen_Cons':Nil'2(_n898), _gen_Cons':Nil'2(0)) → _gen_Cons':Nil'2(0), rt ∈ Ω(1 + n898)