*** 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__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
add(0(),X) -> X
add(s(X),Y) -> s(add(X,Y))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
if(false(),X,Y) -> activate(Y)
if(true(),X,Y) -> activate(X)
p(X) -> n__p(X)
p(s(X)) -> X
prod(X1,X2) -> n__prod(X1,X2)
prod(0(),X) -> 0()
prod(s(X),Y) -> add(Y,prod(X,Y))
s(X) -> n__s(X)
zero(0()) -> true()
zero(s(X)) -> false()
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0}
Obligation:
Innermost
basic terms: {0,activate,add,fact,if,p,prod,s,zero}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
InnermostRuleRemoval
Proof:
Arguments of following rules are not normal-forms.
add(0(),X) -> X
add(s(X),Y) -> s(add(X,Y))
p(s(X)) -> X
prod(0(),X) -> 0()
prod(s(X),Y) -> add(Y,prod(X,Y))
zero(0()) -> true()
zero(s(X)) -> false()
All above mentioned rules can be savely removed.
*** 1.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__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
if(false(),X,Y) -> activate(Y)
if(true(),X,Y) -> activate(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0}
Obligation:
Innermost
basic terms: {0,activate,add,fact,if,p,prod,s,zero}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
DependencyPairs {dpKind_ = WIDP}
Proof:
We add the following weak innermost dependency pairs:
Strict DPs
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
Weak DPs
and mark the set of starting terms.
*** 1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
Strict TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
if(false(),X,Y) -> activate(Y)
if(true(),X,Y) -> activate(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,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__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
*** 1.1.1.1 Progress [(O(1),O(n^1))] ***
Considered Problem:
Strict DP Rules:
0#() -> c_1()
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
Strict TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnTrs}
Proof:
The weightgap principle applies using the following constant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(fact) = {1},
uargs(p) = {1},
uargs(prod) = {1,2},
uargs(s) = {1},
uargs(fact#) = {1},
uargs(p#) = {1},
uargs(prod#) = {1,2},
uargs(s#) = {1},
uargs(c_3) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_7) = {1},
uargs(c_10) = {1},
uargs(c_11) = {1}
Following symbols are considered usable:
{}
TcT has computed the following interpretation:
p(0) = [1]
p(activate) = [3] x1 + [2]
p(add) = [4] x1 + [1] x2 + [0]
p(fact) = [1] x1 + [2]
p(false) = [0]
p(if) = [1]
p(n__0) = [0]
p(n__fact) = [1] x1 + [1]
p(n__p) = [1] x1 + [1]
p(n__prod) = [1] x1 + [1] x2 + [2]
p(n__s) = [1] x1 + [1]
p(p) = [1] x1 + [2]
p(prod) = [1] x1 + [1] x2 + [3]
p(s) = [1] x1 + [2]
p(true) = [2]
p(zero) = [0]
p(0#) = [4]
p(activate#) = [3] x1 + [0]
p(add#) = [1] x2 + [0]
p(fact#) = [1] x1 + [5]
p(if#) = [4] x1 + [3] x2 + [3] x3 + [0]
p(p#) = [1] x1 + [6]
p(prod#) = [1] x1 + [1] x2 + [0]
p(s#) = [1] x1 + [0]
p(zero#) = [1] x1 + [1]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [1] x1 + [0]
p(c_4) = [1] x1 + [1]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [4]
p(c_7) = [1] x1 + [1]
p(c_8) = [1]
p(c_9) = [4]
p(c_10) = [1] x1 + [0]
p(c_11) = [1] x1 + [4]
p(c_12) = [0]
p(c_13) = [1]
p(c_14) = [0]
Following rules are strictly oriented:
0#() = [4]
> [0]
= c_1()
fact#(X) = [1] X + [5]
> [1]
= c_8(if#(zero(X)
,n__s(n__0())
,n__prod(X,n__fact(n__p(X)))))
fact#(X) = [1] X + [5]
> [4]
= c_9()
if#(true(),X,Y) = [3] X + [3] Y + [8]
> [3] X + [4]
= c_11(activate#(X))
p#(X) = [1] X + [6]
> [0]
= c_12()
0() = [1]
> [0]
= n__0()
activate(X) = [3] X + [2]
> [1] X + [0]
= X
activate(n__0()) = [2]
> [1]
= 0()
activate(n__fact(X)) = [3] X + [5]
> [3] X + [4]
= fact(activate(X))
activate(n__p(X)) = [3] X + [5]
> [3] X + [4]
= p(activate(X))
activate(n__prod(X1,X2)) = [3] X1 + [3] X2 + [8]
> [3] X1 + [3] X2 + [7]
= prod(activate(X1),activate(X2))
activate(n__s(X)) = [3] X + [5]
> [3] X + [4]
= s(activate(X))
fact(X) = [1] X + [2]
> [1]
= if(zero(X)
,n__s(n__0())
,n__prod(X,n__fact(n__p(X))))
fact(X) = [1] X + [2]
> [1] X + [1]
= n__fact(X)
p(X) = [1] X + [2]
> [1] X + [1]
= n__p(X)
prod(X1,X2) = [1] X1 + [1] X2 + [3]
> [1] X1 + [1] X2 + [2]
= n__prod(X1,X2)
s(X) = [1] X + [2]
> [1] X + [1]
= n__s(X)
Following rules are (at-least) weakly oriented:
activate#(X) = [3] X + [0]
>= [0]
= c_2()
activate#(n__0()) = [0]
>= [4]
= c_3(0#())
activate#(n__fact(X)) = [3] X + [3]
>= [3] X + [8]
= c_4(fact#(activate(X)))
activate#(n__p(X)) = [3] X + [3]
>= [3] X + [8]
= c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) = [3] X1 + [3] X2 + [6]
>= [3] X1 + [3] X2 + [8]
= c_6(prod#(activate(X1)
,activate(X2)))
activate#(n__s(X)) = [3] X + [3]
>= [3] X + [3]
= c_7(s#(activate(X)))
if#(false(),X,Y) = [3] X + [3] Y + [0]
>= [3] Y + [0]
= c_10(activate#(Y))
prod#(X1,X2) = [1] X1 + [1] X2 + [0]
>= [1]
= c_13()
s#(X) = [1] X + [0]
>= [0]
= c_14()
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
if#(false(),X,Y) -> c_10(activate#(Y))
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
Strict TRS Rules:
Weak DP Rules:
0#() -> c_1()
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
Weak TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{8,9}
by application of
Pre({8,9}) = {5,6}.
Here rules are labelled as follows:
1: activate#(X) -> c_2()
2: activate#(n__0()) -> c_3(0#())
3: activate#(n__fact(X)) ->
c_4(fact#(activate(X)))
4: activate#(n__p(X)) ->
c_5(p#(activate(X)))
5: activate#(n__prod(X1,X2)) ->
c_6(prod#(activate(X1)
,activate(X2)))
6: activate#(n__s(X)) ->
c_7(s#(activate(X)))
7: if#(false(),X,Y) ->
c_10(activate#(Y))
8: prod#(X1,X2) -> c_13()
9: s#(X) -> c_14()
10: 0#() -> c_1()
11: fact#(X) -> c_8(if#(zero(X)
,n__s(n__0())
,n__prod(X,n__fact(n__p(X)))))
12: fact#(X) -> c_9()
13: if#(true(),X,Y) ->
c_11(activate#(X))
14: p#(X) -> c_12()
*** 1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
if#(false(),X,Y) -> c_10(activate#(Y))
Strict TRS Rules:
Weak DP Rules:
0#() -> c_1()
fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
fact#(X) -> c_9()
if#(true(),X,Y) -> c_11(activate#(X))
p#(X) -> c_12()
prod#(X1,X2) -> c_13()
s#(X) -> c_14()
Weak TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:activate#(X) -> c_2()
2:S:activate#(n__0()) -> c_3(0#())
-->_1 0#() -> c_1():8
3:S:activate#(n__fact(X)) -> c_4(fact#(activate(X)))
-->_1 fact#(X) -> c_9():10
-->_1 fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))):9
4:S:activate#(n__p(X)) -> c_5(p#(activate(X)))
-->_1 p#(X) -> c_12():12
5:S:activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
-->_1 prod#(X1,X2) -> c_13():13
6:S:activate#(n__s(X)) -> c_7(s#(activate(X)))
-->_1 s#(X) -> c_14():14
7:S:if#(false(),X,Y) -> c_10(activate#(Y))
-->_1 activate#(n__s(X)) -> c_7(s#(activate(X))):6
-->_1 activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2))):5
-->_1 activate#(n__p(X)) -> c_5(p#(activate(X))):4
-->_1 activate#(n__fact(X)) -> c_4(fact#(activate(X))):3
-->_1 activate#(n__0()) -> c_3(0#()):2
-->_1 activate#(X) -> c_2():1
8:W:0#() -> c_1()
9:W:fact#(X) -> c_8(if#(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X)))))
10:W:fact#(X) -> c_9()
11:W:if#(true(),X,Y) -> c_11(activate#(X))
-->_1 activate#(n__s(X)) -> c_7(s#(activate(X))):6
-->_1 activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2))):5
-->_1 activate#(n__p(X)) -> c_5(p#(activate(X))):4
-->_1 activate#(n__fact(X)) -> c_4(fact#(activate(X))):3
-->_1 activate#(n__0()) -> c_3(0#()):2
-->_1 activate#(X) -> c_2():1
12:W:p#(X) -> c_12()
13:W:prod#(X1,X2) -> c_13()
14:W:s#(X) -> c_14()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
14: s#(X) -> c_14()
13: prod#(X1,X2) -> c_13()
12: p#(X) -> c_12()
9: fact#(X) -> c_8(if#(zero(X)
,n__s(n__0())
,n__prod(X,n__fact(n__p(X)))))
10: fact#(X) -> c_9()
8: 0#() -> c_1()
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3(0#())
activate#(n__fact(X)) -> c_4(fact#(activate(X)))
activate#(n__p(X)) -> c_5(p#(activate(X)))
activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
activate#(n__s(X)) -> c_7(s#(activate(X)))
if#(false(),X,Y) -> c_10(activate#(Y))
Strict TRS Rules:
Weak DP Rules:
if#(true(),X,Y) -> c_11(activate#(X))
Weak TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1,c_6/1,c_7/1,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:activate#(X) -> c_2()
2:S:activate#(n__0()) -> c_3(0#())
3:S:activate#(n__fact(X)) -> c_4(fact#(activate(X)))
4:S:activate#(n__p(X)) -> c_5(p#(activate(X)))
5:S:activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2)))
6:S:activate#(n__s(X)) -> c_7(s#(activate(X)))
7:S:if#(false(),X,Y) -> c_10(activate#(Y))
-->_1 activate#(n__s(X)) -> c_7(s#(activate(X))):6
-->_1 activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2))):5
-->_1 activate#(n__p(X)) -> c_5(p#(activate(X))):4
-->_1 activate#(n__fact(X)) -> c_4(fact#(activate(X))):3
-->_1 activate#(n__0()) -> c_3(0#()):2
-->_1 activate#(X) -> c_2():1
11:W:if#(true(),X,Y) -> c_11(activate#(X))
-->_1 activate#(n__s(X)) -> c_7(s#(activate(X))):6
-->_1 activate#(n__prod(X1,X2)) -> c_6(prod#(activate(X1),activate(X2))):5
-->_1 activate#(n__p(X)) -> c_5(p#(activate(X))):4
-->_1 activate#(n__fact(X)) -> c_4(fact#(activate(X))):3
-->_1 activate#(n__0()) -> c_3(0#()):2
-->_1 activate#(X) -> c_2():1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
activate#(n__0()) -> c_3()
activate#(n__fact(X)) -> c_4()
activate#(n__p(X)) -> c_5()
activate#(n__prod(X1,X2)) -> c_6()
activate#(n__s(X)) -> c_7()
*** 1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3()
activate#(n__fact(X)) -> c_4()
activate#(n__p(X)) -> c_5()
activate#(n__prod(X1,X2)) -> c_6()
activate#(n__s(X)) -> c_7()
if#(false(),X,Y) -> c_10(activate#(Y))
Strict TRS Rules:
Weak DP Rules:
if#(true(),X,Y) -> c_11(activate#(X))
Weak TRS Rules:
0() -> n__0()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__fact(X)) -> fact(activate(X))
activate(n__p(X)) -> p(activate(X))
activate(n__prod(X1,X2)) -> prod(activate(X1),activate(X2))
activate(n__s(X)) -> s(activate(X))
fact(X) -> if(zero(X),n__s(n__0()),n__prod(X,n__fact(n__p(X))))
fact(X) -> n__fact(X)
p(X) -> n__p(X)
prod(X1,X2) -> n__prod(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3()
activate#(n__fact(X)) -> c_4()
activate#(n__p(X)) -> c_5()
activate#(n__prod(X1,X2)) -> c_6()
activate#(n__s(X)) -> c_7()
if#(false(),X,Y) -> c_10(activate#(Y))
if#(true(),X,Y) -> c_11(activate#(X))
*** 1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3()
activate#(n__fact(X)) -> c_4()
activate#(n__p(X)) -> c_5()
activate#(n__prod(X1,X2)) -> c_6()
activate#(n__s(X)) -> c_7()
if#(false(),X,Y) -> c_10(activate#(Y))
Strict TRS Rules:
Weak DP Rules:
if#(true(),X,Y) -> c_11(activate#(X))
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
RemoveHeads
Proof:
Consider the dependency graph
1:S:activate#(X) -> c_2()
2:S:activate#(n__0()) -> c_3()
3:S:activate#(n__fact(X)) -> c_4()
4:S:activate#(n__p(X)) -> c_5()
5:S:activate#(n__prod(X1,X2)) -> c_6()
6:S:activate#(n__s(X)) -> c_7()
7:S:if#(false(),X,Y) -> c_10(activate#(Y))
-->_1 activate#(n__s(X)) -> c_7():6
-->_1 activate#(n__prod(X1,X2)) -> c_6():5
-->_1 activate#(n__p(X)) -> c_5():4
-->_1 activate#(n__fact(X)) -> c_4():3
-->_1 activate#(n__0()) -> c_3():2
-->_1 activate#(X) -> c_2():1
8:W:if#(true(),X,Y) -> c_11(activate#(X))
-->_1 activate#(n__s(X)) -> c_7():6
-->_1 activate#(n__prod(X1,X2)) -> c_6():5
-->_1 activate#(n__p(X)) -> c_5():4
-->_1 activate#(n__fact(X)) -> c_4():3
-->_1 activate#(n__0()) -> c_3():2
-->_1 activate#(X) -> c_2():1
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(7,if#(false(),X,Y) -> c_10(activate#(Y))),(8,if#(true(),X,Y) -> c_11(activate#(X)))]
*** 1.1.1.1.1.1.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
activate#(X) -> c_2()
activate#(n__0()) -> c_3()
activate#(n__fact(X)) -> c_4()
activate#(n__p(X)) -> c_5()
activate#(n__prod(X1,X2)) -> c_6()
activate#(n__s(X)) -> c_7()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
RemoveHeads
Proof:
Consider the dependency graph
1:S:activate#(X) -> c_2()
2:S:activate#(n__0()) -> c_3()
3:S:activate#(n__fact(X)) -> c_4()
4:S:activate#(n__p(X)) -> c_5()
5:S:activate#(n__prod(X1,X2)) -> c_6()
6:S:activate#(n__s(X)) -> c_7()
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(1,activate#(X) -> c_2()),(2,activate#(n__0()) -> c_3()),(3,activate#(n__fact(X)) -> c_4()),(4,activate#(n__p(X)) -> c_5()),(5,activate#(n__prod(X1,X2)) -> c_6()),(6,activate#(n__s(X)) -> c_7())]
*** 1.1.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:
Weak TRS Rules:
Signature:
{0/0,activate/1,add/2,fact/1,if/3,p/1,prod/2,s/1,zero/1,0#/0,activate#/1,add#/2,fact#/1,if#/3,p#/1,prod#/2,s#/1,zero#/1} / {false/0,n__0/0,n__fact/1,n__p/1,n__prod/2,n__s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0,c_8/1,c_9/0,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0}
Obligation:
Innermost
basic terms: {0#,activate#,add#,fact#,if#,p#,prod#,s#,zero#}/{false,n__0,n__fact,n__p,n__prod,n__s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).