MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: lcs(x,e()) -> 0() lcs(a(x),a(y)) -> s(lcs(x,y)) lcs(a(x),b(y)) -> max(lcs(x,b(y)),lcs(a(x),y)) lcs(b(x),a(y)) -> max(lcs(x,a(y)),lcs(b(x),y)) lcs(b(x),b(y)) -> s(lcs(x,y)) lcs(e(),y) -> 0() max(x,0()) -> 0() max(0(),y) -> 0() max(s(x),s(y)) -> max(x,y) - Signature: {lcs/2,max/2} / {0/0,a/1,b/1,e/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {lcs,max} and constructors {0,a,b,e,s} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs lcs#(x,e()) -> c_1() lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) lcs#(e(),y) -> c_6() max#(x,0()) -> c_7() max#(0(),y) -> c_8() max#(s(x),s(y)) -> c_9(max#(x,y)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: lcs#(x,e()) -> c_1() lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) lcs#(e(),y) -> c_6() max#(x,0()) -> c_7() max#(0(),y) -> c_8() max#(s(x),s(y)) -> c_9(max#(x,y)) - Weak TRS: lcs(x,e()) -> 0() lcs(a(x),a(y)) -> s(lcs(x,y)) lcs(a(x),b(y)) -> max(lcs(x,b(y)),lcs(a(x),y)) lcs(b(x),a(y)) -> max(lcs(x,a(y)),lcs(b(x),y)) lcs(b(x),b(y)) -> s(lcs(x,y)) lcs(e(),y) -> 0() max(x,0()) -> 0() max(0(),y) -> 0() max(s(x),s(y)) -> max(x,y) - Signature: {lcs/2,max/2,lcs#/2,max#/2} / {0/0,a/1,b/1,e/0,s/1,c_1/0,c_2/1,c_3/3,c_4/3,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {lcs#,max#} and constructors {0,a,b,e,s} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,6,7,8} by application of Pre({1,6,7,8}) = {2,3,4,5,9}. Here rules are labelled as follows: 1: lcs#(x,e()) -> c_1() 2: lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) 3: lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) 4: lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) 5: lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) 6: lcs#(e(),y) -> c_6() 7: max#(x,0()) -> c_7() 8: max#(0(),y) -> c_8() 9: max#(s(x),s(y)) -> c_9(max#(x,y)) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) max#(s(x),s(y)) -> c_9(max#(x,y)) - Weak DPs: lcs#(x,e()) -> c_1() lcs#(e(),y) -> c_6() max#(x,0()) -> c_7() max#(0(),y) -> c_8() - Weak TRS: lcs(x,e()) -> 0() lcs(a(x),a(y)) -> s(lcs(x,y)) lcs(a(x),b(y)) -> max(lcs(x,b(y)),lcs(a(x),y)) lcs(b(x),a(y)) -> max(lcs(x,a(y)),lcs(b(x),y)) lcs(b(x),b(y)) -> s(lcs(x,y)) lcs(e(),y) -> 0() max(x,0()) -> 0() max(0(),y) -> 0() max(s(x),s(y)) -> max(x,y) - Signature: {lcs/2,max/2,lcs#/2,max#/2} / {0/0,a/1,b/1,e/0,s/1,c_1/0,c_2/1,c_3/3,c_4/3,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {lcs#,max#} and constructors {0,a,b,e,s} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) -->_1 lcs#(b(x),b(y)) -> c_5(lcs#(x,y)):4 -->_1 lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)):3 -->_1 lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)):2 -->_1 lcs#(e(),y) -> c_6():7 -->_1 lcs#(x,e()) -> c_1():6 -->_1 lcs#(a(x),a(y)) -> c_2(lcs#(x,y)):1 2:S:lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) -->_1 max#(s(x),s(y)) -> c_9(max#(x,y)):5 -->_2 lcs#(b(x),b(y)) -> c_5(lcs#(x,y)):4 -->_1 max#(0(),y) -> c_8():9 -->_1 max#(x,0()) -> c_7():8 -->_2 lcs#(e(),y) -> c_6():7 -->_3 lcs#(x,e()) -> c_1():6 -->_3 lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)):2 -->_2 lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)):2 -->_3 lcs#(a(x),a(y)) -> c_2(lcs#(x,y)):1 3:S:lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) -->_1 max#(s(x),s(y)) -> c_9(max#(x,y)):5 -->_3 lcs#(b(x),b(y)) -> c_5(lcs#(x,y)):4 -->_1 max#(0(),y) -> c_8():9 -->_1 max#(x,0()) -> c_7():8 -->_2 lcs#(e(),y) -> c_6():7 -->_3 lcs#(x,e()) -> c_1():6 -->_3 lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)):3 -->_2 lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)):3 -->_2 lcs#(a(x),a(y)) -> c_2(lcs#(x,y)):1 4:S:lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) -->_1 lcs#(e(),y) -> c_6():7 -->_1 lcs#(x,e()) -> c_1():6 -->_1 lcs#(b(x),b(y)) -> c_5(lcs#(x,y)):4 -->_1 lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)):3 -->_1 lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)):2 -->_1 lcs#(a(x),a(y)) -> c_2(lcs#(x,y)):1 5:S:max#(s(x),s(y)) -> c_9(max#(x,y)) -->_1 max#(0(),y) -> c_8():9 -->_1 max#(x,0()) -> c_7():8 -->_1 max#(s(x),s(y)) -> c_9(max#(x,y)):5 6:W:lcs#(x,e()) -> c_1() 7:W:lcs#(e(),y) -> c_6() 8:W:max#(x,0()) -> c_7() 9:W:max#(0(),y) -> c_8() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 8: max#(x,0()) -> c_7() 9: max#(0(),y) -> c_8() 6: lcs#(x,e()) -> c_1() 7: lcs#(e(),y) -> c_6() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: lcs#(a(x),a(y)) -> c_2(lcs#(x,y)) lcs#(a(x),b(y)) -> c_3(max#(lcs(x,b(y)),lcs(a(x),y)),lcs#(x,b(y)),lcs#(a(x),y)) lcs#(b(x),a(y)) -> c_4(max#(lcs(x,a(y)),lcs(b(x),y)),lcs#(x,a(y)),lcs#(b(x),y)) lcs#(b(x),b(y)) -> c_5(lcs#(x,y)) max#(s(x),s(y)) -> c_9(max#(x,y)) - Weak TRS: lcs(x,e()) -> 0() lcs(a(x),a(y)) -> s(lcs(x,y)) lcs(a(x),b(y)) -> max(lcs(x,b(y)),lcs(a(x),y)) lcs(b(x),a(y)) -> max(lcs(x,a(y)),lcs(b(x),y)) lcs(b(x),b(y)) -> s(lcs(x,y)) lcs(e(),y) -> 0() max(x,0()) -> 0() max(0(),y) -> 0() max(s(x),s(y)) -> max(x,y) - Signature: {lcs/2,max/2,lcs#/2,max#/2} / {0/0,a/1,b/1,e/0,s/1,c_1/0,c_2/1,c_3/3,c_4/3,c_5/1,c_6/0,c_7/0,c_8/0,c_9/1} - Obligation: innermost runtime complexity wrt. defined symbols {lcs#,max#} and constructors {0,a,b,e,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE