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

minus(X, 0) → X
minus(s(X), s(Y)) → p(minus(X, Y))
p(s(X)) → X
div(0, s(Y)) → 0
div(s(X), s(Y)) → s(div(minus(X, Y), s(Y)))

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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


minus'(X, 0') → X
minus'(s'(X), s'(Y)) → p'(minus'(X, Y))
p'(s'(X)) → X
div'(0', s'(Y)) → 0'
div'(s'(X), s'(Y)) → s'(div'(minus'(X, Y), s'(Y)))

Rewrite Strategy: INNERMOST

Infered types.

Rules:
minus'(X, 0') → X
minus'(s'(X), s'(Y)) → p'(minus'(X, Y))
p'(s'(X)) → X
div'(0', s'(Y)) → 0'
div'(s'(X), s'(Y)) → s'(div'(minus'(X, Y), s'(Y)))

Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_gen_0':s'2 :: Nat → 0':s'

Heuristically decided to analyse the following defined symbols:
minus', div'

They will be analysed ascendingly in the following order:
minus' < div'

Rules:
minus'(X, 0') → X
minus'(s'(X), s'(Y)) → p'(minus'(X, Y))
p'(s'(X)) → X
div'(0', s'(Y)) → 0'
div'(s'(X), s'(Y)) → s'(div'(minus'(X, Y), s'(Y)))

Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_gen_0':s'2 :: Nat → 0':s'

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

The following defined symbols remain to be analysed:
minus', div'

They will be analysed ascendingly in the following order:
minus' < div'

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

Induction Base:
minus'(_gen_0':s'2(+(1, 0)), _gen_0':s'2(+(1, 0)))

Induction Step:
minus'(_gen_0':s'2(+(1, +(_$n5, 1))), _gen_0':s'2(+(1, +(_$n5, 1)))) →RΩ(1)
p'(minus'(_gen_0':s'2(+(1, _$n5)), _gen_0':s'2(+(1, _$n5)))) →IH
p'(_*3)

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

Rules:
minus'(X, 0') → X
minus'(s'(X), s'(Y)) → p'(minus'(X, Y))
p'(s'(X)) → X
div'(0', s'(Y)) → 0'
div'(s'(X), s'(Y)) → s'(div'(minus'(X, Y), s'(Y)))

Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_gen_0':s'2 :: Nat → 0':s'

Lemmas:
minus'(_gen_0':s'2(+(1, _n4)), _gen_0':s'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)

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

The following defined symbols remain to be analysed:
div'

Proved the following rewrite lemma:
div'(_gen_0':s'2(_n964), _gen_0':s'2(1)) → _gen_0':s'2(_n964), rt ∈ Ω(1 + n964)

Induction Base:
div'(_gen_0':s'2(0), _gen_0':s'2(1)) →RΩ(1)
0'

Induction Step:
div'(_gen_0':s'2(+(_$n965, 1)), _gen_0':s'2(1)) →RΩ(1)
s'(div'(minus'(_gen_0':s'2(_$n965), _gen_0':s'2(0)), s'(_gen_0':s'2(0)))) →RΩ(1)
s'(div'(_gen_0':s'2(_$n965), s'(_gen_0':s'2(0)))) →IH
s'(_gen_0':s'2(_$n965))

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

Rules:
minus'(X, 0') → X
minus'(s'(X), s'(Y)) → p'(minus'(X, Y))
p'(s'(X)) → X
div'(0', s'(Y)) → 0'
div'(s'(X), s'(Y)) → s'(div'(minus'(X, Y), s'(Y)))

Types:
minus' :: 0':s' → 0':s' → 0':s'
0' :: 0':s'
s' :: 0':s' → 0':s'
p' :: 0':s' → 0':s'
div' :: 0':s' → 0':s' → 0':s'
_hole_0':s'1 :: 0':s'
_gen_0':s'2 :: Nat → 0':s'

Lemmas:
minus'(_gen_0':s'2(+(1, _n4)), _gen_0':s'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
div'(_gen_0':s'2(_n964), _gen_0':s'2(1)) → _gen_0':s'2(_n964), rt ∈ Ω(1 + n964)

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

No more defined symbols left to analyse.

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