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

p(s(x)) → x
fact(0) → s(0)
fact(s(x)) → *(s(x), fact(p(s(x))))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
+(x, 0) → x
+(x, s(y)) → s(+(x, y))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
fact' :: s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
+' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Heuristically decided to analyse the following defined symbols:
fact', *', +'

They will be analysed ascendingly in the following order:
*' < fact'
+' < *'

Rules:
p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
fact' :: s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
+' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

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

The following defined symbols remain to be analysed:
+', fact', *'

They will be analysed ascendingly in the following order:
*' < fact'
+' < *'

Proved the following rewrite lemma:
+'(_gen_s':0'2(a), _gen_s':0'2(_n4)) → _gen_s':0'2(+(_n4, a)), rt ∈ Ω(1 + n4)

Induction Base:
+'(_gen_s':0'2(a), _gen_s':0'2(0)) →RΩ(1)
_gen_s':0'2(a)

Induction Step:
+'(_gen_s':0'2(_a137), _gen_s':0'2(+(_$n5, 1))) →RΩ(1)
s'(+'(_gen_s':0'2(_a137), _gen_s':0'2(_$n5))) →IH
s'(_gen_s':0'2(+(_$n5, _a137)))

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

Rules:
p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
fact' :: s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
+' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Lemmas:
+'(_gen_s':0'2(a), _gen_s':0'2(_n4)) → _gen_s':0'2(+(_n4, a)), rt ∈ Ω(1 + n4)

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

The following defined symbols remain to be analysed:
*', fact'

They will be analysed ascendingly in the following order:
*' < fact'

Proved the following rewrite lemma:
*'(_gen_s':0'2(_n480), _gen_s':0'2(b)) → _gen_s':0'2(*(_n480, b)), rt ∈ Ω(1 + b740·n480 + n480)

Induction Base:
*'(_gen_s':0'2(0), _gen_s':0'2(b)) →RΩ(1)
0'

Induction Step:
*'(_gen_s':0'2(+(_$n481, 1)), _gen_s':0'2(_b740)) →RΩ(1)
+'(*'(_gen_s':0'2(_$n481), _gen_s':0'2(_b740)), _gen_s':0'2(_b740)) →IH
+'(_gen_s':0'2(*(_$n481, _b740)), _gen_s':0'2(_b740)) →LΩ(1 + b740)
_gen_s':0'2(+(_b740, *(_$n481, _b740)))

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

Rules:
p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
fact' :: s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
+' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Lemmas:
+'(_gen_s':0'2(a), _gen_s':0'2(_n4)) → _gen_s':0'2(+(_n4, a)), rt ∈ Ω(1 + n4)
*'(_gen_s':0'2(_n480), _gen_s':0'2(b)) → _gen_s':0'2(*(_n480, b)), rt ∈ Ω(1 + b740·n480 + n480)

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

The following defined symbols remain to be analysed:
fact'

Proved the following rewrite lemma:
fact'(_gen_s':0'2(_n1221)) → _*3, rt ∈ Ω(n1221)

Induction Base:
fact'(_gen_s':0'2(0))

Induction Step:
fact'(_gen_s':0'2(+(_$n1222, 1))) →RΩ(1)
*'(s'(_gen_s':0'2(_$n1222)), fact'(p'(s'(_gen_s':0'2(_$n1222))))) →RΩ(1)
*'(s'(_gen_s':0'2(_$n1222)), fact'(_gen_s':0'2(_$n1222))) →IH
*'(s'(_gen_s':0'2(_$n1222)), _*3)

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

Rules:
p'(s'(x)) → x
fact'(0') → s'(0')
fact'(s'(x)) → *'(s'(x), fact'(p'(s'(x))))
*'(0', y) → 0'
*'(s'(x), y) → +'(*'(x, y), y)
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))

Types:
p' :: s':0' → s':0'
s' :: s':0' → s':0'
fact' :: s':0' → s':0'
0' :: s':0'
*' :: s':0' → s':0' → s':0'
+' :: s':0' → s':0' → s':0'
_hole_s':0'1 :: s':0'
_gen_s':0'2 :: Nat → s':0'

Lemmas:
+'(_gen_s':0'2(a), _gen_s':0'2(_n4)) → _gen_s':0'2(+(_n4, a)), rt ∈ Ω(1 + n4)
*'(_gen_s':0'2(_n480), _gen_s':0'2(b)) → _gen_s':0'2(*(_n480, b)), rt ∈ Ω(1 + b740·n480 + n480)
fact'(_gen_s':0'2(_n1221)) → _*3, rt ∈ Ω(n1221)

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

No more defined symbols left to analyse.

The lowerbound Ω(n2) was proven with the following lemma:
*'(_gen_s':0'2(_n480), _gen_s':0'2(b)) → _gen_s':0'2(*(_n480, b)), rt ∈ Ω(1 + b740·n480 + n480)