WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
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} / {der/1,dout/1,plus/2,times/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {din,u21,u22,u31,u32,u41,u42} and constructors {der,dout
,plus,times}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
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.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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 TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
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()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
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()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
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)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
SimplifyRHS
+ Details:
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)))
* Step 5: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {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}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} 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.
** Step 5.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- 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(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
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]
p(plus) = [1] x2 + [0]
p(times) = [1] x2 + [1]
p(u21) = [0]
p(u22) = [1] x1 + [0]
p(u31) = [1] x1 + [0]
p(u32) = [1]
p(u41) = [1] x1 + [0]
p(u42) = [7] x1 + [0]
p(din#) = [0]
p(u21#) = [2] x1 + [0]
p(u22#) = [4] x4 + [1]
p(u31#) = [6] x1 + [0]
p(u32#) = [1] x1 + [2] x3 + [2] x4 + [1]
p(u41#) = [0]
p(u42#) = [0]
p(c_1) = [4] x1 + [2] x2 + [0]
p(c_2) = [1] x1 + [1] x2 + [0]
p(c_3) = [1] x1 + [2] x2 + [0]
p(c_4) = [1] x1 + [0]
p(c_5) = [1]
p(c_6) = [2] x1 + [6]
p(c_7) = [1]
p(c_8) = [4] x1 + [0]
p(c_9) = [1]
Following rules are strictly oriented:
u21#(dout(DX),X,Y) = [2]
> [0]
= 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) = [6]
>= [6]
= 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) = [0]
>= [0]
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = [1]
>= [1]
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = [1]
>= [1]
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = [1]
>= [1]
= dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) = [1]
>= [0]
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = [7]
>= [1]
= dout(DDX)
** Step 5.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- 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)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak DPs:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
** Step 5.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak DPs:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {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}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
4: u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
5: u41#(dout(DX),X) -> c_8(din#(der(DX)))
The strictly oriented rules are moved into the weak component.
*** Step 5.b:1.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- 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)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak DPs:
u21#(dout(DX),X,Y) -> c_4(din#(der(Y)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
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) = [2]
p(plus) = [1] x2 + [1]
p(times) = [6]
p(u21) = [3] x1 + [0]
p(u22) = [4] x1 + [5]
p(u31) = [4] x1 + [0]
p(u32) = [1] x1 + [3]
p(u41) = [1] x1 + [0]
p(u42) = [1] x1 + [0]
p(din#) = [0]
p(u21#) = [3] x1 + [0]
p(u22#) = [1] x1 + [1] x2 + [1]
p(u31#) = [4] x1 + [0]
p(u32#) = [2] x3 + [2]
p(u41#) = [4] x1 + [0]
p(u42#) = [4] x2 + [1] x3 + [0]
p(c_1) = [1] x1 + [1] x2 + [0]
p(c_2) = [4] x1 + [4] x2 + [0]
p(c_3) = [4] x1 + [2] x2 + [0]
p(c_4) = [1] x1 + [6]
p(c_5) = [2]
p(c_6) = [4] x1 + [0]
p(c_7) = [1]
p(c_8) = [4] x1 + [6]
p(c_9) = [1]
Following rules are strictly oriented:
u31#(dout(DX),X,Y) = [8]
> [0]
= c_6(din#(der(Y)))
u41#(dout(DX),X) = [8]
> [6]
= 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) = [6]
>= [6]
= c_4(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) = [6]
>= [5]
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = [13]
>= [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) = [5]
>= [2]
= dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) = [2]
>= [0]
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = [2]
>= [2]
= dout(DDX)
*** Step 5.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 5.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {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}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} 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}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.
**** Step 5.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
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) = x1
p(times) = 2 + x1
p(u21) = 2*x1 + 2*x1*x2 + 3*x1*x3 + 2*x1^2
p(u22) = 2*x1 + 3*x1*x2 + 2*x1^2 + 2*x2*x4 + 3*x3 + x4 + x4^2
p(u31) = 3*x1*x3 + 2*x1^2
p(u32) = x1 + x1*x2 + 2*x1*x3 + 2*x1^2 + 3*x3 + x3*x4
p(u41) = 2*x1*x2 + x1^2
p(u42) = 1 + 2*x1 + 2*x1*x2 + 2*x1^2 + 2*x2 + x2*x3 + x3
p(din#) = 1 + 2*x1
p(u21#) = 2*x1 + 2*x1*x2 + 2*x1*x3
p(u22#) = x3^2
p(u31#) = 3 + x1 + 2*x1*x2 + 2*x1*x3 + x1^2
p(u32#) = x1 + 2*x1*x2 + x1*x3 + 2*x2*x3 + 2*x3
p(u41#) = 2*x1
p(u42#) = 2 + x1 + 2*x2 + 2*x2^2
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) = 1
Following rules are strictly oriented:
din#(der(times(X,Y))) = 5 + 2*X
> 4 + 2*X
= c_3(u31#(din(der(X)),X,Y),din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = 1 + 2*X
>= 1 + 2*X
= c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(plus(X,Y))) = 1 + 2*X
>= 1 + 2*X
= c_2(u21#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) = 2 + 2*DX + 2*DX*X + 2*DX*Y + 2*X + 2*Y
>= 2 + 2*Y
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 5 + 3*DX + 2*DX*X + 2*DX*Y + DX^2 + 2*X + 2*Y
>= 1 + 2*Y
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 2 + 2*DX
>= 1 + 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 + 6*DX + 2*DX*X + 3*DX*Y + 2*DX^2 + 2*X + 3*Y
>= DX + 2*DX*X + DX^2 + 3*Y
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 4 + DX + 2*DX*X + DX^2 + 6*DY + 3*DY*X + 2*DY^2 + 3*X + 3*Y
>= 1 + DX
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = 2 + 4*DX + 3*DX*Y + 2*DX^2 + 3*Y
>= DX*Y + 3*Y
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 3 + DX*Y + 5*DY + DY*X + 2*DY*Y + 2*DY^2 + X + 5*Y
>= 3 + X
= dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) = 1 + 2*DX + 2*DX*X + DX^2 + 2*X
>= 1 + DX + DX*X + 2*X
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 5 + 6*DDX + 2*DDX*X + 2*DDX^2 + DX + DX*X + 4*X
>= 1 + DDX
= dout(DDX)
**** Step 5.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 5.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {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}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} 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}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.
***** Step 5.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- 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)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
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) = 2 + x1
p(times) = 2 + x1
p(u21) = x1 + 3*x1*x2 + 2*x1*x3 + 3*x1^2
p(u22) = 3 + x1*x2 + 3*x1*x3 + 3*x1*x4 + 3*x2 + 3*x2*x4 + x3 + x3*x4 + 3*x4
p(u31) = 2*x1*x2 + x1^2
p(u32) = 1 + 3*x1 + x1^2 + 2*x2 + 2*x4
p(u41) = 3*x1*x2
p(u42) = x1 + x1*x2 + 3*x1^2 + 3*x2
p(din#) = 3*x1
p(u21#) = 2*x1 + 3*x1*x3 + x1^2
p(u22#) = 2*x4 + x4^2
p(u31#) = 3 + 3*x1*x3
p(u32#) = x2^2
p(u41#) = 2*x1^2
p(u42#) = 1 + x1^2 + x2^2 + 2*x3^2
p(c_1) = x1 + x2
p(c_2) = x1 + x2
p(c_3) = 3 + x1 + x2
p(c_4) = 3 + x1
p(c_5) = 1
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1
p(c_9) = 0
Following rules are strictly oriented:
din#(der(plus(X,Y))) = 6 + 3*X
> 3*X
= c_2(u21#(din(der(X)),X,Y),din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(der(X))) = 3*X
>= 3*X
= c_1(u41#(din(der(X)),X),din#(der(X)))
din#(der(times(X,Y))) = 6 + 3*X
>= 6 + 3*X
= c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) = 3 + 4*DX + 3*DX*Y + DX^2 + 3*Y
>= 3 + 3*Y
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 3 + 3*DX*Y + 3*Y
>= 3*Y
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 2 + 4*DX + 2*DX^2
>= 3*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 + 7*DX + 3*DX*X + 2*DX*Y + 3*DX^2 + 3*X + 2*Y
>= 3 + 3*DX + 3*DX*X + DX*Y + 3*X + Y
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 3 + 6*DX + 3*DX*DY + 3*DX*X + DX*Y + DY*X + 3*DY*Y + 4*X + 4*Y
>= 3 + DX
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = 1 + 2*DX + 2*DX*X + DX^2 + 2*X
>= 1 + 2*DX + 2*X
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 5 + 2*DX + 5*DY + DY^2 + 2*X
>= 5 + X
= dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) = 3*DX*X + 3*X
>= 3*X
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 4 + 7*DDX + DDX*X + 3*DDX^2 + 4*X
>= 1 + DDX
= dout(DDX)
***** Step 5.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 5.b:1.b:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {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}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} 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}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.
****** Step 5.b:1.b:1.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
din#(der(der(X))) -> c_1(u41#(din(der(X)),X),din#(der(X)))
- Weak DPs:
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:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
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) = 2 + x1
p(plus) = 1 + x1
p(times) = x1 + x2
p(u21) = 3*x1
p(u22) = 3 + 3*x4
p(u31) = x1^2
p(u32) = 3*x1 + x1*x2 + x4
p(u41) = 2*x1 + x1*x2
p(u42) = x1 + x2*x3 + 2*x3
p(din#) = 3*x1
p(u21#) = 2 + 2*x1 + 2*x1*x3
p(u22#) = 2*x1 + x1*x3 + 2*x1^2 + 2*x2^2
p(u31#) = 2*x1 + 2*x1*x3
p(u32#) = 1 + 2*x1 + 2*x1*x2 + x2 + x4
p(u41#) = x1^2
p(u42#) = 2 + x1*x2 + 2*x1*x3 + 2*x1^2 + x2 + x3
p(c_1) = 1 + x1 + x2
p(c_2) = 1 + x1 + x2
p(c_3) = x1 + x2
p(c_4) = x1
p(c_5) = 0
p(c_6) = 1 + x1
p(c_7) = 0
p(c_8) = 1 + x1
p(c_9) = 1
Following rules are strictly oriented:
din#(der(der(X))) = 6 + 3*X
> 4 + 3*X
= c_1(u41#(din(der(X)),X),din#(der(X)))
Following rules are (at-least) weakly oriented:
din#(der(plus(X,Y))) = 6 + 3*X
>= 6 + 3*X
= c_2(u21#(din(der(X)),X,Y),din#(der(X)))
din#(der(times(X,Y))) = 3 + 3*X + 3*Y
>= 3 + 3*X
= c_3(u31#(din(der(X)),X,Y),din#(der(X)))
u21#(dout(DX),X,Y) = 6 + 2*DX + 2*DX*Y + 4*Y
>= 3 + 3*Y
= c_4(din#(der(Y)))
u31#(dout(DX),X,Y) = 4 + 2*DX + 2*DX*Y + 4*Y
>= 4 + 3*Y
= c_6(din#(der(Y)))
u41#(dout(DX),X) = 4 + 4*DX + DX^2
>= 4 + 3*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) = 6 + 3*DX
>= 3 + 3*DX
= u22(din(der(Y)),X,Y,DX)
u22(dout(DY),X,Y,DX) = 3 + 3*DX
>= 3 + DX
= dout(plus(DX,DY))
u31(dout(DX),X,Y) = 4 + 4*DX + DX^2
>= DX
= u32(din(der(Y)),X,Y,DX)
u32(dout(DY),X,Y,DX) = 6 + DX + 3*DY + DY*X + 2*X
>= 3 + DY + X
= dout(plus(times(X,DY),times(Y,DX)))
u41(dout(DX),X) = 4 + 2*DX + DX*X + 2*X
>= 2*DX + DX*X
= u42(din(der(DX)),X,DX)
u42(dout(DDX),X,DX) = 2 + DDX + 2*DX + DX*X
>= 2 + DDX
= dout(DDX)
****** Step 5.b:1.b:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak 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(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
****** Step 5.b:1.b:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak 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(din#(der(Y)))
u31#(dout(DX),X,Y) -> c_6(din#(der(Y)))
u41#(dout(DX),X) -> c_8(din#(der(DX)))
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
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)))
****** Step 5.b:1.b:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
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 runtime complexity wrt. defined symbols {din#,u21#,u22#,u31#,u32#,u41#,u42#} and constructors {der
,dout,plus,times}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))