*** 1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
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)
Weak DP Rules:
Weak TRS Rules:
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:
Full
basic terms: {0,activate,div,geq,if,minus,s}/{false,n__0,n__s,true}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
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.
*** 1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
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 Rules:
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)
Weak DP Rules:
Weak TRS Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
UsableRules
Proof:
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)
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
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 Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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)
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
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 Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
Weak DP Rules:
0#() -> c_1()
geq#(X,n__0()) -> c_7()
geq#(n__0(),n__s(Y)) -> c_8()
Weak TRS Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
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()
*** 1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
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 Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__s(X)) -> s(X)
s(X) -> n__s(X)
Weak DP Rules:
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#())
Weak TRS Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
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 Rules:
activate(X) -> X
activate(n__0()) -> 0()
s(X) -> n__s(X)
Weak DP Rules:
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 Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
if#(false(),X,Y) -> c_10(activate#(Y))
s#(X) -> c_14(X)
Strict TRS Rules:
s(X) -> n__s(X)
Weak DP Rules:
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 Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
s(X) -> n__s(X)
Weak DP Rules:
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 Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
Proof:
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:
{}
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.
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
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 Rules:
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:
Full
basic terms: {0#,activate#,div#,geq#,if#,minus#,s#}/{false,n__0,n__s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).