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

mul0(Cons(x, xs), y) → add0(mul0(xs, y), y)
add0(Cons(x, xs), y) → add0(xs, Cons(S, y))
mul0(Nil, y) → Nil
add0(Nil, y) → y
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)
add0'(Cons'(x, xs), y) → add0'(xs, Cons'(S', y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
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)
add0'(Cons'(xs), y) → add0'(xs, Cons'(y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
goal'(xs, ys) → mul0'(xs, ys)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
add0'(Cons'(xs), y) → add0'(xs, Cons'(y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
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:
mul0', add0'

They will be analysed ascendingly in the following order:
add0' < mul0'

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
add0'(Cons'(xs), y) → add0'(xs, Cons'(y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
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:
add0', mul0'

They will be analysed ascendingly in the following order:
add0' < mul0'

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

The following conjecture could not be proven:

add0'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) →? _gen_Cons':Nil'2(+(_n4, b))

Rules:
mul0'(Cons'(xs), y) → add0'(mul0'(xs, y), y)
add0'(Cons'(xs), y) → add0'(xs, Cons'(y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
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)
add0'(mul0'(_gen_Cons':Nil'2(_$n899), _gen_Cons':Nil'2(0)), _gen_Cons':Nil'2(0)) →IH
add0'(_gen_Cons':Nil'2(0), _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)
add0'(Cons'(xs), y) → add0'(xs, Cons'(y))
mul0'(Nil', y) → Nil'
add0'(Nil', y) → y
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)