MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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()
*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(x,#()) -> c_4()
+#(#(),x) -> c_5()
+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
0#(#()) -> c_10()
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
prod#(nil()) -> c_12()
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_14(0#(#()))
Weak DPs
and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(#(),x) -> c_1()
*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(x,#()) -> c_4()
+#(#(),x) -> c_5()
+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
0#(#()) -> c_10()
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
prod#(nil()) -> c_12()
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_14(0#(#()))
- Weak TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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/3,c_4/0
,c_5/0,c_6/2,c_7/1,c_8/1,c_9/3,c_10/0,c_11/2,c_12/0,c_13/2,c_14/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,4,5,10,12}
by application of
Pre({1,4,5,10,12}) = {2,3,6,7,8,9,11,13,14}.
Here rules are labelled as follows:
1: *#(#(),x) -> c_1()
2: *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
3: *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
4: +#(x,#()) -> c_4()
5: +#(#(),x) -> c_5()
6: +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
7: +#(0(x),1(y)) -> c_7(+#(x,y))
8: +#(1(x),0(y)) -> c_8(+#(x,y))
9: +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
10: 0#(#()) -> c_10()
11: prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
12: prod#(nil()) -> c_12()
13: sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
14: sum#(nil()) -> c_14(0#(#()))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
sum#(nil()) -> c_14(0#(#()))
- Weak DPs:
*#(#(),x) -> c_1()
+#(x,#()) -> c_4()
+#(#(),x) -> c_5()
0#(#()) -> c_10()
prod#(nil()) -> c_12()
- Weak TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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/3,c_4/0
,c_5/0,c_6/2,c_7/1,c_8/1,c_9/3,c_10/0,c_11/2,c_12/0,c_13/2,c_14/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
{9}
by application of
Pre({9}) = {8}.
Here rules are labelled as follows:
1: *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
2: *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
3: +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
4: +#(0(x),1(y)) -> c_7(+#(x,y))
5: +#(1(x),0(y)) -> c_8(+#(x,y))
6: +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
7: prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
8: sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
9: sum#(nil()) -> c_14(0#(#()))
10: *#(#(),x) -> c_1()
11: +#(x,#()) -> c_4()
12: +#(#(),x) -> c_5()
13: 0#(#()) -> c_10()
14: prod#(nil()) -> c_12()
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
- Weak DPs:
*#(#(),x) -> c_1()
+#(x,#()) -> c_4()
+#(#(),x) -> c_5()
0#(#()) -> c_10()
prod#(nil()) -> c_12()
sum#(nil()) -> c_14(0#(#()))
- Weak TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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/3,c_4/0
,c_5/0,c_6/2,c_7/1,c_8/1,c_9/3,c_10/0,c_11/2,c_12/0,c_13/2,c_14/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:*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
-->_2 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_1 0#(#()) -> c_10():12
-->_2 *#(#(),x) -> c_1():9
-->_2 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
2:S:*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
-->_2 0#(#()) -> c_10():12
-->_1 +#(#(),x) -> c_5():11
-->_1 +#(x,#()) -> c_4():10
-->_3 *#(#(),x) -> c_1():9
-->_3 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_3 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
3:S:+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
-->_2 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_2 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_2 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 0#(#()) -> c_10():12
-->_2 +#(#(),x) -> c_5():11
-->_2 +#(x,#()) -> c_4():10
-->_2 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
4:S:+#(0(x),1(y)) -> c_7(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(#(),x) -> c_5():11
-->_1 +#(x,#()) -> c_4():10
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
5:S:+#(1(x),0(y)) -> c_8(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(#(),x) -> c_5():11
-->_1 +#(x,#()) -> c_4():10
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
6:S:+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
-->_1 0#(#()) -> c_10():12
-->_3 +#(#(),x) -> c_5():11
-->_2 +#(#(),x) -> c_5():11
-->_3 +#(x,#()) -> c_4():10
-->_3 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_2 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_3 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_3 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_2 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_3 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
7:S:prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
-->_2 prod#(nil()) -> c_12():13
-->_1 *#(#(),x) -> c_1():9
-->_2 prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l)):7
-->_1 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_1 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
8:S:sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
-->_2 sum#(nil()) -> c_14(0#(#())):14
-->_1 +#(#(),x) -> c_5():11
-->_1 +#(x,#()) -> c_4():10
-->_2 sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l)):8
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
9:W:*#(#(),x) -> c_1()
10:W:+#(x,#()) -> c_4()
11:W:+#(#(),x) -> c_5()
12:W:0#(#()) -> c_10()
13:W:prod#(nil()) -> c_12()
14:W:sum#(nil()) -> c_14(0#(#()))
-->_1 0#(#()) -> c_10():12
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
14: sum#(nil()) -> c_14(0#(#()))
13: prod#(nil()) -> c_12()
9: *#(#(),x) -> c_1()
10: +#(x,#()) -> c_4()
11: +#(#(),x) -> c_5()
12: 0#(#()) -> c_10()
* Step 5: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
- Weak TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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/3,c_4/0
,c_5/0,c_6/2,c_7/1,c_8/1,c_9/3,c_10/0,c_11/2,c_12/0,c_13/2,c_14/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:*#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y))
-->_2 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_2 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
2:S:*#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
-->_3 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_3 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
3:S:+#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y))
-->_2 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_2 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_2 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_2 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
4:S:+#(0(x),1(y)) -> c_7(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
5:S:+#(1(x),0(y)) -> c_8(+#(x,y))
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
6:S:+#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y))
-->_3 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_2 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_3 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_3 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_2 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_3 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
7:S:prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
-->_2 prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l)):7
-->_1 *#(1(x),y) -> c_3(+#(0(*(x,y)),y),0#(*(x,y)),*#(x,y)):2
-->_1 *#(0(x),y) -> c_2(0#(*(x,y)),*#(x,y)):1
8:S:sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
-->_2 sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l)):8
-->_1 +#(1(x),1(y)) -> c_9(0#(+(+(x,y),1(#()))),+#(+(x,y),1(#())),+#(x,y)):6
-->_1 +#(1(x),0(y)) -> c_8(+#(x,y)):5
-->_1 +#(0(x),1(y)) -> c_7(+#(x,y)):4
-->_1 +#(0(x),0(y)) -> c_6(0#(+(x,y)),+#(x,y)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
*#(0(x),y) -> c_2(*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),*#(x,y))
+#(0(x),0(y)) -> c_6(+#(x,y))
+#(1(x),1(y)) -> c_9(+#(+(x,y),1(#())),+#(x,y))
* Step 6: Failure MAYBE
+ Considered Problem:
- Strict DPs:
*#(0(x),y) -> c_2(*#(x,y))
*#(1(x),y) -> c_3(+#(0(*(x,y)),y),*#(x,y))
+#(0(x),0(y)) -> c_6(+#(x,y))
+#(0(x),1(y)) -> c_7(+#(x,y))
+#(1(x),0(y)) -> c_8(+#(x,y))
+#(1(x),1(y)) -> c_9(+#(+(x,y),1(#())),+#(x,y))
prod#(cons(x,l)) -> c_11(*#(x,prod(l)),prod#(l))
sum#(cons(x,l)) -> c_13(+#(x,sum(l)),sum#(l))
- Weak TRS:
*(#(),x) -> #()
*(0(x),y) -> 0(*(x,y))
*(1(x),y) -> +(0(*(x,y)),y)
+(x,#()) -> x
+(#(),x) -> x
+(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/1,c_3/2,c_4/0
,c_5/0,c_6/1,c_7/1,c_8/1,c_9/2,c_10/0,c_11/2,c_12/0,c_13/2,c_14/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