*** 1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
goal(xs,ys) -> mul0(xs,ys)
isZero(C(x,y)) -> False()
isZero(Z()) -> True()
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
second(C(x,y)) -> y
Weak DP Rules:
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1} / {C/2,False/0,S/0,True/0,Z/0}
Obligation:
Innermost
basic terms: {add0,goal,isZero,mul0,second}/{C,False,S,True,Z}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
add0#(Z(),y) -> c_2()
goal#(xs,ys) -> c_3(mul0#(xs,ys))
isZero#(C(x,y)) -> c_4()
isZero#(Z()) -> c_5()
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
mul0#(Z(),y) -> c_7()
second#(C(x,y)) -> c_8()
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
add0#(Z(),y) -> c_2()
goal#(xs,ys) -> c_3(mul0#(xs,ys))
isZero#(C(x,y)) -> c_4()
isZero#(Z()) -> c_5()
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
mul0#(Z(),y) -> c_7()
second#(C(x,y)) -> c_8()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
goal(xs,ys) -> mul0(xs,ys)
isZero(C(x,y)) -> False()
isZero(Z()) -> True()
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
second(C(x,y)) -> y
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
add0#(Z(),y) -> c_2()
goal#(xs,ys) -> c_3(mul0#(xs,ys))
isZero#(C(x,y)) -> c_4()
isZero#(Z()) -> c_5()
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
mul0#(Z(),y) -> c_7()
second#(C(x,y)) -> c_8()
*** 1.1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
add0#(Z(),y) -> c_2()
goal#(xs,ys) -> c_3(mul0#(xs,ys))
isZero#(C(x,y)) -> c_4()
isZero#(Z()) -> c_5()
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
mul0#(Z(),y) -> c_7()
second#(C(x,y)) -> c_8()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{2,4,5,7,8}
by application of
Pre({2,4,5,7,8}) = {1,3,6}.
Here rules are labelled as follows:
1: add0#(C(x,y),y') -> c_1(add0#(y
,C(S(),y')))
2: add0#(Z(),y) -> c_2()
3: goal#(xs,ys) -> c_3(mul0#(xs
,ys))
4: isZero#(C(x,y)) -> c_4()
5: isZero#(Z()) -> c_5()
6: mul0#(C(x,y),y') ->
c_6(add0#(mul0(y,y'),y')
,mul0#(y,y'))
7: mul0#(Z(),y) -> c_7()
8: second#(C(x,y)) -> c_8()
*** 1.1.1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
goal#(xs,ys) -> c_3(mul0#(xs,ys))
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
add0#(Z(),y) -> c_2()
isZero#(C(x,y)) -> c_4()
isZero#(Z()) -> c_5()
mul0#(Z(),y) -> c_7()
second#(C(x,y)) -> c_8()
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
-->_1 add0#(Z(),y) -> c_2():4
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):1
2:S:goal#(xs,ys) -> c_3(mul0#(xs,ys))
-->_1 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):3
-->_1 mul0#(Z(),y) -> c_7():7
3:S:mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
-->_2 mul0#(Z(),y) -> c_7():7
-->_1 add0#(Z(),y) -> c_2():4
-->_2 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):3
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):1
4:W:add0#(Z(),y) -> c_2()
5:W:isZero#(C(x,y)) -> c_4()
6:W:isZero#(Z()) -> c_5()
7:W:mul0#(Z(),y) -> c_7()
8:W:second#(C(x,y)) -> c_8()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
8: second#(C(x,y)) -> c_8()
6: isZero#(Z()) -> c_5()
5: isZero#(C(x,y)) -> c_4()
7: mul0#(Z(),y) -> c_7()
4: add0#(Z(),y) -> c_2()
*** 1.1.1.1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
goal#(xs,ys) -> c_3(mul0#(xs,ys))
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveHeads
Proof:
Consider the dependency graph
1:S:add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):1
2:S:goal#(xs,ys) -> c_3(mul0#(xs,ys))
-->_1 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):3
3:S:mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
-->_2 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):3
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):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).
[(2,goal#(xs,ys) -> c_3(mul0#(xs,ys)))]
*** 1.1.1.1.1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Problem (S)
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
*** 1.1.1.1.1.1.1 Progress [(?,O(n^3))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
Proof:
We decompose the input problem according to the dependency graph into the upper component
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
and a lower component
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Further, following extension rules are added to the lower component.
mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
mul0#(C(x,y),y') -> mul0#(y,y')
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: mul0#(C(x,y),y') ->
c_6(add0#(mul0(y,y'),y')
,mul0#(y,y'))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_6) = {1,2}
Following symbols are considered usable:
{add0#,goal#,isZero#,mul0#,second#}
TcT has computed the following interpretation:
p(C) = [1] x1 + [1] x2 + [2]
p(False) = [0]
p(S) = [0]
p(True) = [0]
p(Z) = [3]
p(add0) = [8] x1 + [0]
p(goal) = [0]
p(isZero) = [0]
p(mul0) = [3] x1 + [1] x2 + [0]
p(second) = [0]
p(add0#) = [2]
p(goal#) = [0]
p(isZero#) = [0]
p(mul0#) = [9] x1 + [4]
p(second#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [1] x1 + [1] x2 + [15]
p(c_7) = [1]
p(c_8) = [2]
Following rules are strictly oriented:
mul0#(C(x,y),y') = [9] x + [9] y + [22]
> [9] y + [21]
= c_6(add0#(mul0(y,y'),y')
,mul0#(y,y'))
Following rules are (at-least) weakly oriented:
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
-->_2 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: mul0#(C(x,y),y') ->
c_6(add0#(mul0(y,y'),y')
,mul0#(y,y'))
*** 1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
mul0#(C(x,y),y') -> mul0#(y,y')
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: add0#(C(x,y),y') -> c_1(add0#(y
,C(S(),y')))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
mul0#(C(x,y),y') -> mul0#(y,y')
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_1) = {1}
Following symbols are considered usable:
{add0,mul0,add0#,goal#,isZero#,mul0#,second#}
TcT has computed the following interpretation:
p(C) = 1 + x2
p(False) = 1
p(S) = 0
p(True) = 1
p(Z) = 0
p(add0) = x1 + x2
p(goal) = 1 + x1
p(isZero) = 2
p(mul0) = 2 + x1*x2
p(second) = 2*x1 + x1^2
p(add0#) = 2 + x1
p(goal#) = 0
p(isZero#) = 2
p(mul0#) = 5*x1 + 5*x1*x2 + 5*x1^2 + 2*x2 + 2*x2^2
p(second#) = 0
p(c_1) = x1
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 1
p(c_6) = x1
p(c_7) = 1
p(c_8) = 0
Following rules are strictly oriented:
add0#(C(x,y),y') = 3 + y
> 2 + y
= c_1(add0#(y,C(S(),y')))
Following rules are (at-least) weakly oriented:
mul0#(C(x,y),y') = 10 + 15*y + 5*y*y' + 5*y^2 + 7*y' + 2*y'^2
>= 4 + y*y'
= add0#(mul0(y,y'),y')
mul0#(C(x,y),y') = 10 + 15*y + 5*y*y' + 5*y^2 + 7*y' + 2*y'^2
>= 5*y + 5*y*y' + 5*y^2 + 2*y' + 2*y'^2
= mul0#(y,y')
add0(C(x,y),y') = 1 + y + y'
>= 1 + y + y'
= add0(y,C(S(),y'))
add0(Z(),y) = y
>= y
= y
mul0(C(x,y),y') = 2 + y*y' + y'
>= 2 + y*y' + y'
= add0(mul0(y,y'),y')
mul0(Z(),y) = 2
>= 0
= Z()
*** 1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
mul0#(C(x,y),y') -> mul0#(y,y')
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
mul0#(C(x,y),y') -> mul0#(y,y')
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):1
2:W:mul0#(C(x,y),y') -> add0#(mul0(y,y'),y')
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):1
3:W:mul0#(C(x,y),y') -> mul0#(y,y')
-->_1 mul0#(C(x,y),y') -> mul0#(y,y'):3
-->_1 mul0#(C(x,y),y') -> add0#(mul0(y,y'),y'):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: mul0#(C(x,y),y') -> mul0#(y,y')
2: mul0#(C(x,y),y') -> add0#(mul0(y
,y')
,y')
1: add0#(C(x,y),y') -> c_1(add0#(y
,C(S(),y')))
*** 1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):2
-->_2 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):1
2:W:add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y')))
-->_1 add0#(C(x,y),y') -> c_1(add0#(y,C(S(),y'))):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: add0#(C(x,y),y') -> c_1(add0#(y
,C(S(),y')))
*** 1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/2,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y'))
-->_2 mul0#(C(x,y),y') -> c_6(add0#(mul0(y,y'),y'),mul0#(y,y')):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
*** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
add0(C(x,y),y') -> add0(y,C(S(),y'))
add0(Z(),y) -> y
mul0(C(x,y),y') -> add0(mul0(y,y'),y')
mul0(Z(),y) -> Z()
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
*** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: mul0#(C(x,y),y') -> c_6(mul0#(y
,y'))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_6) = {1}
Following symbols are considered usable:
{add0#,goal#,isZero#,mul0#,second#}
TcT has computed the following interpretation:
p(C) = [1] x1 + [1] x2 + [2]
p(False) = [0]
p(S) = [0]
p(True) = [0]
p(Z) = [0]
p(add0) = [0]
p(goal) = [0]
p(isZero) = [0]
p(mul0) = [0]
p(second) = [0]
p(add0#) = [0]
p(goal#) = [0]
p(isZero#) = [0]
p(mul0#) = [3] x1 + [1]
p(second#) = [0]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [0]
Following rules are strictly oriented:
mul0#(C(x,y),y') = [3] x + [3] y + [7]
> [3] y + [1]
= c_6(mul0#(y,y'))
Following rules are (at-least) weakly oriented:
*** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:mul0#(C(x,y),y') -> c_6(mul0#(y,y'))
-->_1 mul0#(C(x,y),y') -> c_6(mul0#(y,y')):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: mul0#(C(x,y),y') -> c_6(mul0#(y
,y'))
*** 1.1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
Signature:
{add0/2,goal/2,isZero/1,mul0/2,second/1,add0#/2,goal#/2,isZero#/1,mul0#/2,second#/1} / {C/2,False/0,S/0,True/0,Z/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0}
Obligation:
Innermost
basic terms: {add0#,goal#,isZero#,mul0#,second#}/{C,False,S,True,Z}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).