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)) O(0()) -> 0() - Signature: {*/2,+/2,O/1} / {0/0,I/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,+,O} and constructors {0,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)) O#(0()) -> c_11() 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)) O#(0()) -> c_11() - 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)) O(0()) -> 0() - Signature: {*/2,+/2,O/1,*#/2,+#/2,O#/1} / {0/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} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,O#} and constructors {0,I} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,5,6,11} by application of Pre({1,2,5,6,11}) = {3,4,7,8,9,10}. 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: O#(0()) -> c_11() * 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)) - Weak DPs: *#(x,0()) -> c_1() *#(0(),x) -> c_2() +#(x,0()) -> c_5() +#(0(),x) -> c_6() O#(0()) -> c_11() - 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)) O(0()) -> 0() - Signature: {*/2,+/2,O/1,*#/2,+#/2,O#/1} / {0/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} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,O#} and constructors {0,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_11():11 -->_1 +#(0(),x) -> c_6():10 -->_1 +#(x,0()) -> c_5():9 -->_3 *#(0(),x) -> c_2():8 -->_3 *#(x,0()) -> c_1():7 -->_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_11():11 -->_2 *#(0(),x) -> c_2():8 -->_2 *#(x,0()) -> c_1():7 -->_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_11():11 -->_3 +#(0(),x) -> c_6():10 -->_2 +#(0(),x) -> c_6():10 -->_3 +#(x,0()) -> c_5():9 -->_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():10 -->_1 +#(x,0()) -> c_5():9 -->_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():10 -->_1 +#(x,0()) -> c_5():9 -->_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_11():11 -->_2 +#(0(),x) -> c_6():10 -->_2 +#(x,0()) -> c_5():9 -->_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:W:*#(x,0()) -> c_1() 8:W:*#(0(),x) -> c_2() 9:W:+#(x,0()) -> c_5() 10:W:+#(0(),x) -> c_6() 11:W:O#(0()) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 7: *#(x,0()) -> c_1() 8: *#(0(),x) -> c_2() 9: +#(x,0()) -> c_5() 10: +#(0(),x) -> c_6() 11: O#(0()) -> c_11() * 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)) - 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)) O(0()) -> 0() - Signature: {*/2,+/2,O/1,*#/2,+#/2,O#/1} / {0/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} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,O#} and constructors {0,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 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)) * 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)) - 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)) O(0()) -> 0() - Signature: {*/2,+/2,O/1,*#/2,+#/2,O#/1} / {0/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} - Obligation: innermost runtime complexity wrt. defined symbols {*#,+#,O#} and constructors {0,I} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE