MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1} / {#/0,1/1,cons/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {*,+,0,prod,sum} and constructors {#,1,cons,nil}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
*#(#(),x) -> c_1()
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(x,#()) -> c_5()
+#(#(),x) -> c_6()
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
0#(#()) -> c_12()
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
prod#(nil()) -> c_14()
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_16(0#(#()))
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(#(),x) -> c_1()
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(x,#()) -> c_5()
+#(#(),x) -> c_6()
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
0#(#()) -> c_12()
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
prod#(nil()) -> c_14()
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_16(0#(#()))
- Weak TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1,*#/2,+#/2,0#/1,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3
,c_5/0,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/3,c_12/0,c_13/2,c_14/0,c_15/2,c_16/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,0#,prod#,sum#} and constructors {#,1,cons,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,5,6,12,14}
by application of
Pre({1,5,6,12,14}) = {2,3,4,7,8,9,10,11,13,15,16}.
Here rules are labelled as follows:
1: *#(#(),x) -> c_1()
2: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
3: *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
4: *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
5: +#(x,#()) -> c_5()
6: +#(#(),x) -> c_6()
7: +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
8: +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
9: +#(0(x),1(y)) -> c_9(+#(x,y))
10: +#(1(x),0(y)) -> c_10(+#(x,y))
11: +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
12: 0#(#()) -> c_12()
13: prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
14: prod#(nil()) -> c_14()
15: sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
16: sum#(nil()) -> c_16(0#(#()))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_16(0#(#()))
- Weak DPs:
*#(#(),x) -> c_1()
+#(x,#()) -> c_5()
+#(#(),x) -> c_6()
0#(#()) -> c_12()
prod#(nil()) -> c_14()
- Weak TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1,*#/2,+#/2,0#/1,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3
,c_5/0,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/3,c_12/0,c_13/2,c_14/0,c_15/2,c_16/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,0#,prod#,sum#} and constructors {#,1,cons,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{11}
by application of
Pre({11}) = {10}.
Here rules are labelled as follows:
1: *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
2: *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
3: *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
4: +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
5: +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
6: +#(0(x),1(y)) -> c_9(+#(x,y))
7: +#(1(x),0(y)) -> c_10(+#(x,y))
8: +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
9: prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
10: sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
11: sum#(nil()) -> c_16(0#(#()))
12: *#(#(),x) -> c_1()
13: +#(x,#()) -> c_5()
14: +#(#(),x) -> c_6()
15: 0#(#()) -> c_12()
16: prod#(nil()) -> c_14()
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
- Weak DPs:
*#(#(),x) -> c_1()
+#(x,#()) -> c_5()
+#(#(),x) -> c_6()
0#(#()) -> c_12()
prod#(nil()) -> c_14()
sum#(nil()) -> c_16(0#(#()))
- Weak TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1,*#/2,+#/2,0#/1,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3
,c_5/0,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/3,c_12/0,c_13/2,c_14/0,c_15/2,c_16/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,0#,prod#,sum#} and constructors {#,1,cons,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
-->_2 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_1 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_2 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_1 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_2 *#(#(),x) -> c_1():11
-->_1 *#(#(),x) -> c_1():11
-->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
-->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
2:S:*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
-->_2 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_1 0#(#()) -> c_12():14
-->_2 *#(#(),x) -> c_1():11
-->_2 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
3:S:*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_2 0#(#()) -> c_12():14
-->_1 +#(#(),x) -> c_6():13
-->_1 +#(x,#()) -> c_5():12
-->_3 *#(#(),x) -> c_1():11
-->_3 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_3 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_3 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
4:S:+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_2 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_2 +#(#(),x) -> c_6():13
-->_1 +#(#(),x) -> c_6():13
-->_2 +#(x,#()) -> c_5():12
-->_1 +#(x,#()) -> c_5():12
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
5:S:+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 0#(#()) -> c_12():14
-->_2 +#(#(),x) -> c_6():13
-->_2 +#(x,#()) -> c_5():12
-->_2 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
6:S:+#(0(x),1(y)) -> c_9(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(#(),x) -> c_6():13
-->_1 +#(x,#()) -> c_5():12
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
7:S:+#(1(x),0(y)) -> c_10(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(#(),x) -> c_6():13
-->_1 +#(x,#()) -> c_5():12
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
8:S:+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
-->_1 0#(#()) -> c_12():14
-->_3 +#(#(),x) -> c_6():13
-->_2 +#(#(),x) -> c_6():13
-->_3 +#(x,#()) -> c_5():12
-->_3 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_3 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_3 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_3 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_3 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
9:S:prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
-->_2 prod#(nil()) -> c_14():15
-->_1 *#(#(),x) -> c_1():11
-->_2 prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l)):9
-->_1 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_1 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
10:S:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
-->_2 sum#(nil()) -> c_16(0#(#())):16
-->_1 +#(#(),x) -> c_6():13
-->_1 +#(x,#()) -> c_5():12
-->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):10
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
11:W:*#(#(),x) -> c_1()
12:W:+#(x,#()) -> c_5()
13:W:+#(#(),x) -> c_6()
14:W:0#(#()) -> c_12()
15:W:prod#(nil()) -> c_14()
16:W:sum#(nil()) -> c_16(0#(#()))
-->_1 0#(#()) -> c_12():14
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
16: sum#(nil()) -> c_16(0#(#()))
15: prod#(nil()) -> c_14()
11: *#(#(),x) -> c_1()
12: +#(x,#()) -> c_5()
13: +#(#(),x) -> c_6()
14: 0#(#()) -> c_12()
* Step 5: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
- Weak TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1,*#/2,+#/2,0#/1,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/0,c_2/2,c_3/2,c_4/3
,c_5/0,c_6/0,c_7/2,c_8/2,c_9/1,c_10/1,c_11/3,c_12/0,c_13/2,c_14/0,c_15/2,c_16/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,0#,prod#,sum#} and constructors {#,1,cons,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
-->_2 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_1 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_2 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_1 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
-->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
2:S:*#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y))
-->_2 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_2 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_2 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
3:S:*#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_3 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_3 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_3 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
4:S:+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_2 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
5:S:+#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y))
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_2 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
6:S:+#(0(x),1(y)) -> c_9(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
7:S:+#(1(x),0(y)) -> c_10(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
8:S:+#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
-->_3 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_2 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_3 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_3 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_2 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_3 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_3 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
-->_2 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
9:S:prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
-->_2 prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l)):9
-->_1 *#(1(x),y) -> c_4(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):3
-->_1 *#(0(x),y) -> c_3(0#(*(x,y)),*#(x,y)):2
-->_1 *#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z)):1
10:S:sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
-->_2 sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l)):10
-->_1 +#(1(x),1(y)) -> c_11(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):8
-->_1 +#(1(x),0(y)) -> c_10(+#(x,y)):7
-->_1 +#(0(x),1(y)) -> c_9(+#(x,y)):6
-->_1 +#(0(x),0(y)) -> c_8(0#(+(x,y)),+#(x,y)):5
-->_1 +#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z)):4
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
*#(0(x),y) -> c_3(*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),*#(x,y))
+#(0(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_11(+#(+(x,y),1(#())),+#(x,y))
* Step 6: Failure MAYBE
+ Considered Problem:
- Strict DPs:
*#(*(x,y),z) -> c_2(*#(x,*(y,z)),*#(y,z))
*#(0(x),y) -> c_3(*#(x,y))
*#(1(x),y) -> c_4(+#(0(*(x,y)),y),*#(x,y))
+#(+(x,y),z) -> c_7(+#(x,+(y,z)),+#(y,z))
+#(0(x),0(y)) -> c_8(+#(x,y))
+#(0(x),1(y)) -> c_9(+#(x,y))
+#(1(x),0(y)) -> c_10(+#(x,y))
+#(1(x),1(y)) -> c_11(+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_13(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_15(+#(x,sum(l)),sum#(l))
- Weak TRS:
*(#(),x) -> #()
*(*(x,y),z) -> *(x,*(y,z))
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(+(x,y),z) -> +(x,+(y,z))
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#())))
0(#()) -> #()
prod(cons(x,l)) -> *(x,prod(l))
prod(nil()) -> 1(#())
sum(cons(x,l)) -> +(x,sum(l))
sum(nil()) -> 0(#())
- Signature:
{*/2,+/2,0/1,prod/1,sum/1,*#/2,+#/2,0#/1,prod#/1,sum#/1} / {#/0,1/1,cons/2,nil/0,c_1/0,c_2/2,c_3/1,c_4/2
,c_5/0,c_6/0,c_7/2,c_8/1,c_9/1,c_10/1,c_11/2,c_12/0,c_13/2,c_14/0,c_15/2,c_16/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {*#,+#,0#,prod#,sum#} and constructors {#,1,cons,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE