### (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)
0n__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) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(2n):
The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →+ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].

The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →+ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].

### (3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

### (4) 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

Infered types.

### (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

### (7) 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

### (8) 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

### (9) 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 + n53)

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

### (11) 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 + n53)

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

### (12) 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 + n8453 + n84532)

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

### (14) 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 + n53)
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 + n8453 + n84532)

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

### (15) 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 + n19693 + n196932)

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

### (17) 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 + n53)
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 + n8453 + n84532)
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 + n19693 + n196932)

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

### (18) 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 + n26343)

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

### (20) 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 + n26343)
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 + n8453 + n84532)
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 + n19693 + n196932)

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

### (21) 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 + n35003 + n350032)

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

### (23) 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 + n26343)
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 + n35003 + n350032)
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 + n19693 + n196932)

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.

### (24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n2) 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 + n35003 + n350032)

### (26) 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 + n26343)
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 + n35003 + n350032)
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 + n19693 + n196932)

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.

### (27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n2) 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 + n35003 + n350032)

### (29) 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 + n26343)
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 + n8453 + n84532)
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 + n19693 + n196932)

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.

### (30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n2) 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 + n8453 + n84532)

### (32) 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 + n53)
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 + n8453 + n84532)
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 + n19693 + n196932)

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.

### (33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n2) 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 + n8453 + n84532)

### (35) 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 + n53)
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 + n8453 + n84532)

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.

### (36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n2) 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 + n8453 + n84532)

### (38) 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 + n53)

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.

### (39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n1) 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 + n53)