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'

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'

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 ircR ∈ Ω(n).

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'

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 ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).

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'

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 ircR ∈ Ω(n).

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'

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 ircR ∈ Ω(n).

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'

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

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'.

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'

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

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 Ω(n2) 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)