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

*(x, *(y, z)) → *(otimes(x, y), z)
*(1, y) → y
*(+(x, y), z) → oplus(*(x, z), *(y, z))
*(x, oplus(y, z)) → oplus(*(x, y), *(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:


*'(x, *'(y, z)) → *'(otimes'(x, y), z)
*'(1', y) → y
*'(+'(x, y), z) → oplus'(*'(x, z), *'(y, z))
*'(x, oplus'(y, z)) → oplus'(*'(x, y), *'(x, z))

Rewrite Strategy: INNERMOST

Sliced the following arguments:
otimes'/0
otimes'/1

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


*'(x, *'(y, z)) → *'(otimes', z)
*'(1', y) → y
*'(+'(x, y), z) → oplus'(*'(x, z), *'(y, z))
*'(x, oplus'(y, z)) → oplus'(*'(x, y), *'(x, z))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
*'(x, *'(y, z)) → *'(otimes', z)
*'(1', y) → y
*'(+'(x, y), z) → oplus'(*'(x, z), *'(y, z))
*'(x, oplus'(y, z)) → oplus'(*'(x, y), *'(x, z))

Types:
*' :: otimes':1':+' → oplus' → oplus'
otimes' :: otimes':1':+'
1' :: otimes':1':+'
+' :: otimes':1':+' → otimes':1':+' → otimes':1':+'
oplus' :: oplus' → oplus' → oplus'
_hole_oplus'1 :: oplus'
_hole_otimes':1':+'2 :: otimes':1':+'
_gen_oplus'3 :: Nat → oplus'
_gen_otimes':1':+'4 :: Nat → otimes':1':+'

Heuristically decided to analyse the following defined symbols:
*'

Rules:
*'(x, *'(y, z)) → *'(otimes', z)
*'(1', y) → y
*'(+'(x, y), z) → oplus'(*'(x, z), *'(y, z))
*'(x, oplus'(y, z)) → oplus'(*'(x, y), *'(x, z))

Types:
*' :: otimes':1':+' → oplus' → oplus'
otimes' :: otimes':1':+'
1' :: otimes':1':+'
+' :: otimes':1':+' → otimes':1':+' → otimes':1':+'
oplus' :: oplus' → oplus' → oplus'
_hole_oplus'1 :: oplus'
_hole_otimes':1':+'2 :: otimes':1':+'
_gen_oplus'3 :: Nat → oplus'
_gen_otimes':1':+'4 :: Nat → otimes':1':+'

Generator Equations:
_gen_oplus'3(0) ⇔ _hole_oplus'1
_gen_oplus'3(+(x, 1)) ⇔ oplus'(_hole_oplus'1, _gen_oplus'3(x))
_gen_otimes':1':+'4(0) ⇔ 1'
_gen_otimes':1':+'4(+(x, 1)) ⇔ +'(1', _gen_otimes':1':+'4(x))

The following defined symbols remain to be analysed:
*'

Proved the following rewrite lemma:
*'(_gen_otimes':1':+'4(0), _gen_oplus'3(_n6)) → _*5, rt ∈ Ω(n6)

Induction Base:
*'(_gen_otimes':1':+'4(0), _gen_oplus'3(0))

Induction Step:
*'(_gen_otimes':1':+'4(0), _gen_oplus'3(+(_$n7, 1))) →RΩ(1)
oplus'(*'(_gen_otimes':1':+'4(0), _hole_oplus'1), *'(_gen_otimes':1':+'4(0), _gen_oplus'3(_$n7))) →RΩ(1)
oplus'(_hole_oplus'1, *'(_gen_otimes':1':+'4(0), _gen_oplus'3(_$n7))) →IH
oplus'(_hole_oplus'1, _*5)

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

Rules:
*'(x, *'(y, z)) → *'(otimes', z)
*'(1', y) → y
*'(+'(x, y), z) → oplus'(*'(x, z), *'(y, z))
*'(x, oplus'(y, z)) → oplus'(*'(x, y), *'(x, z))

Types:
*' :: otimes':1':+' → oplus' → oplus'
otimes' :: otimes':1':+'
1' :: otimes':1':+'
+' :: otimes':1':+' → otimes':1':+' → otimes':1':+'
oplus' :: oplus' → oplus' → oplus'
_hole_oplus'1 :: oplus'
_hole_otimes':1':+'2 :: otimes':1':+'
_gen_oplus'3 :: Nat → oplus'
_gen_otimes':1':+'4 :: Nat → otimes':1':+'

Lemmas:
*'(_gen_otimes':1':+'4(0), _gen_oplus'3(_n6)) → _*5, rt ∈ Ω(n6)

Generator Equations:
_gen_oplus'3(0) ⇔ _hole_oplus'1
_gen_oplus'3(+(x, 1)) ⇔ oplus'(_hole_oplus'1, _gen_oplus'3(x))
_gen_otimes':1':+'4(0) ⇔ 1'
_gen_otimes':1':+'4(+(x, 1)) ⇔ +'(1', _gen_otimes':1':+'4(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
*'(_gen_otimes':1':+'4(0), _gen_oplus'3(_n6)) → _*5, rt ∈ Ω(n6)