MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
2ndsneg(0(),Z) -> rnil()
2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
2ndspos(0(),Z) -> rnil()
2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
from(X) -> cons(X,from(s(X)))
pi(X) -> 2ndspos(X,from(0()))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
square(X) -> times(X,X)
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1
,rcons/2,rnil/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg,2ndspos,from,pi,plus,square
,times} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
2ndsneg#(0(),Z) -> c_1()
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(0(),Z) -> c_4()
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(0(),Y) -> c_9()
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(0(),Y) -> c_12()
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(0(),Z) -> c_1()
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(0(),Z) -> c_4()
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(0(),Y) -> c_9()
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(0(),Y) -> c_12()
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak TRS:
2ndsneg(0(),Z) -> rnil()
2ndsneg(s(N),cons(X,Z)) -> 2ndsneg(s(N),cons2(X,Z))
2ndsneg(s(N),cons2(X,cons(Y,Z))) -> rcons(negrecip(Y),2ndspos(N,Z))
2ndspos(0(),Z) -> rnil()
2ndspos(s(N),cons(X,Z)) -> 2ndspos(s(N),cons2(X,Z))
2ndspos(s(N),cons2(X,cons(Y,Z))) -> rcons(posrecip(Y),2ndsneg(N,Z))
from(X) -> cons(X,from(s(X)))
pi(X) -> 2ndspos(X,from(0()))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
square(X) -> times(X,X)
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
2ndsneg#(0(),Z) -> c_1()
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(0(),Z) -> c_4()
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(0(),Y) -> c_9()
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(0(),Y) -> c_12()
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(0(),Z) -> c_1()
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(0(),Z) -> c_4()
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(0(),Y) -> c_9()
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(0(),Y) -> c_12()
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak TRS:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,4,9,12}
by application of
Pre({1,4,9,12}) = {3,6,8,10,11,13}.
Here rules are labelled as follows:
1: 2ndsneg#(0(),Z) -> c_1()
2: 2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
3: 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
4: 2ndspos#(0(),Z) -> c_4()
5: 2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
6: 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
7: from#(X) -> c_7(from#(s(X)))
8: pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
9: plus#(0(),Y) -> c_9()
10: plus#(s(X),Y) -> c_10(plus#(X,Y))
11: square#(X) -> c_11(times#(X,X))
12: times#(0(),Y) -> c_12()
13: times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak DPs:
2ndsneg#(0(),Z) -> c_1()
2ndspos#(0(),Z) -> c_4()
plus#(0(),Y) -> c_9()
times#(0(),Y) -> c_12()
- Weak TRS:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
-->_1 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z)):2
2:S:2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
-->_1 2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z))):3
-->_1 2ndspos#(0(),Z) -> c_4():11
3:S:2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
4:S:2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
-->_1 2ndsneg#(0(),Z) -> c_1():10
-->_1 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z)):2
-->_1 2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z))):1
5:S:from#(X) -> c_7(from#(s(X)))
-->_1 from#(X) -> c_7(from#(s(X))):5
6:S:pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
-->_1 2ndspos#(0(),Z) -> c_4():11
-->_2 from#(X) -> c_7(from#(s(X))):5
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
-->_1 2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z))):3
7:S:plus#(s(X),Y) -> c_10(plus#(X,Y))
-->_1 plus#(0(),Y) -> c_9():12
-->_1 plus#(s(X),Y) -> c_10(plus#(X,Y)):7
8:S:square#(X) -> c_11(times#(X,X))
-->_1 times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y)):9
-->_1 times#(0(),Y) -> c_12():13
9:S:times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
-->_2 times#(0(),Y) -> c_12():13
-->_1 plus#(0(),Y) -> c_9():12
-->_2 times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y)):9
-->_1 plus#(s(X),Y) -> c_10(plus#(X,Y)):7
10:W:2ndsneg#(0(),Z) -> c_1()
11:W:2ndspos#(0(),Z) -> c_4()
12:W:plus#(0(),Y) -> c_9()
13:W:times#(0(),Y) -> c_12()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
13: times#(0(),Y) -> c_12()
12: plus#(0(),Y) -> c_9()
11: 2ndspos#(0(),Z) -> c_4()
10: 2ndsneg#(0(),Z) -> c_1()
* Step 5: RemoveHeads MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(s(X),Y) -> c_10(plus#(X,Y))
square#(X) -> c_11(times#(X,X))
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak TRS:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
-->_1 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z)):2
2:S:2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
-->_1 2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z))):3
3:S:2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
4:S:2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
-->_1 2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z)):2
-->_1 2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z))):1
5:S:from#(X) -> c_7(from#(s(X)))
-->_1 from#(X) -> c_7(from#(s(X))):5
6:S:pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
-->_2 from#(X) -> c_7(from#(s(X))):5
-->_1 2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z)):4
-->_1 2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z))):3
7:S:plus#(s(X),Y) -> c_10(plus#(X,Y))
-->_1 plus#(s(X),Y) -> c_10(plus#(X,Y)):7
8:S:square#(X) -> c_11(times#(X,X))
-->_1 times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y)):9
9:S:times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
-->_2 times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y)):9
-->_1 plus#(s(X),Y) -> c_10(plus#(X,Y)):7
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(8,square#(X) -> c_11(times#(X,X)))]
* Step 6: NaturalMI MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
plus#(s(X),Y) -> c_10(plus#(X,Y))
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak TRS:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_3) = {1},
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_7) = {1},
uargs(c_8) = {1,2},
uargs(c_10) = {1},
uargs(c_13) = {1,2}
Following symbols are considered usable:
{2ndsneg#,2ndspos#,from#,pi#,plus#,square#,times#}
TcT has computed the following interpretation:
p(0) = [1]
p(2ndsneg) = [2] x1 + [1]
p(2ndspos) = [1] x1 + [2]
p(cons) = [1]
p(cons2) = [0]
p(from) = [1]
p(negrecip) = [1]
p(pi) = [1] x1 + [2]
p(plus) = [4]
p(posrecip) = [2]
p(rcons) = [0]
p(rnil) = [1]
p(s) = [0]
p(square) = [4] x1 + [0]
p(times) = [1] x2 + [10]
p(2ndsneg#) = [0]
p(2ndspos#) = [0]
p(from#) = [2] x1 + [0]
p(pi#) = [1] x1 + [10]
p(plus#) = [0]
p(square#) = [1] x1 + [1]
p(times#) = [0]
p(c_1) = [1]
p(c_2) = [1] x1 + [0]
p(c_3) = [8] x1 + [0]
p(c_4) = [2]
p(c_5) = [8] x1 + [0]
p(c_6) = [4] x1 + [0]
p(c_7) = [8] x1 + [0]
p(c_8) = [1] x1 + [1] x2 + [0]
p(c_9) = [0]
p(c_10) = [4] x1 + [0]
p(c_11) = [8] x1 + [0]
p(c_12) = [1]
p(c_13) = [1] x1 + [8] x2 + [0]
Following rules are strictly oriented:
pi#(X) = [1] X + [10]
> [2]
= c_8(2ndspos#(X,from(0())),from#(0()))
Following rules are (at-least) weakly oriented:
2ndsneg#(s(N),cons(X,Z)) = [0]
>= [0]
= c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) = [0]
>= [0]
= c_3(2ndspos#(N,Z))
2ndspos#(s(N),cons(X,Z)) = [0]
>= [0]
= c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) = [0]
>= [0]
= c_6(2ndsneg#(N,Z))
from#(X) = [2] X + [0]
>= [0]
= c_7(from#(s(X)))
plus#(s(X),Y) = [0]
>= [0]
= c_10(plus#(X,Y))
times#(s(X),Y) = [0]
>= [0]
= c_13(plus#(Y,times(X,Y)),times#(X,Y))
* Step 7: Failure MAYBE
+ Considered Problem:
- Strict DPs:
2ndsneg#(s(N),cons(X,Z)) -> c_2(2ndsneg#(s(N),cons2(X,Z)))
2ndsneg#(s(N),cons2(X,cons(Y,Z))) -> c_3(2ndspos#(N,Z))
2ndspos#(s(N),cons(X,Z)) -> c_5(2ndspos#(s(N),cons2(X,Z)))
2ndspos#(s(N),cons2(X,cons(Y,Z))) -> c_6(2ndsneg#(N,Z))
from#(X) -> c_7(from#(s(X)))
plus#(s(X),Y) -> c_10(plus#(X,Y))
times#(s(X),Y) -> c_13(plus#(Y,times(X,Y)),times#(X,Y))
- Weak DPs:
pi#(X) -> c_8(2ndspos#(X,from(0())),from#(0()))
- Weak TRS:
from(X) -> cons(X,from(s(X)))
plus(0(),Y) -> Y
plus(s(X),Y) -> s(plus(X,Y))
times(0(),Y) -> 0()
times(s(X),Y) -> plus(Y,times(X,Y))
- Signature:
{2ndsneg/2,2ndspos/2,from/1,pi/1,plus/2,square/1,times/2,2ndsneg#/2,2ndspos#/2,from#/1,pi#/1,plus#/2
,square#/1,times#/2} / {0/0,cons/2,cons2/2,negrecip/1,posrecip/1,rcons/2,rnil/0,s/1,c_1/0,c_2/1,c_3/1,c_4/0
,c_5/1,c_6/1,c_7/1,c_8/2,c_9/0,c_10/1,c_11/1,c_12/0,c_13/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {2ndsneg#,2ndspos#,from#,pi#,plus#,square#
,times#} and constructors {0,cons,cons2,negrecip,posrecip,rcons,rnil,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE