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