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

*(x, +(y, z)) → +(*(x, y), *(x, z))
*(+(x, y), z) → +(*(x, z), *(y, z))
*(x, 1) → x
*(1, y) → y

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

Rewrite Strategy: INNERMOST

Infered types.

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

Types:
*' :: +':1' → +':1' → +':1'
+' :: +':1' → +':1' → +':1'
1' :: +':1'
_hole_+':1'1 :: +':1'
_gen_+':1'2 :: Nat → +':1'

Heuristically decided to analyse the following defined symbols:
*'

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

Types:
*' :: +':1' → +':1' → +':1'
+' :: +':1' → +':1' → +':1'
1' :: +':1'
_hole_+':1'1 :: +':1'
_gen_+':1'2 :: Nat → +':1'

Generator Equations:
_gen_+':1'2(0) ⇔ 1'
_gen_+':1'2(+(x, 1)) ⇔ +'(1', _gen_+':1'2(x))

The following defined symbols remain to be analysed:
*'

Proved the following rewrite lemma:
*'(_gen_+':1'2(a), _gen_+':1'2(_n4)) → _*3, rt ∈ Ω(n4)

Induction Base:
*'(_gen_+':1'2(a), _gen_+':1'2(0))

Induction Step:
*'(_gen_+':1'2(_a62803), _gen_+':1'2(+(_$n5, 1))) →RΩ(1)
+'(*'(_gen_+':1'2(_a62803), 1'), *'(_gen_+':1'2(_a62803), _gen_+':1'2(_$n5))) →RΩ(1)
+'(_gen_+':1'2(_a62803), *'(_gen_+':1'2(_a62803), _gen_+':1'2(_$n5))) →IH
+'(_gen_+':1'2(_a62803), _*3)

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

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

Types:
*' :: +':1' → +':1' → +':1'
+' :: +':1' → +':1' → +':1'
1' :: +':1'
_hole_+':1'1 :: +':1'
_gen_+':1'2 :: Nat → +':1'

Lemmas:
*'(_gen_+':1'2(a), _gen_+':1'2(_n4)) → _*3, rt ∈ Ω(n4)

Generator Equations:
_gen_+':1'2(0) ⇔ 1'
_gen_+':1'2(+(x, 1)) ⇔ +'(1', _gen_+':1'2(x))

No more defined symbols left to analyse.

The lowerbound Ω(n) was proven with the following lemma:
*'(_gen_+':1'2(a), _gen_+':1'2(_n4)) → _*3, rt ∈ Ω(n4)