```* Step 1: DependencyPairs WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
div(0(),n__s(Y)) -> 0()
div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
geq(X,n__0()) -> true()
geq(n__0(),n__s(Y)) -> false()
geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
if(false(),X,Y) -> activate(Y)
if(true(),X,Y) -> activate(X)
minus(n__0(),Y) -> 0()
minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
s(X) -> n__s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__s/1,true/0}
- Obligation:
runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false,n__0,n__s
,true}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following weak dependency pairs:

Strict DPs
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
div#(0(),n__s(Y)) -> c_5(0#())
div#(s(X),n__s(Y)) -> c_6(if#(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0()))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
Weak DPs

and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
div#(0(),n__s(Y)) -> c_5(0#())
div#(s(X),n__s(Y)) -> c_6(if#(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0()))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
div(0(),n__s(Y)) -> 0()
div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0())
geq(X,n__0()) -> true()
geq(n__0(),n__s(Y)) -> false()
geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y))
if(false(),X,Y) -> activate(Y)
if(true(),X,Y) -> activate(X)
minus(n__0(),Y) -> 0()
minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y))
s(X) -> n__s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,5,6}
by application of
Pre({1,5,6}) = {2,3,7,10,12}.
Here rules are labelled as follows:
1: 0#() -> c_1()
2: activate#(X) -> c_2(X)
3: activate#(n__0()) -> c_3(0#())
4: activate#(n__s(X)) -> c_4(s#(X))
5: geq#(X,n__0()) -> c_7()
6: geq#(n__0(),n__s(Y)) -> c_8()
7: geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
8: if#(false(),X,Y) -> c_10(activate#(Y))
9: if#(true(),X,Y) -> c_11(activate#(X))
10: minus#(n__0(),Y) -> c_12(0#())
11: minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
12: s#(X) -> c_14(X)
* Step 4: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
- Weak DPs:
0#() -> c_1()
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2,7}
by application of
Pre({2,7}) = {1,5,6,8,9}.
Here rules are labelled as follows:
1: activate#(X) -> c_2(X)
2: activate#(n__0()) -> c_3(0#())
3: activate#(n__s(X)) -> c_4(s#(X))
4: geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
5: if#(false(),X,Y) -> c_10(activate#(Y))
6: if#(true(),X,Y) -> c_11(activate#(X))
7: minus#(n__0(),Y) -> c_12(0#())
8: minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
9: s#(X) -> c_14(X)
10: 0#() -> c_1()
11: geq#(X,n__0()) -> c_7()
12: geq#(n__0(),n__s(Y)) -> c_8()
* Step 5: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
activate#(X) -> c_2(X)
activate#(n__s(X)) -> c_4(s#(X))
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Strict TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
- Weak DPs:
0#() -> c_1()
activate#(n__0()) -> c_3(0#())
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
minus#(n__0(),Y) -> c_12(0#())
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(geq#) = {1,2},
uargs(minus#) = {1,2},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [1]
p(activate) = [1] x1 + [0]
p(div) = [0]
p(false) = [0]
p(geq) = [0]
p(if) = [0]
p(minus) = [0]
p(n__0) = [0]
p(n__s) = [1] x1 + [4]
p(s) = [1] x1 + [0]
p(true) = [6]
p(0#) = [0]
p(activate#) = [0]
p(div#) = [0]
p(geq#) = [1] x1 + [1] x2 + [8]
p(if#) = [5] x1 + [0]
p(minus#) = [1] x1 + [1] x2 + [0]
p(s#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [8]
p(c_8) = [12]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [0]

Following rules are strictly oriented:
geq#(n__s(X),n__s(Y)) = [1] X + [1] Y + [16]
> [1] X + [1] Y + [8]
= c_9(geq#(activate(X),activate(Y)))

if#(true(),X,Y) = [30]
> [0]
= c_11(activate#(X))

minus#(n__s(X),n__s(Y)) = [1] X + [1] Y + [8]
> [1] X + [1] Y + [0]
= c_13(minus#(activate(X),activate(Y)))

0() = [1]
> [0]
= n__0()

activate(n__s(X)) = [1] X + [4]
> [1] X + [0]
= s(X)

Following rules are (at-least) weakly oriented:
0#() =  [0]
>= [0]
=  c_1()

activate#(X) =  [0]
>= [0]
=  c_2(X)

activate#(n__0()) =  [0]
>= [0]
=  c_3(0#())

activate#(n__s(X)) =  [0]
>= [0]
=  c_4(s#(X))

geq#(X,n__0()) =  [1] X + [8]
>= [8]
=  c_7()

geq#(n__0(),n__s(Y)) =  [1] Y + [12]
>= [12]
=  c_8()

if#(false(),X,Y) =  [0]
>= [0]
=  c_10(activate#(Y))

minus#(n__0(),Y) =  [1] Y + [0]
>= [0]
=  c_12(0#())

s#(X) =  [0]
>= [0]
=  c_14(X)

activate(X) =  [1] X + [0]
>= [1] X + [0]
=  X

activate(n__0()) =  [0]
>= [1]
=  0()

s(X) =  [1] X + [0]
>= [1] X + [4]
=  n__s(X)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 6: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
activate#(X) -> c_2(X)
activate#(n__s(X)) -> c_4(s#(X))
if#(false(),X,Y) -> c_10(activate#(Y))
s#(X) -> c_14(X)
- Strict TRS:
activate(X) -> X
activate(n__0()) -> 0()
s(X) -> n__s(X)
- Weak DPs:
0#() -> c_1()
activate#(n__0()) -> c_3(0#())
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
- Weak TRS:
0() -> n__0()
activate(n__s(X)) -> s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(geq#) = {1,2},
uargs(minus#) = {1,2},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [4]
p(activate) = [1] x1 + [4]
p(div) = [0]
p(false) = [0]
p(geq) = [0]
p(if) = [0]
p(minus) = [0]
p(n__0) = [4]
p(n__s) = [1] x1 + [4]
p(s) = [1] x1 + [0]
p(true) = [1]
p(0#) = [5]
p(activate#) = [2] x1 + [1]
p(div#) = [0]
p(geq#) = [1] x1 + [1] x2 + [4]
p(if#) = [1] x1 + [2] x2 + [3] x3 + [2]
p(minus#) = [1] x1 + [1] x2 + [1]
p(s#) = [2] x1 + [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [3]
p(c_4) = [1] x1 + [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [1]
p(c_8) = [2]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [3]
p(c_11) = [1] x1 + [2]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [2] x1 + [0]

Following rules are strictly oriented:
activate#(X) = [2] X + [1]
> [0]
= c_2(X)

activate#(n__s(X)) = [2] X + [9]
> [2] X + [0]
= c_4(s#(X))

activate(X) = [1] X + [4]
> [1] X + [0]
= X

activate(n__0()) = [8]
> [4]
= 0()

Following rules are (at-least) weakly oriented:
0#() =  [5]
>= [0]
=  c_1()

activate#(n__0()) =  [9]
>= [8]
=  c_3(0#())

geq#(X,n__0()) =  [1] X + [8]
>= [1]
=  c_7()

geq#(n__0(),n__s(Y)) =  [1] Y + [12]
>= [2]
=  c_8()

geq#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [12]
>= [1] X + [1] Y + [12]
=  c_9(geq#(activate(X),activate(Y)))

if#(false(),X,Y) =  [2] X + [3] Y + [2]
>= [2] Y + [4]
=  c_10(activate#(Y))

if#(true(),X,Y) =  [2] X + [3] Y + [3]
>= [2] X + [3]
=  c_11(activate#(X))

minus#(n__0(),Y) =  [1] Y + [5]
>= [5]
=  c_12(0#())

minus#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [9]
>= [1] X + [1] Y + [9]
=  c_13(minus#(activate(X),activate(Y)))

s#(X) =  [2] X + [0]
>= [2] X + [0]
=  c_14(X)

0() =  [4]
>= [4]
=  n__0()

activate(n__s(X)) =  [1] X + [8]
>= [1] X + [0]
=  s(X)

s(X) =  [1] X + [0]
>= [1] X + [4]
=  n__s(X)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 7: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
if#(false(),X,Y) -> c_10(activate#(Y))
s#(X) -> c_14(X)
- Strict TRS:
s(X) -> n__s(X)
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(geq#) = {1,2},
uargs(minus#) = {1,2},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [4]
p(activate) = [1] x1 + [5]
p(div) = [2] x2 + [0]
p(false) = [2]
p(geq) = [0]
p(if) = [2] x3 + [0]
p(minus) = [0]
p(n__0) = [2]
p(n__s) = [1] x1 + [7]
p(s) = [1] x1 + [4]
p(true) = [0]
p(0#) = [1]
p(activate#) = [1]
p(div#) = [1] x2 + [4]
p(geq#) = [1] x1 + [1] x2 + [1]
p(if#) = [4] x1 + [2] x3 + [7]
p(minus#) = [1] x1 + [1] x2 + [1]
p(s#) = [1]
p(c_1) = [0]
p(c_2) = [1]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [2] x1 + [0]
p(c_6) = [4]
p(c_7) = [0]
p(c_8) = [1]
p(c_9) = [1] x1 + [4]
p(c_10) = [1] x1 + [1]
p(c_11) = [1] x1 + [6]
p(c_12) = [1] x1 + [2]
p(c_13) = [1] x1 + [1]
p(c_14) = [0]

Following rules are strictly oriented:
if#(false(),X,Y) = [2] Y + [15]
> [2]
= c_10(activate#(Y))

s#(X) = [1]
> [0]
= c_14(X)

Following rules are (at-least) weakly oriented:
0#() =  [1]
>= [0]
=  c_1()

activate#(X) =  [1]
>= [1]
=  c_2(X)

activate#(n__0()) =  [1]
>= [1]
=  c_3(0#())

activate#(n__s(X)) =  [1]
>= [1]
=  c_4(s#(X))

geq#(X,n__0()) =  [1] X + [3]
>= [0]
=  c_7()

geq#(n__0(),n__s(Y)) =  [1] Y + [10]
>= [1]
=  c_8()

geq#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [15]
>= [1] X + [1] Y + [15]
=  c_9(geq#(activate(X),activate(Y)))

if#(true(),X,Y) =  [2] Y + [7]
>= [7]
=  c_11(activate#(X))

minus#(n__0(),Y) =  [1] Y + [3]
>= [3]
=  c_12(0#())

minus#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [15]
>= [1] X + [1] Y + [12]
=  c_13(minus#(activate(X),activate(Y)))

0() =  [4]
>= [2]
=  n__0()

activate(X) =  [1] X + [5]
>= [1] X + [0]
=  X

activate(n__0()) =  [7]
>= [4]
=  0()

activate(n__s(X)) =  [1] X + [12]
>= [1] X + [4]
=  s(X)

s(X) =  [1] X + [4]
>= [1] X + [7]
=  n__s(X)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 8: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
s(X) -> n__s(X)
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(geq#) = {1,2},
uargs(minus#) = {1,2},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_9) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1},
uargs(c_13) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(0) = [4]
p(activate) = [1] x1 + [4]
p(div) = [0]
p(false) = [0]
p(geq) = [0]
p(if) = [0]
p(minus) = [0]
p(n__0) = [1]
p(n__s) = [1] x1 + [4]
p(s) = [1] x1 + [6]
p(true) = [0]
p(0#) = [1]
p(activate#) = [2]
p(div#) = [0]
p(geq#) = [1] x1 + [1] x2 + [5]
p(if#) = [2]
p(minus#) = [1] x1 + [1] x2 + [0]
p(s#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [0]
p(c_6) = [0]
p(c_7) = [0]
p(c_8) = [2]
p(c_9) = [1] x1 + [0]
p(c_10) = [1] x1 + [0]
p(c_11) = [1] x1 + [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [1] x1 + [0]
p(c_14) = [0]

Following rules are strictly oriented:
s(X) = [1] X + [6]
> [1] X + [4]
= n__s(X)

Following rules are (at-least) weakly oriented:
0#() =  [1]
>= [0]
=  c_1()

activate#(X) =  [2]
>= [0]
=  c_2(X)

activate#(n__0()) =  [2]
>= [1]
=  c_3(0#())

activate#(n__s(X)) =  [2]
>= [0]
=  c_4(s#(X))

geq#(X,n__0()) =  [1] X + [6]
>= [0]
=  c_7()

geq#(n__0(),n__s(Y)) =  [1] Y + [10]
>= [2]
=  c_8()

geq#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [13]
>= [1] X + [1] Y + [13]
=  c_9(geq#(activate(X),activate(Y)))

if#(false(),X,Y) =  [2]
>= [2]
=  c_10(activate#(Y))

if#(true(),X,Y) =  [2]
>= [2]
=  c_11(activate#(X))

minus#(n__0(),Y) =  [1] Y + [1]
>= [1]
=  c_12(0#())

minus#(n__s(X),n__s(Y)) =  [1] X + [1] Y + [8]
>= [1] X + [1] Y + [8]
=  c_13(minus#(activate(X),activate(Y)))

s#(X) =  [0]
>= [0]
=  c_14(X)

0() =  [4]
>= [1]
=  n__0()

activate(X) =  [1] X + [4]
>= [1] X + [0]
=  X

activate(n__0()) =  [5]
>= [4]
=  0()

activate(n__s(X)) =  [1] X + [8]
>= [1] X + [6]
=  s(X)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 9: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
0#() -> c_1()
activate#(X) -> c_2(X)
activate#(n__0()) -> c_3(0#())
activate#(n__s(X)) -> c_4(s#(X))
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
geq#(n__s(X),n__s(Y)) -> c_9(geq#(activate(X),activate(Y)))
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
minus#(n__0(),Y) -> c_12(0#())
minus#(n__s(X),n__s(Y)) -> c_13(minus#(activate(X),activate(Y)))
s#(X) -> c_14(X)
- Weak TRS:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
- Signature:
{0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1,0#/0,activate#/1,div#/2,geq#/2,if#/3,minus#/2,s#/1} / {false/0
,n__0/0,n__s/1,true/0,c_1/0,c_2/1,c_3/1,c_4/1,c_5/1,c_6/1,c_7/0,c_8/0,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1
,c_14/1}
- Obligation:
runtime complexity wrt. defined symbols {0#,activate#,div#,geq#,if#,minus#,s#} and constructors {false,n__0
,n__s,true}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))
```