*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Weak DP Rules:
Weak TRS Rules:
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3} / {der/1,dout/1,plus/2,times/2}
Obligation:
Innermost
basic terms: {din,u21,u22,u31,u32,u41,u42}/{der,dout,plus,times}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
u22#(dout(DY),X,Y,DX) -> c_5()
u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
u32#(dout(DY),X,Y,DX) -> c_7()
u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
u42#(dout(DDX),X,DX) -> c_9()
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
u22#(dout(DY),X,Y,DX) -> c_5()
u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
u32#(dout(DY),X,Y,DX) -> c_7()
u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
u42#(dout(DDX),X,DX) -> c_9()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{5,7,9}
by application of
Pre({5,7,9}) = {4,6,8}.
Here rules are labelled as follows:
1: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
4: u21#(dout(DX),X,Y) ->
c_4(u22#(din(der(Y)),X,Y,DX)
,din#(der(Y)))
5: u22#(dout(DY),X,Y,DX) -> c_5()
6: u31#(dout(DX),X,Y) ->
c_6(u32#(din(der(Y)),X,Y,DX)
,din#(der(Y)))
7: u32#(dout(DY),X,Y,DX) -> c_7()
8: u41#(dout(DX),X) ->
c_8(u42#(din(der(DX)),X,DX)
,din#(der(DX)))
9: u42#(dout(DDX),X,DX) -> c_9()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
Strict TRS Rules:
Weak DP Rules:
u22#(dout(DY),X,Y,DX) -> c_5()
u32#(dout(DY),X,Y,DX) -> c_7()
u42#(dout(DDX),X,DX) -> c_9()
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
-->_1 u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))):6
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
2:S:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
-->_1 u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))):4
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
3:S:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
-->_1 u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))):5
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
4:S:u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
-->_1 u22#(dout(DY),X,Y,DX) -> c_5():7
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
5:S:u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
-->_1 u32#(dout(DY),X,Y,DX) -> c_7():8
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
6:S:u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
-->_1 u42#(dout(DDX),X,DX) -> c_9():9
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
7:W:u22#(dout(DY),X,Y,DX) -> c_5()
8:W:u32#(dout(DY),X,Y,DX) -> c_7()
9:W:u42#(dout(DDX),X,DX) -> c_9()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: u22#(dout(DY),X,Y,DX) -> c_5()
8: u32#(dout(DY),X,Y,DX) -> c_7()
9: u42#(dout(DDX),X,DX) -> c_9()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/2,c_5/0,c_6/2,c_7/0,c_8/2,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
-->_1 u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX))):6
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
2:S:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
-->_1 u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y))):4
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
3:S:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
-->_1 u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y))):5
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
4:S:u21#(dout(DX),X,Y) -> c_4(u22#(din(der(Y)),X,Y,DX),din#(der(Y)))
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
5:S:u31#(dout(DX),X,Y) -> c_6(u32#(din(der(Y)),X,Y,DX),din#(der(Y)))
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
6:S:u41#(dout(DX),X) -> c_8(u42#(din(der(DX)),X,DX),din#(der(DX)))
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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:
6: u41#(dout(DX),X) ->
c_8(din#(der(DX)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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_1) = {1,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = [0]
p(din) = [0]
p(dout) = [1] x1 + [1]
p(plus) = [1] x2 + [3]
p(times) = [1] x2 + [0]
p(u21) = [0]
p(u22) = [6] x1 + [0]
p(u31) = [1] x1 + [0]
p(u32) = [4] x1 + [1] x4 + [1]
p(u41) = [4] x1 + [0]
p(u42) = [6] x1 + [3] x3 + [4]
p(din#) = [0]
p(u21#) = [4] x1 + [0]
p(u22#) = [2] x1 + [1] x4 + [4]
p(u31#) = [1] x1 + [0]
p(u32#) = [1] x2 + [1] x3 + [1] x4 + [0]
p(u41#) = [4] x1 + [0]
p(u42#) = [1] x2 + [2]
p(c_1) = [2] x1 + [4] x2 + [0]
p(c_2) = [4] x1 + [2] x2 + [0]
p(c_3) = [2] x1 + [2] x2 + [0]
p(c_4) = [4] x1 + [4]
p(c_5) = [2]
p(c_6) = [4] x1 + [1]
p(c_7) = [0]
p(c_8) = [1] x1 + [0]
p(c_9) = [1]
Following rules are strictly oriented:
u41#(dout(DX),X) = [4] DX + [4]
> [0]
= c_8(din#(der(DX)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = [0]
>= [0]
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
din#(der(plus(X,Y))) = [0]
>= [0]
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
din#(der(times(X,Y))) = [0]
>= [0]
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
u21#(dout(DX),X,Y) = [4] DX + [4]
>= [4]
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = [1] DX + [1]
>= [1]
= c_6(din#(der(Y)))
din(der(der(X))) = [0]
>= [0]
= u41(din(der(X)),X)
din(der(plus(X,Y))) = [0]
>= [0]
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = [0]
>= [0]
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = [0]
>= [0]
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = [6] DY + [6]
>= [1] DY + [4]
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = [1] DX + [1]
>= [1] DX + [1]
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = [1] DX + [4] DY + [5]
>= [1] DX + [4]
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = [4] DX + [4]
>= [3] DX + [4]
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = [6] DDX + [3] DX + [10]
>= [1] DDX + [1]
= dout(DDX)
*** 1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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:
4: u21#(dout(DX),X,Y) ->
c_4(din#(der(Y)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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_1) = {1,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = [0]
p(din) = [1] x1 + [0]
p(dout) = [1] x1 + [1]
p(plus) = [1] x1 + [0]
p(times) = [3]
p(u21) = [2] x1 + [0]
p(u22) = [1] x1 + [2] x4 + [0]
p(u31) = [1] x1 + [0]
p(u32) = [4] x1 + [1] x4 + [0]
p(u41) = [0]
p(u42) = [7] x1 + [0]
p(din#) = [0]
p(u21#) = [4] x1 + [0]
p(u22#) = [1] x2 + [1]
p(u31#) = [0]
p(u32#) = [1] x2 + [4] x3 + [4]
p(u41#) = [0]
p(u42#) = [1] x1 + [0]
p(c_1) = [4] x1 + [1] x2 + [0]
p(c_2) = [4] x1 + [1] x2 + [0]
p(c_3) = [4] x1 + [2] x2 + [0]
p(c_4) = [1] x1 + [2]
p(c_5) = [4]
p(c_6) = [2] x1 + [0]
p(c_7) = [2]
p(c_8) = [1] x1 + [0]
p(c_9) = [1]
Following rules are strictly oriented:
u21#(dout(DX),X,Y) = [4] DX + [4]
> [2]
= c_4(din#(der(Y)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = [0]
>= [0]
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
din#(der(plus(X,Y))) = [0]
>= [0]
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
din#(der(times(X,Y))) = [0]
>= [0]
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
u31#(dout(DX),X,Y) = [0]
>= [0]
= c_6(din#(der(Y)))
u41#(dout(DX),X) = [0]
>= [0]
= c_8(din#(der(DX)))
din(der(der(X))) = [0]
>= [0]
= u41(din(der(X)),X)
din(der(plus(X,Y))) = [0]
>= [0]
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = [0]
>= [0]
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = [2] DX + [2]
>= [2] DX + [0]
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = [2] DX + [1] DY + [1]
>= [1] DX + [1]
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = [1] DX + [1]
>= [1] DX + [0]
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = [1] DX + [4] DY + [4]
>= [4]
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = [0]
>= [0]
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = [7] DDX + [7]
>= [1] DDX + [1]
= dout(DDX)
*** 1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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:
4: u31#(dout(DX),X,Y) ->
c_6(din#(der(Y)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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_1) = {1,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = [0]
p(din) = [1] x1 + [0]
p(dout) = [2]
p(plus) = [1] x1 + [6]
p(times) = [1] x2 + [0]
p(u21) = [2] x1 + [0]
p(u22) = [1] x1 + [0]
p(u31) = [4] x1 + [0]
p(u32) = [2] x1 + [3]
p(u41) = [2] x1 + [0]
p(u42) = [4] x1 + [1]
p(din#) = [0]
p(u21#) = [6] x1 + [0]
p(u22#) = [1] x1 + [1] x2 + [1] x4 + [0]
p(u31#) = [2] x1 + [0]
p(u32#) = [1]
p(u41#) = [1] x1 + [0]
p(u42#) = [2] x2 + [0]
p(c_1) = [4] x1 + [4] x2 + [0]
p(c_2) = [2] x1 + [1] x2 + [0]
p(c_3) = [1] x1 + [1] x2 + [0]
p(c_4) = [1] x1 + [7]
p(c_5) = [4]
p(c_6) = [1] x1 + [2]
p(c_7) = [0]
p(c_8) = [2] x1 + [2]
p(c_9) = [1]
Following rules are strictly oriented:
u31#(dout(DX),X,Y) = [4]
> [2]
= c_6(din#(der(Y)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = [0]
>= [0]
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
din#(der(plus(X,Y))) = [0]
>= [0]
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
din#(der(times(X,Y))) = [0]
>= [0]
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
u21#(dout(DX),X,Y) = [12]
>= [7]
= c_4(din#(der(Y)))
u41#(dout(DX),X) = [2]
>= [2]
= c_8(din#(der(DX)))
din(der(der(X))) = [0]
>= [0]
= u41(din(der(X)),X)
din(der(plus(X,Y))) = [0]
>= [0]
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = [0]
>= [0]
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = [4]
>= [0]
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = [2]
>= [2]
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = [8]
>= [3]
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = [7]
>= [2]
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = [4]
>= [1]
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = [9]
>= [2]
= dout(DDX)
*** 1.1.1.1.1.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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:
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
Consider the set of all dependency pairs
1: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
4: u21#(dout(DX),X,Y) ->
c_4(din#(der(Y)))
5: u31#(dout(DX),X,Y) ->
c_6(din#(der(Y)))
6: u41#(dout(DX),X) ->
c_8(din#(der(DX)))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{3}
These cover all (indirect) predecessors of dependency pairs
{3,5}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = 1 + x1
p(din) = 0
p(dout) = 1 + x1
p(plus) = x1
p(times) = 1 + x1
p(u21) = 3*x1 + 3*x1*x3 + x1^2
p(u22) = 3*x1 + 2*x1*x4 + x1^2 + 2*x4
p(u31) = 3*x1 + x1^2
p(u32) = 2 + x1 + 2*x1*x2 + 2*x1*x4 + x1^2
p(u41) = x1 + 2*x1*x2
p(u42) = 2*x1^2 + 2*x2*x3 + x3
p(din#) = 2*x1
p(u21#) = 2*x1 + 2*x1*x2 + 2*x1*x3 + 2*x1^2
p(u22#) = 0
p(u31#) = x1 + 3*x1*x2 + 2*x1*x3 + x1^2
p(u32#) = 2 + 2*x3 + x3*x4 + 2*x3^2 + x4^2
p(u41#) = 2 + 2*x1
p(u42#) = 2*x2
p(c_1) = x1 + x2
p(c_2) = x1 + x2
p(c_3) = x1 + x2
p(c_4) = 1 + x1
p(c_5) = 0
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1
p(c_9) = 0
Following rules are strictly oriented:
din#(der(times(X,Y))) = 4 + 2*X
> 2 + 2*X
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = 4 + 2*X
>= 4 + 2*X
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
din#(der(plus(X,Y))) = 2 + 2*X
>= 2 + 2*X
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
u21#(dout(DX),X,Y) = 4 + 6*DX + 2*DX*X + 2*DX*Y + 2*DX^2 + 2*X + 2*Y
>= 3 + 2*Y
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 2 + 3*DX + 3*DX*X + 2*DX*Y + DX^2 + 3*X + 2*Y
>= 2 + 2*Y
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 4 + 2*DX
>= 2 + 2*DX
= c_8(din#(der(DX)))
din(der(der(X))) = 0
>= 0
= u41(din(der(X)),X)
din(der(plus(X,Y))) = 0
>= 0
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = 0
>= 0
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = 4 + 5*DX + 3*DX*Y + DX^2 + 3*Y
>= 2*DX
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 4 + 4*DX + 2*DX*DY + 5*DY + DY^2
>= 1 + DX
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = 4 + 5*DX + DX^2
>= 2
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 4 + 2*DX + 2*DX*DY + 3*DY + 2*DY*X + DY^2 + 2*X
>= 2 + X
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = 1 + DX + 2*DX*X + 2*X
>= DX + 2*DX*X
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 2 + 4*DDX + 2*DDX^2 + DX + 2*DX*X
>= 1 + DDX
= dout(DDX)
*** 1.1.1.1.1.2.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.2.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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:
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
Consider the set of all dependency pairs
1: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
4: u21#(dout(DX),X,Y) ->
c_4(din#(der(Y)))
5: u31#(dout(DX),X,Y) ->
c_6(din#(der(Y)))
6: u41#(dout(DX),X) ->
c_8(din#(der(DX)))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{2}
These cover all (indirect) predecessors of dependency pairs
{2,4}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.2.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = x1
p(din) = 0
p(dout) = 1 + x1
p(plus) = 1 + x1 + x2
p(times) = x1 + x2
p(u21) = 2*x1 + 2*x1*x2 + 2*x1^2
p(u22) = 2 + x1*x2 + 2*x1*x4 + 2*x1^2 + x2 + x2*x4 + 2*x4
p(u31) = x1*x3
p(u32) = 2*x1 + 2*x1*x2 + 2*x1*x3 + 2*x1*x4 + x3*x4
p(u41) = x1*x2 + 2*x1^2
p(u42) = 3*x1 + x2*x3 + x3 + x3^2
p(din#) = x1^2
p(u21#) = x1 + 2*x2 + x2*x3 + x3^2
p(u22#) = 2*x1*x4 + x2 + x2*x3 + x3 + x3^2 + 2*x4^2
p(u31#) = 2*x1 + 2*x1*x3 + x2*x3 + x3^2
p(u32#) = 2*x1 + 2*x1*x2 + x1*x3 + x1*x4 + x2 + 2*x2*x4 + 2*x4
p(u41#) = 2*x1^2
p(u42#) = x1 + 2*x1*x2 + x1*x3 + 2*x2 + 2*x2*x3 + 2*x3^2
p(c_1) = x1 + x2
p(c_2) = x1 + x2
p(c_3) = x1 + x2
p(c_4) = x1
p(c_5) = 0
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1
p(c_9) = 1
Following rules are strictly oriented:
din#(der(plus(X,Y))) = 1 + 2*X + 2*X*Y + X^2 + 2*Y + Y^2
> 2*X + X*Y + X^2 + Y^2
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = X^2
>= X^2
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
din#(der(times(X,Y))) = 2*X*Y + X^2 + Y^2
>= X*Y + X^2 + Y^2
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
u21#(dout(DX),X,Y) = 1 + DX + 2*X + X*Y + Y^2
>= Y^2
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 2 + 2*DX + 2*DX*Y + X*Y + 2*Y + Y^2
>= Y^2
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2
>= DX^2
= c_8(din#(der(DX)))
din(der(der(X))) = 0
>= 0
= u41(din(der(X)),X)
din(der(plus(X,Y))) = 0
>= 0
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = 0
>= 0
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = 4 + 6*DX + 2*DX*X + 2*DX^2 + 2*X
>= 2 + 2*DX + DX*X + X
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 4 + 4*DX + 2*DX*DY + DX*X + 4*DY + DY*X + 2*DY^2 + 2*X
>= 2 + DX + DY
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = DX*Y + Y
>= DX*Y
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 2 + 2*DX + 2*DX*DY + DX*Y + 2*DY + 2*DY*X + 2*DY*Y + 2*X + 2*Y
>= 2 + DX + DY + X + Y
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = 2 + 4*DX + DX*X + 2*DX^2 + X
>= DX + DX*X + DX^2
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 3 + 3*DDX + DX + DX*X + DX^2
>= 1 + DDX
= dout(DDX)
*** 1.1.1.1.1.2.2.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.2.2.2.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
Consider the set of all dependency pairs
1: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
4: u21#(dout(DX),X,Y) ->
c_4(din#(der(Y)))
5: u31#(dout(DX),X,Y) ->
c_6(din#(der(Y)))
6: u41#(dout(DX),X) ->
c_8(din#(der(DX)))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,6}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.2.2.2.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
Strict TRS Rules:
Weak DP Rules:
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
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,2},
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1},
uargs(c_6) = {1},
uargs(c_8) = {1}
Following symbols are considered usable:
{din,u21,u22,u31,u32,u41,u42,din#,u21#,u22#,u31#,u32#,u41#,u42#}
TcT has computed the following interpretation:
p(der) = 1 + x1
p(din) = 0
p(dout) = 1 + x1
p(plus) = 1 + x1 + x2
p(times) = 1 + x1
p(u21) = x1 + x1^2
p(u22) = 3*x1^2 + 3*x4
p(u31) = x1 + 2*x1*x3 + 2*x1^2
p(u32) = 3 + x1 + 2*x1*x2 + x3 + x3*x4 + x4
p(u41) = 0
p(u42) = 3*x1*x2 + 2*x1^2
p(din#) = x1
p(u21#) = 1 + 3*x1*x2 + 3*x1*x3 + x3
p(u22#) = 1 + 2*x1^2 + x2*x3 + 2*x2*x4 + x4 + 2*x4^2
p(u31#) = 3*x1 + 2*x1*x2 + 2*x1*x3
p(u32#) = 2 + 2*x1^2 + x2 + x2*x4 + x4 + x4^2
p(u41#) = x1 + 3*x1^2
p(u42#) = x2*x3 + x3 + x3^2
p(c_1) = x1 + x2
p(c_2) = x1 + x2
p(c_3) = x1 + x2
p(c_4) = x1
p(c_5) = 0
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1
p(c_9) = 0
Following rules are strictly oriented:
din#(der(der(X))) = 2 + X
> 1 + X
= c_1(u41#(din(der(X)),X)
,din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(plus(X,Y))) = 2 + X + Y
>= 2 + X + Y
= c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
din#(der(times(X,Y))) = 2 + X
>= 1 + X
= c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
u21#(dout(DX),X,Y) = 1 + 3*DX*X + 3*DX*Y + 3*X + 4*Y
>= 1 + Y
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 3 + 3*DX + 2*DX*X + 2*DX*Y + 2*X + 2*Y
>= 1 + Y
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 4 + 7*DX + 3*DX^2
>= 1 + DX
= c_8(din#(der(DX)))
din(der(der(X))) = 0
>= 0
= u41(din(der(X)),X)
din(der(plus(X,Y))) = 0
>= 0
= u21(din(der(X)),X,Y)
din(der(times(X,Y))) = 0
>= 0
= u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) = 2 + 3*DX + DX^2
>= 3*DX
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 3 + 3*DX + 6*DY + 3*DY^2
>= 2 + DX + DY
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = 3 + 5*DX + 2*DX*Y + 2*DX^2 + 2*Y
>= 3 + DX + DX*Y + Y
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 4 + DX + DX*Y + DY + 2*DY*X + 2*X + Y
>= 4 + X + Y
= dout(plus(times(X,DY)
,times(Y,DX)))
u41(dout(DX),X) = 0
>= 0
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 2 + 4*DDX + 3*DDX*X + 2*DDX^2 + 3*X
>= 1 + DDX
= dout(DDX)
*** 1.1.1.1.1.2.2.2.2.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.2.2.2.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
-->_1 u41#(dout(DX),X) -> c_8(din#(der(DX))):6
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
2:W:din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X)))
-->_1 u21#(dout(DX),X,Y) -> c_4(din#(der(Y))):4
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
3:W:din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X)))
-->_1 u31#(dout(DX),X,Y) -> c_6(din#(der(Y))):5
-->_2 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_2 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_2 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
4:W:u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
-->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
5:W:u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
-->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
6:W:u41#(dout(DX),X) -> c_8(din#(der(DX)))
-->_1 din#(der(times(X,Y))) -> c_3(u31#(din(der(X)),X,Y),din#(der(X))):3
-->_1 din#(der(plus(X,Y))) -> c_2(u21#(din(der(X)),X,Y),din#(der(X))):2
-->_1 din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: din#(der(der(X))) ->
c_1(u41#(din(der(X)),X)
,din#(der(X)))
6: u41#(dout(DX),X) ->
c_8(din#(der(DX)))
5: u31#(dout(DX),X,Y) ->
c_6(din#(der(Y)))
3: din#(der(times(X,Y))) ->
c_3(u31#(din(der(X)),X,Y)
,din#(der(X)))
4: u21#(dout(DX),X,Y) ->
c_4(din#(der(Y)))
2: din#(der(plus(X,Y))) ->
c_2(u21#(din(der(X)),X,Y)
,din#(der(X)))
*** 1.1.1.1.1.2.2.2.2.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
din(der(der(X))) -> u41(din(der(X)),X)
din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) -> dout(DDX)
Signature:
{din/1,u21/3,u22/4,u31/3,u32/4,u41/2,u42/3,din#/1,u21#/3,u22#/4,u31#/3,u32#/4,u41#/2,u42#/3} / {der/1,dout/1,plus/2,times/2,c_1/2,c_2/2,c_3/2,c_4/1,c_5/0,c_6/1,c_7/0,c_8/1,c_9/0}
Obligation:
Innermost
basic terms: {din#,u21#,u22#,u31#,u32#,u41#,u42#}/{der,dout,plus,times}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).