WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2} / {c/0,c1/1,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT,LESSLEAVES,concat,lessleaves} and constructors {c ,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2} / {c/0,c1/1,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT,LESSLEAVES,concat,lessleaves} and constructors {c ,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2} / {c/0,c1/1,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT,LESSLEAVES,concat,lessleaves} and constructors {c ,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: CONCAT(y,z){y -> cons(x,y)} = CONCAT(cons(x,y),z) ->^+ c1(CONCAT(y,z)) = C[CONCAT(y,z) = CONCAT(y,z){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2} / {c/0,c1/1,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT,LESSLEAVES,concat,lessleaves} and constructors {c ,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) CONCAT#(leaf(),z0) -> c_2() LESSLEAVES#(z0,leaf()) -> c_3() LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() Weak DPs concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) concat#(leaf(),z0) -> c_8() lessleaves#(z0,leaf()) -> c_9() lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) lessleaves#(leaf(),cons(z0,z1)) -> c_11() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) CONCAT#(leaf(),z0) -> c_2() LESSLEAVES#(z0,leaf()) -> c_3() LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() - Weak DPs: concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) concat#(leaf(),z0) -> c_8() lessleaves#(z0,leaf()) -> c_9() lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) lessleaves#(leaf(),cons(z0,z1)) -> c_11() - Weak TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/4,c_5/4,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,6} by application of Pre({2,3,6}) = {1,4,5}. Here rules are labelled as follows: 1: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) 2: CONCAT#(leaf(),z0) -> c_2() 3: LESSLEAVES#(z0,leaf()) -> c_3() 4: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) 5: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) 6: LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() 7: concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) 8: concat#(leaf(),z0) -> c_8() 9: lessleaves#(z0,leaf()) -> c_9() 10: lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) 11: lessleaves#(leaf(),cons(z0,z1)) -> c_11() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) - Weak DPs: CONCAT#(leaf(),z0) -> c_2() LESSLEAVES#(z0,leaf()) -> c_3() LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) concat#(leaf(),z0) -> c_8() lessleaves#(z0,leaf()) -> c_9() lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) lessleaves#(leaf(),cons(z0,z1)) -> c_11() - Weak TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/4,c_5/4,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) -->_1 CONCAT#(leaf(),z0) -> c_2():4 -->_1 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 2:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) -->_3 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 -->_2 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):3 -->_3 concat#(leaf(),z0) -> c_8():8 -->_2 concat#(leaf(),z0) -> c_8():8 -->_1 LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6():6 -->_1 LESSLEAVES#(z0,leaf()) -> c_3():5 -->_4 CONCAT#(leaf(),z0) -> c_2():4 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):2 -->_4 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 3:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) -->_3 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 -->_2 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 -->_3 concat#(leaf(),z0) -> c_8():8 -->_2 concat#(leaf(),z0) -> c_8():8 -->_1 LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6():6 -->_1 LESSLEAVES#(z0,leaf()) -> c_3():5 -->_4 CONCAT#(leaf(),z0) -> c_2():4 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):3 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):2 -->_4 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 4:W:CONCAT#(leaf(),z0) -> c_2() 5:W:LESSLEAVES#(z0,leaf()) -> c_3() 6:W:LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() 7:W:concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) -->_1 concat#(leaf(),z0) -> c_8():8 -->_1 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 8:W:concat#(leaf(),z0) -> c_8() 9:W:lessleaves#(z0,leaf()) -> c_9() 10:W:lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) -->_1 lessleaves#(leaf(),cons(z0,z1)) -> c_11():11 -->_1 lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)):10 -->_1 lessleaves#(z0,leaf()) -> c_9():9 -->_3 concat#(leaf(),z0) -> c_8():8 -->_2 concat#(leaf(),z0) -> c_8():8 -->_3 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 -->_2 concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)):7 11:W:lessleaves#(leaf(),cons(z0,z1)) -> c_11() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: lessleaves#(cons(z0,z1),cons(z2,z3)) -> c_10(lessleaves#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3)) 11: lessleaves#(leaf(),cons(z0,z1)) -> c_11() 9: lessleaves#(z0,leaf()) -> c_9() 5: LESSLEAVES#(z0,leaf()) -> c_3() 6: LESSLEAVES#(leaf(),cons(z0,z1)) -> c_6() 7: concat#(cons(z0,z1),z2) -> c_7(concat#(z1,z2)) 8: concat#(leaf(),z0) -> c_8() 4: CONCAT#(leaf(),z0) -> c_2() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) - Weak TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/4,c_5/4,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) -->_1 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 2:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)) -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):3 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):2 -->_4 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 3:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)) -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z2,z3)):3 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,concat#(z0,z1) ,concat#(z2,z3) ,CONCAT#(z0,z1)):2 -->_4 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) - Weak TRS: CONCAT(cons(z0,z1),z2) -> c1(CONCAT(z1,z2)) CONCAT(leaf(),z0) -> c() LESSLEAVES(z0,leaf()) -> c2() LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c4(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z0,z1)) LESSLEAVES(cons(z0,z1),cons(z2,z3)) -> c5(LESSLEAVES(concat(z0,z1),concat(z2,z3)),CONCAT(z2,z3)) LESSLEAVES(leaf(),cons(z0,z1)) -> c3() concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 lessleaves(z0,leaf()) -> false() lessleaves(cons(z0,z1),cons(z2,z3)) -> lessleaves(concat(z0,z1),concat(z2,z3)) lessleaves(leaf(),cons(z0,z1)) -> true() - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) ** Step 1.b:6: DecomposeDG. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) and a lower component CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) Further, following extension rules are added to the lower component. LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> LESSLEAVES#(concat(z0,z1),concat(z2,z3)) *** Step 1.b:6.a:1: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z0,z1)) -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z2,z3)):2 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z0,z1)):1 2:S:LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)),CONCAT#(z2,z3)) -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z2,z3)):2 -->_1 LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3)) ,CONCAT#(z0,z1)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) *** Step 1.b:6.a:2: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {concat,CONCAT#,LESSLEAVES#,concat#,lessleaves#} TcT has computed the following interpretation: p(CONCAT) = [1] p(LESSLEAVES) = [2] x1 + [1] x2 + [1] p(c) = [8] p(c1) = [4] p(c2) = [2] p(c3) = [2] p(c4) = [1] x1 + [1] x2 + [1] p(c5) = [1] x2 + [2] p(concat) = [1] x1 + [1] x2 + [2] p(cons) = [1] x1 + [1] x2 + [10] p(false) = [0] p(leaf) = [1] p(lessleaves) = [1] x1 + [2] x2 + [8] p(true) = [4] p(CONCAT#) = [0] p(LESSLEAVES#) = [1] x2 + [14] p(concat#) = [1] x1 + [2] p(lessleaves#) = [2] x1 + [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [1] p(c_3) = [1] p(c_4) = [1] x1 + [1] p(c_5) = [1] x1 + [8] p(c_6) = [2] p(c_7) = [1] x1 + [1] p(c_8) = [2] p(c_9) = [4] p(c_10) = [1] x1 + [4] x3 + [0] p(c_11) = [0] Following rules are strictly oriented: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z2 + [1] z3 + [24] > [1] z2 + [1] z3 + [17] = c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) Following rules are (at-least) weakly oriented: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z2 + [1] z3 + [24] >= [1] z2 + [1] z3 + [24] = c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [12] >= [1] z0 + [1] z1 + [1] z2 + [12] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [3] >= [1] z0 + [0] = z0 *** Step 1.b:6.a:3: WeightGap. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) - Weak DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(cons) = {2}, uargs(LESSLEAVES#) = {1,2}, uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(CONCAT) = [0] p(LESSLEAVES) = [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c2) = [0] p(c3) = [0] p(c4) = [1] x1 + [1] x2 + [0] p(c5) = [0] p(concat) = [1] x1 + [1] x2 + [1] p(cons) = [1] x1 + [1] x2 + [6] p(false) = [0] p(leaf) = [0] p(lessleaves) = [0] p(true) = [0] p(CONCAT#) = [2] x2 + [0] p(LESSLEAVES#) = [1] x1 + [1] x2 + [3] p(concat#) = [1] x1 + [0] p(lessleaves#) = [1] x1 + [1] x2 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [1] p(c_4) = [1] x1 + [10] p(c_5) = [1] x1 + [3] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [0] Following rules are strictly oriented: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [15] > [1] z0 + [1] z1 + [1] z2 + [1] z3 + [8] = c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) Following rules are (at-least) weakly oriented: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [1] z0 + [1] z1 + [1] z2 + [1] z3 + [15] >= [1] z0 + [1] z1 + [1] z2 + [1] z3 + [15] = c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [7] >= [1] z0 + [1] z1 + [1] z2 + [7] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [1] >= [1] z0 + [0] = z0 Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 1.b:6.a:4: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_4(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> c_5(LESSLEAVES#(concat(z0,z1),concat(z2,z3))) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:6.b:1: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) - Weak DPs: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> LESSLEAVES#(concat(z0,z1),concat(z2,z3)) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1} Following symbols are considered usable: {concat,CONCAT#,LESSLEAVES#,concat#,lessleaves#} TcT has computed the following interpretation: p(CONCAT) = [0] p(LESSLEAVES) = [0] p(c) = [0] p(c1) = [1] x1 + [0] p(c2) = [0] p(c3) = [0] p(c4) = [1] x1 + [1] p(c5) = [0] p(concat) = [1] x1 + [1] x2 + [0] p(cons) = [1] x1 + [1] x2 + [1] p(false) = [1] p(leaf) = [0] p(lessleaves) = [0] p(true) = [2] p(CONCAT#) = [2] x1 + [2] x2 + [3] p(LESSLEAVES#) = [4] x1 + [2] x2 + [14] p(concat#) = [1] x2 + [2] p(lessleaves#) = [1] x2 + [1] p(c_1) = [1] x1 + [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [1] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] p(c_8) = [2] p(c_9) = [8] p(c_10) = [1] x2 + [2] p(c_11) = [1] Following rules are strictly oriented: CONCAT#(cons(z0,z1),z2) = [2] z0 + [2] z1 + [2] z2 + [5] > [2] z1 + [2] z2 + [3] = c_1(CONCAT#(z1,z2)) Following rules are (at-least) weakly oriented: LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [4] z0 + [4] z1 + [2] z2 + [2] z3 + [20] >= [2] z0 + [2] z1 + [3] = CONCAT#(z0,z1) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [4] z0 + [4] z1 + [2] z2 + [2] z3 + [20] >= [2] z2 + [2] z3 + [3] = CONCAT#(z2,z3) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) = [4] z0 + [4] z1 + [2] z2 + [2] z3 + [20] >= [4] z0 + [4] z1 + [2] z2 + [2] z3 + [14] = LESSLEAVES#(concat(z0,z1),concat(z2,z3)) concat(cons(z0,z1),z2) = [1] z0 + [1] z1 + [1] z2 + [1] >= [1] z0 + [1] z1 + [1] z2 + [1] = cons(z0,concat(z1,z2)) concat(leaf(),z0) = [1] z0 + [0] >= [1] z0 + [0] = z0 *** Step 1.b:6.b:2: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: CONCAT#(cons(z0,z1),z2) -> c_1(CONCAT#(z1,z2)) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z0,z1) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> CONCAT#(z2,z3) LESSLEAVES#(cons(z0,z1),cons(z2,z3)) -> LESSLEAVES#(concat(z0,z1),concat(z2,z3)) - Weak TRS: concat(cons(z0,z1),z2) -> cons(z0,concat(z1,z2)) concat(leaf(),z0) -> z0 - Signature: {CONCAT/2,LESSLEAVES/2,concat/2,lessleaves/2,CONCAT#/2,LESSLEAVES#/2,concat#/2,lessleaves#/2} / {c/0,c1/1 ,c2/0,c3/0,c4/2,c5/2,cons/2,false/0,leaf/0,true/0,c_1/1,c_2/0,c_3/0,c_4/2,c_5/2,c_6/0,c_7/1,c_8/0,c_9/0 ,c_10/3,c_11/0} - Obligation: innermost runtime complexity wrt. defined symbols {CONCAT#,LESSLEAVES#,concat# ,lessleaves#} and constructors {c,c1,c2,c3,c4,c5,cons,false,leaf,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))