The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^2, INF).

(0) Obligation:

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

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Rewrite Strategy: FULL

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

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

minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

S is empty.
Rewrite Strategy: FULL

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
minus, activate, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(6) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
activate, minus, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Induction Base:
activate(gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
gen_n__0:n__s:n__minus:n__div3_3(0)

Induction Step:
activate(gen_n__0:n__s:n__minus:n__div3_3(+(n5_3, 1))) →_R^Ω(1)
s(activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3))) →_IH
s(gen_n__0:n__s:n__minus:n__div3_3(c6_3)) →_R^Ω(1)
n__s(gen_n__0:n__s:n__minus:n__div3_3(n5_3))

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

(8) Complex Obligation (BEST)

(9) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
minus, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Induction Base:
minus(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
0' →_R^Ω(1)
n__0

Induction Step:
minus(gen_n__0:n__s:n__minus:n__div3_3(+(n845_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n845_3, 1))) →_R^Ω(1)
minus(activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3))) →_L^{Ω(1 + n845₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3))) →_L^{Ω(1 + n845₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) →_IH
gen_n__0:n__s:n__minus:n__div3_3(0)

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

(11) Complex Obligation (BEST)

(12) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
geq, activate

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Induction Base:
geq(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
true

Induction Step:
geq(gen_n__0:n__s:n__minus:n__div3_3(+(n1969_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n1969_3, 1))) →_R^Ω(1)
geq(activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3))) →_L^{Ω(1 + n1969₃)}
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3))) →_L^{Ω(1 + n1969₃)}
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) →_IH
true

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

(14) Complex Obligation (BEST)

(15) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
activate, minus

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)

Induction Base:
activate(gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
gen_n__0:n__s:n__minus:n__div3_3(0)

Induction Step:
activate(gen_n__0:n__s:n__minus:n__div3_3(+(n2634_3, 1))) →_R^Ω(1)
s(activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3))) →_IH
s(gen_n__0:n__s:n__minus:n__div3_3(c2635_3)) →_R^Ω(1)
n__s(gen_n__0:n__s:n__minus:n__div3_3(n2634_3))

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

(17) Complex Obligation (BEST)

(18) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
minus

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

Induction Base:
minus(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
0' →_R^Ω(1)
n__0

Induction Step:
minus(gen_n__0:n__s:n__minus:n__div3_3(+(n3500_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n3500_3, 1))) →_R^Ω(1)
minus(activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3))) →_L^{Ω(1 + n3500₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3))) →_L^{Ω(1 + n3500₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) →_IH
gen_n__0:n__s:n__minus:n__div3_3(0)

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

(20) Complex Obligation (BEST)

(21) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(22) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

(23) BOUNDS(n^2, INF)

(24) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(25) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

(26) BOUNDS(n^2, INF)

(27) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(28) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(29) BOUNDS(n^2, INF)

(30) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(32) BOUNDS(n^2, INF)

(33) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(34) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(35) BOUNDS(n^2, INF)

(36) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(37) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

(38) BOUNDS(n^1, INF)