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

+(x, 0) → x
+(x, s(y)) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(*(x, y), x)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
fact(x) → iffact(x, ge(x, s(s(0))))
iffact(x, true) → *(x, fact(-(x, s(0))))
iffact(x, false) → s(0)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))
*'(x, 0') → 0'
*'(x, s'(y)) → +'(*'(x, y), x)
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
fact'(x) → iffact'(x, ge'(x, s'(s'(0'))))
iffact'(x, true') → *'(x, fact'(-'(x, s'(0'))))
iffact'(x, false') → s'(0')

Rewrite Strategy: INNERMOST

Infered types.

Rules:
+'(x, 0') → x
+'(x, s'(y)) → s'(+'(x, y))
*'(x, 0') → 0'
*'(x, s'(y)) → +'(*'(x, y), x)
ge'(x, 0') → true'
ge'(0', s'(y)) → false'
ge'(s'(x), s'(y)) → ge'(x, y)
-'(x, 0') → x
-'(s'(x), s'(y)) → -'(x, y)
fact'(x) → iffact'(x, ge'(x, s'(s'(0'))))
iffact'(x, true') → *'(x, fact'(-'(x, s'(0'))))
iffact'(x, false') → s'(0')

Types:
+' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
*' :: 0':s' → 0':s' → 0':s'
ge' :: 0':s' → 0':s' → true':false'
true' :: true':false'
false' :: true':false'
-' :: 0':s' → 0':s' → 0':s'
fact' :: 0':s' → 0':s'
iffact' :: 0':s' → true':false' → 0':s'
_hole_0':s'1 :: 0':s'
_hole_true':false'2 :: true':false'
_gen_0':s'3 :: Nat → 0':s'

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

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

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))

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

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

Proved the following rewrite lemma:
+'(_gen_0':s'3(a), _gen_0':s'3(_n5)) → _gen_0':s'3(+(_n5, a)), rt ∈ Ω(1 + _n5)

Induction Base:
+'(_gen_0':s'3(a), _gen_0':s'3(0)) →_R^Ω(1)
_gen_0':s'3(a)

Induction Step:
+'(_gen_0':s'3(_a138), _gen_0':s'3(+(_$n6, 1))) →_R^Ω(1)
s'(+'(_gen_0':s'3(_a138), _gen_0':s'3(_$n6))) →_IH
s'(_gen_0':s'3(+(_$n6, _a138)))

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

Lemmas:
+'(_gen_0':s'3(a), _gen_0':s'3(_n5)) → _gen_0':s'3(+(_n5, a)), rt ∈ Ω(1 + _n5)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))

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

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

Proved the following rewrite lemma:
*'(_gen_0':s'3(a), _gen_0':s'3(_n728)) → _gen_0':s'3(*(_n728, a)), rt ∈ Ω(1 + _a988·_n728 + _n728)

Induction Base:
*'(_gen_0':s'3(a), _gen_0':s'3(0)) →_R^Ω(1)
0'

Induction Step:
*'(_gen_0':s'3(_a988), _gen_0':s'3(+(_$n729, 1))) →_R^Ω(1)
+'(*'(_gen_0':s'3(_a988), _gen_0':s'3(_$n729)), _gen_0':s'3(_a988)) →_IH
+'(_gen_0':s'3(*(_$n729, _a988)), _gen_0':s'3(_a988)) →_L^{Ω(1 + _a988)}
_gen_0':s'3(+(_a988, *(_$n729, _a988)))

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

Lemmas:
+'(_gen_0':s'3(a), _gen_0':s'3(_n5)) → _gen_0':s'3(+(_n5, a)), rt ∈ Ω(1 + _n5)
*'(_gen_0':s'3(a), _gen_0':s'3(_n728)) → _gen_0':s'3(*(_n728, a)), rt ∈ Ω(1 + _a988·_n728 + _n728)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))

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

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

Proved the following rewrite lemma:
ge'(_gen_0':s'3(_n1782), _gen_0':s'3(_n1782)) → true', rt ∈ Ω(1 + _n1782)

Induction Base:
ge'(_gen_0':s'3(0), _gen_0':s'3(0)) →_R^Ω(1)
true'

Induction Step:
ge'(_gen_0':s'3(+(_$n1783, 1)), _gen_0':s'3(+(_$n1783, 1))) →_R^Ω(1)
ge'(_gen_0':s'3(_$n1783), _gen_0':s'3(_$n1783)) →_IH
true'

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

Lemmas:
+'(_gen_0':s'3(a), _gen_0':s'3(_n5)) → _gen_0':s'3(+(_n5, a)), rt ∈ Ω(1 + _n5)
*'(_gen_0':s'3(a), _gen_0':s'3(_n728)) → _gen_0':s'3(*(_n728, a)), rt ∈ Ω(1 + _a988·_n728 + _n728)
ge'(_gen_0':s'3(_n1782), _gen_0':s'3(_n1782)) → true', rt ∈ Ω(1 + _n1782)

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(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_0':s'3(_n2451), _gen_0':s'3(_n2451)) → _gen_0':s'3(0), rt ∈ Ω(1 + _n2451)

Induction Base:
-'(_gen_0':s'3(0), _gen_0':s'3(0)) →_R^Ω(1)
_gen_0':s'3(0)

Induction Step:
-'(_gen_0':s'3(+(_$n2452, 1)), _gen_0':s'3(+(_$n2452, 1))) →_R^Ω(1)
-'(_gen_0':s'3(_$n2452), _gen_0':s'3(_$n2452)) →_IH
_gen_0':s'3(0)

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

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))

The following defined symbols remain to be analysed:
fact'

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

Generator Equations:
_gen_0':s'3(0) ⇔ 0'
_gen_0':s'3(+(x, 1)) ⇔ s'(_gen_0':s'3(x))

No more defined symbols left to analyse.

The lowerbound Ω(n²) was proven with the following lemma:
*'(_gen_0':s'3(a), _gen_0':s'3(_n728)) → _gen_0':s'3(*(_n728, a)), rt ∈ Ω(1 + _a988·_n728 + _n728)