WORST_CASE(Omega(n^1),O(n^5)) * Step 1: Sum WORST_CASE(Omega(n^1),O(n^5)) + Considered Problem: - Strict TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1} / {mark/1,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,active,cons,from,proper,s,top} and constructors {mark ,ok} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1} / {mark/1,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,active,cons,from,proper,s,top} and constructors {mark ,ok} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: 2nd(x){x -> mark(x)} = 2nd(mark(x)) ->^+ mark(2nd(x)) = C[2nd(x) = 2nd(x){}] ** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^5)) + Considered Problem: - Strict TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1} / {mark/1,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,active,cons,from,proper,s,top} and constructors {mark ,ok} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(2nd(cons(X,cons(Y,Z)))) -> c_4() active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) Weak DPs and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(2nd(cons(X,cons(Y,Z)))) -> c_4() active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4} by application of Pre({4}) = {3,5,6,8,20}. Here rules are labelled as follows: 1: 2nd#(mark(X)) -> c_1(2nd#(X)) 2: 2nd#(ok(X)) -> c_2(2nd#(X)) 3: active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) 4: active#(2nd(cons(X,cons(Y,Z)))) -> c_4() 5: active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) 6: active#(from(X)) -> c_6(from#(active(X)),active#(X)) 7: active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) 8: active#(s(X)) -> c_8(s#(active(X)),active#(X)) 9: cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) 10: cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) 11: from#(mark(X)) -> c_11(from#(X)) 12: from#(ok(X)) -> c_12(from#(X)) 13: proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) 14: proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 15: proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) 16: proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) 17: s#(mark(X)) -> c_17(s#(X)) 18: s#(ok(X)) -> c_18(s#(X)) 19: top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) 20: top#(ok(X)) -> c_20(top#(active(X)),active#(X)) ** Step 1.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) - Weak DPs: active#(2nd(cons(X,cons(Y,Z)))) -> c_4() - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:2nd#(mark(X)) -> c_1(2nd#(X)) -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 2:S:2nd#(ok(X)) -> c_2(2nd#(X)) -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 3:S:active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7 -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 4:S:active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7 -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 5:S:active#(from(X)) -> c_6(from#(active(X)),active#(X)) -->_1 from#(ok(X)) -> c_12(from#(X)):11 -->_1 from#(mark(X)) -> c_11(from#(X)):10 -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7 -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6 -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 6:S:active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) -->_3 s#(ok(X)) -> c_18(s#(X)):17 -->_3 s#(mark(X)) -> c_17(s#(X)):16 -->_2 from#(ok(X)) -> c_12(from#(X)):11 -->_2 from#(mark(X)) -> c_11(from#(X)):10 -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 7:S:active#(s(X)) -> c_8(s#(active(X)),active#(X)) -->_1 s#(ok(X)) -> c_18(s#(X)):17 -->_1 s#(mark(X)) -> c_17(s#(X)):16 -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20 -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7 -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 8:S:cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 9:S:cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 10:S:from#(mark(X)) -> c_11(from#(X)) -->_1 from#(ok(X)) -> c_12(from#(X)):11 -->_1 from#(mark(X)) -> c_11(from#(X)):10 11:S:from#(ok(X)) -> c_12(from#(X)) -->_1 from#(ok(X)) -> c_12(from#(X)):11 -->_1 from#(mark(X)) -> c_11(from#(X)):10 12:S:proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 13:S:proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_3 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_3 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_3 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 14:S:proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 -->_1 from#(ok(X)) -> c_12(from#(X)):11 -->_1 from#(mark(X)) -> c_11(from#(X)):10 15:S:proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_18(s#(X)):17 -->_1 s#(mark(X)) -> c_17(s#(X)):16 -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 16:S:s#(mark(X)) -> c_17(s#(X)) -->_1 s#(ok(X)) -> c_18(s#(X)):17 -->_1 s#(mark(X)) -> c_17(s#(X)):16 17:S:s#(ok(X)) -> c_18(s#(X)) -->_1 s#(ok(X)) -> c_18(s#(X)):17 -->_1 s#(mark(X)) -> c_17(s#(X)):16 18:S:top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):19 -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):18 -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):15 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):14 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):13 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):12 19:S:top#(ok(X)) -> c_20(top#(active(X)),active#(X)) -->_2 active#(2nd(cons(X,cons(Y,Z)))) -> c_4():20 -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):19 -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):18 -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):7 -->_2 active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)):6 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 20:W:active#(2nd(cons(X,cons(Y,Z)))) -> c_4() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 20: active#(2nd(cons(X,cons(Y,Z)))) -> c_4() ** Step 1.b:4: UsableRules WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) ** Step 1.b:5: DecomposeDG WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) and a lower component 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) Further, following extension rules are added to the lower component. top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) *** Step 1.b:5.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_20(top#(active(X)),active#(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):2 -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):1 2:S:top#(ok(X)) -> c_20(top#(active(X)),active#(X)) -->_1 top#(ok(X)) -> c_20(top#(active(X)),active#(X)):2 -->_1 top#(mark(X)) -> c_19(top#(proper(X)),proper#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: top#(mark(X)) -> c_19(top#(proper(X))) top#(ok(X)) -> c_20(top#(active(X))) *** Step 1.b:5.a:2: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: top#(mark(X)) -> c_19(top#(proper(X))) top#(ok(X)) -> c_20(top#(active(X))) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(c_19) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = x1 p(active) = 2 + x1 p(cons) = x1 + x2 p(from) = x1 p(mark) = 2 p(ok) = 2 + x1 p(proper) = 0 p(s) = x1 p(top) = 4 p(2nd#) = x1 p(active#) = 0 p(cons#) = 0 p(from#) = 1 + x1 p(proper#) = 1 + x1 p(s#) = 2 + x1 p(top#) = 4 + 4*x1 p(c_1) = x1 p(c_2) = 0 p(c_3) = x1 + x2 p(c_4) = 0 p(c_5) = 0 p(c_6) = 4 + x2 p(c_7) = x3 p(c_8) = 0 p(c_9) = 0 p(c_10) = 2 p(c_11) = 0 p(c_12) = 1 p(c_13) = x2 p(c_14) = 1 p(c_15) = x1 p(c_16) = x2 p(c_17) = 4 + x1 p(c_18) = 4 p(c_19) = 3 + x1 p(c_20) = x1 Following rules are strictly oriented: top#(mark(X)) = 12 > 7 = c_19(top#(proper(X))) Following rules are (at-least) weakly oriented: top#(ok(X)) = 12 + 4*X >= 12 + 4*X = c_20(top#(active(X))) 2nd(mark(X)) = 2 >= 2 = mark(2nd(X)) 2nd(ok(X)) = 2 + X >= 2 + X = ok(2nd(X)) active(2nd(X)) = 2 + X >= 2 + X = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = 2 + X + Y + Z >= 2 = mark(Y) active(cons(X1,X2)) = 2 + X1 + X2 >= 2 + X1 + X2 = cons(active(X1),X2) active(from(X)) = 2 + X >= 2 + X = from(active(X)) active(from(X)) = 2 + X >= 2 = mark(cons(X,from(s(X)))) active(s(X)) = 2 + X >= 2 + X = s(active(X)) cons(mark(X1),X2) = 2 + X2 >= 2 = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = 4 + X1 + X2 >= 2 + X1 + X2 = ok(cons(X1,X2)) from(mark(X)) = 2 >= 2 = mark(from(X)) from(ok(X)) = 2 + X >= 2 + X = ok(from(X)) proper(2nd(X)) = 0 >= 0 = 2nd(proper(X)) proper(cons(X1,X2)) = 0 >= 0 = cons(proper(X1),proper(X2)) proper(from(X)) = 0 >= 0 = from(proper(X)) proper(s(X)) = 0 >= 0 = s(proper(X)) s(mark(X)) = 2 >= 2 = mark(s(X)) s(ok(X)) = 2 + X >= 2 + X = ok(s(X)) *** Step 1.b:5.a:3: NaturalMI WORST_CASE(?,O(1)) + Considered Problem: - Strict DPs: top#(ok(X)) -> c_20(top#(active(X))) - Weak DPs: top#(mark(X)) -> c_19(top#(proper(X))) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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_19) = {1}, uargs(c_20) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1] x1 + [0] p(active) = [0] p(cons) = [1] x1 + [0] p(from) = [6] x1 + [0] p(mark) = [0] p(ok) = [3] p(proper) = [0] p(s) = [3] x1 + [0] p(top) = [0] p(2nd#) = [0] p(active#) = [0] p(cons#) = [0] p(from#) = [0] p(proper#) = [0] p(s#) = [0] p(top#) = [6] x1 + [10] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] p(c_7) = [0] p(c_8) = [0] p(c_9) = [0] p(c_10) = [0] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [0] p(c_18) = [1] p(c_19) = [1] x1 + [0] p(c_20) = [1] x1 + [14] Following rules are strictly oriented: top#(ok(X)) = [28] > [24] = c_20(top#(active(X))) Following rules are (at-least) weakly oriented: top#(mark(X)) = [10] >= [10] = c_19(top#(proper(X))) 2nd(mark(X)) = [0] >= [0] = mark(2nd(X)) 2nd(ok(X)) = [3] >= [3] = ok(2nd(X)) active(2nd(X)) = [0] >= [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0] >= [0] = mark(Y) active(cons(X1,X2)) = [0] >= [0] = cons(active(X1),X2) active(from(X)) = [0] >= [0] = from(active(X)) active(from(X)) = [0] >= [0] = mark(cons(X,from(s(X)))) active(s(X)) = [0] >= [0] = s(active(X)) cons(mark(X1),X2) = [0] >= [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [3] >= [3] = ok(cons(X1,X2)) from(mark(X)) = [0] >= [0] = mark(from(X)) from(ok(X)) = [18] >= [3] = ok(from(X)) proper(2nd(X)) = [0] >= [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] >= [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] >= [0] = from(proper(X)) proper(s(X)) = [0] >= [0] = s(proper(X)) s(mark(X)) = [0] >= [0] = mark(s(X)) s(ok(X)) = [9] >= [3] = ok(s(X)) *** Step 1.b:5.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: top#(mark(X)) -> c_19(top#(proper(X))) top#(ok(X)) -> c_20(top#(active(X))) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/1,c_20/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 1.b:5.b:1: DecomposeDG WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) and a lower component 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) Further, following extension rules are added to the lower component. active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) **** Step 1.b:5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) -> c_6(from#(active(X)),active#(X)) active#(s(X)) -> c_8(s#(active(X)),active#(X)) proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) top#(ok(X)) -> active#(X) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)) -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):4 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):3 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):2 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):1 2:S:active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)) -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):4 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):3 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):2 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):1 3:S:active#(from(X)) -> c_6(from#(active(X)),active#(X)) -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):4 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):3 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):2 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):1 4:S:active#(s(X)) -> c_8(s#(active(X)),active#(X)) -->_2 active#(s(X)) -> c_8(s#(active(X)),active#(X)):4 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):3 -->_2 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):2 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):1 5:S:proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 6:S:proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_3 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_3 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_3 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 7:S:proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 8:S:proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_2 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_2 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_2 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 9:S:top#(ok(X)) -> active#(X) -->_1 active#(s(X)) -> c_8(s#(active(X)),active#(X)):4 -->_1 active#(from(X)) -> c_6(from#(active(X)),active#(X)):3 -->_1 active#(cons(X1,X2)) -> c_5(cons#(active(X1),X2),active#(X1)):2 -->_1 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):1 10:W:top#(mark(X)) -> proper#(X) -->_1 proper#(s(X)) -> c_16(s#(proper(X)),proper#(X)):8 -->_1 proper#(from(X)) -> c_15(from#(proper(X)),proper#(X)):7 -->_1 proper#(cons(X1,X2)) -> c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):6 -->_1 proper#(2nd(X)) -> c_13(2nd#(proper(X)),proper#(X)):5 11:W:top#(mark(X)) -> top#(proper(X)) -->_1 top#(ok(X)) -> top#(active(X)):12 -->_1 top#(mark(X)) -> top#(proper(X)):11 -->_1 top#(mark(X)) -> proper#(X):10 -->_1 top#(ok(X)) -> active#(X):9 12:W:top#(ok(X)) -> top#(active(X)) -->_1 top#(ok(X)) -> top#(active(X)):12 -->_1 top#(mark(X)) -> top#(proper(X)):11 -->_1 top#(mark(X)) -> proper#(X):10 -->_1 top#(ok(X)) -> active#(X):9 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(proper#(X)) proper#(s(X)) -> c_16(proper#(X)) **** Step 1.b:5.b:1.a:2: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(proper#(X)) proper#(s(X)) -> c_16(proper#(X)) top#(ok(X)) -> active#(X) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [4] p(active) = [2] p(cons) = [2] x1 + [4] x2 + [0] p(from) = [0] p(mark) = [0] p(ok) = [0] p(proper) = [0] p(s) = [2] x1 + [0] p(top) = [4] x1 + [2] p(2nd#) = [4] p(active#) = [0] p(cons#) = [4] p(from#) = [4] x1 + [0] p(proper#) = [0] p(s#) = [2] p(top#) = [7] p(c_1) = [1] p(c_2) = [4] x1 + [0] p(c_3) = [4] x1 + [0] p(c_4) = [0] p(c_5) = [1] x1 + [0] p(c_6) = [1] x1 + [0] p(c_7) = [4] x1 + [1] p(c_8) = [2] x1 + [0] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [1] x1 + [1] p(c_12) = [2] x1 + [4] p(c_13) = [1] x1 + [0] p(c_14) = [1] x1 + [1] x2 + [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [0] p(c_17) = [2] p(c_18) = [0] p(c_19) = [1] x2 + [0] p(c_20) = [4] x1 + [1] Following rules are strictly oriented: top#(ok(X)) = [7] > [0] = active#(X) Following rules are (at-least) weakly oriented: active#(2nd(X)) = [0] >= [0] = c_3(active#(X)) active#(cons(X1,X2)) = [0] >= [0] = c_5(active#(X1)) active#(from(X)) = [0] >= [0] = c_6(active#(X)) active#(s(X)) = [0] >= [0] = c_8(active#(X)) proper#(2nd(X)) = [0] >= [0] = c_13(proper#(X)) proper#(cons(X1,X2)) = [0] >= [0] = c_14(proper#(X1),proper#(X2)) proper#(from(X)) = [0] >= [0] = c_15(proper#(X)) proper#(s(X)) = [0] >= [0] = c_16(proper#(X)) top#(mark(X)) = [7] >= [0] = proper#(X) top#(mark(X)) = [7] >= [7] = top#(proper(X)) top#(ok(X)) = [7] >= [7] = top#(active(X)) **** Step 1.b:5.b:1.a:3: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(proper#(X)) proper#(s(X)) -> c_16(proper#(X)) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 2nd :: ["A"(0)] -(1)-> "A"(0) active :: ["A"(0)] -(0)-> "A"(0) cons :: ["A"(0) x "A"(0)] -(0)-> "A"(0) from :: ["A"(0)] -(1)-> "A"(0) mark :: ["A"(0)] -(0)-> "A"(0) ok :: ["A"(0)] -(0)-> "A"(0) proper :: ["A"(0)] -(0)-> "A"(0) s :: ["A"(0)] -(0)-> "A"(0) active# :: ["A"(0)] -(0)-> "A"(0) proper# :: ["A"(0)] -(0)-> "A"(0) top# :: ["A"(0)] -(0)-> "A"(0) c_3 :: ["A"(0)] -(0)-> "A"(0) c_5 :: ["A"(0)] -(0)-> "A"(0) c_6 :: ["A"(0)] -(0)-> "A"(0) c_8 :: ["A"(0)] -(0)-> "A"(0) c_13 :: ["A"(0)] -(0)-> "A"(0) c_14 :: ["A"(0) x "A"(0)] -(0)-> "A"(0) c_15 :: ["A"(0)] -(0)-> "A"(0) c_16 :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: active#(2nd(X)) -> c_3(active#(X)) active#(from(X)) -> c_6(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(from(X)) -> c_15(proper#(X)) 2. Weak: active#(cons(X1,X2)) -> c_5(active#(X1)) active#(s(X)) -> c_8(active#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(s(X)) -> c_16(proper#(X)) **** Step 1.b:5.b:1.a:4: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_5(active#(X1)) active#(s(X)) -> c_8(active#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(s(X)) -> c_16(proper#(X)) - Weak DPs: active#(2nd(X)) -> c_3(active#(X)) active#(from(X)) -> c_6(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(from(X)) -> c_15(proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [2 0] x_1 + [0] [0 2] [2] p(active) = [0 0] x_1 + [0] [0 4] [3] p(cons) = [1 0] x_1 + [0] [0 1] [0] p(from) = [1 0] x_1 + [0] [0 1] [0] p(mark) = [0] [0] p(ok) = [0 2] x_1 + [4] [0 0] [0] p(proper) = [0 0] x_1 + [0] [0 2] [0] p(s) = [2 0] x_1 + [0] [0 2] [1] p(top) = [1] [0] p(2nd#) = [0 0] x_1 + [1] [0 1] [0] p(active#) = [0 1] x_1 + [0] [0 0] [0] p(cons#) = [0 0] x_1 + [0 0] x_2 + [1] [4 2] [0 4] [4] p(from#) = [1] [0] p(proper#) = [0] [0] p(s#) = [1] [0] p(top#) = [2 0] x_1 + [1] [0 0] [5] p(c_1) = [0 0] x_1 + [2] [1 2] [1] p(c_2) = [0] [1] p(c_3) = [1 1] x_1 + [2] [0 0] [0] p(c_4) = [1] [0] p(c_5) = [1 0] x_1 + [0] [0 1] [0] p(c_6) = [1 0] x_1 + [0] [0 0] [0] p(c_7) = [1 0] x_1 + [0 0] x_3 + [1] [0 2] [1 4] [0] p(c_8) = [2 0] x_1 + [0] [0 1] [0] p(c_9) = [0 0] x_1 + [0] [0 2] [4] p(c_10) = [0 1] x_1 + [1] [1 0] [1] p(c_11) = [1 1] x_1 + [0] [2 1] [4] p(c_12) = [0 0] x_1 + [1] [2 4] [0] p(c_13) = [1 0] x_1 + [0] [4 0] [0] p(c_14) = [4 0] x_1 + [4 0] x_2 + [0] [0 0] [1 1] [0] p(c_15) = [1 2] x_1 + [0] [0 1] [0] p(c_16) = [4 0] x_1 + [0] [0 0] [0] p(c_17) = [1] [2] p(c_18) = [0] [0] p(c_19) = [1 1] x_2 + [0] [1 1] [4] p(c_20) = [0 4] x_1 + [1 2] x_2 + [4] [0 0] [1 0] [0] Following rules are strictly oriented: active#(s(X)) = [0 2] X + [1] [0 0] [0] > [0 2] X + [0] [0 0] [0] = c_8(active#(X)) Following rules are (at-least) weakly oriented: active#(2nd(X)) = [0 2] X + [2] [0 0] [0] >= [0 1] X + [2] [0 0] [0] = c_3(active#(X)) active#(cons(X1,X2)) = [0 1] X1 + [0] [0 0] [0] >= [0 1] X1 + [0] [0 0] [0] = c_5(active#(X1)) active#(from(X)) = [0 1] X + [0] [0 0] [0] >= [0 1] X + [0] [0 0] [0] = c_6(active#(X)) proper#(2nd(X)) = [0] [0] >= [0] [0] = c_13(proper#(X)) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = c_14(proper#(X1),proper#(X2)) proper#(from(X)) = [0] [0] >= [0] [0] = c_15(proper#(X)) proper#(s(X)) = [0] [0] >= [0] [0] = c_16(proper#(X)) top#(mark(X)) = [1] [5] >= [0] [0] = proper#(X) top#(mark(X)) = [1] [5] >= [1] [5] = top#(proper(X)) top#(ok(X)) = [0 4] X + [9] [0 0] [5] >= [0 1] X + [0] [0 0] [0] = active#(X) top#(ok(X)) = [0 4] X + [9] [0 0] [5] >= [1] [5] = top#(active(X)) 2nd(mark(X)) = [0] [2] >= [0] [0] = mark(2nd(X)) 2nd(ok(X)) = [0 4] X + [8] [0 0] [2] >= [0 4] X + [8] [0 0] [0] = ok(2nd(X)) active(2nd(X)) = [0 0] X + [0] [0 8] [11] >= [0 0] X + [0] [0 8] [8] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 0] X + [0] [0 8] [11] >= [0] [0] = mark(Y) active(cons(X1,X2)) = [0 0] X1 + [0] [0 4] [3] >= [0 0] X1 + [0] [0 4] [3] = cons(active(X1),X2) active(from(X)) = [0 0] X + [0] [0 4] [3] >= [0 0] X + [0] [0 4] [3] = from(active(X)) active(from(X)) = [0 0] X + [0] [0 4] [3] >= [0] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [0 0] X + [0] [0 8] [7] >= [0 0] X + [0] [0 8] [7] = s(active(X)) cons(mark(X1),X2) = [0] [0] >= [0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 2] X1 + [4] [0 0] [0] >= [0 2] X1 + [4] [0 0] [0] = ok(cons(X1,X2)) from(mark(X)) = [0] [0] >= [0] [0] = mark(from(X)) from(ok(X)) = [0 2] X + [4] [0 0] [0] >= [0 2] X + [4] [0 0] [0] = ok(from(X)) proper(2nd(X)) = [0 0] X + [0] [0 4] [4] >= [0 0] X + [0] [0 4] [2] = 2nd(proper(X)) proper(cons(X1,X2)) = [0 0] X1 + [0] [0 2] [0] >= [0 0] X1 + [0] [0 2] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0 0] X + [0] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = from(proper(X)) proper(s(X)) = [0 0] X + [0] [0 4] [2] >= [0 0] X + [0] [0 4] [1] = s(proper(X)) s(mark(X)) = [0] [1] >= [0] [0] = mark(s(X)) s(ok(X)) = [0 4] X + [8] [0 0] [1] >= [0 4] X + [6] [0 0] [0] = ok(s(X)) **** Step 1.b:5.b:1.a:5: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_5(active#(X1)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(s(X)) -> c_16(proper#(X)) - Weak DPs: active#(2nd(X)) -> c_3(active#(X)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(from(X)) -> c_15(proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(active) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(cons) = [0 0 1] [1 0 0] [0] [0 1 0] x_1 + [0 0 0] x_2 + [1] [0 0 1] [1 0 0] [0] p(from) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(mark) = [0] [0] [0] p(ok) = [1 1 0] [1] [0 0 0] x_1 + [0] [0 1 1] [1] p(proper) = [0 0 0] [0] [0 1 0] x_1 + [0] [0 0 0] [0] p(s) = [0 0 1] [0] [0 1 0] x_1 + [0] [1 0 0] [0] p(top) = [0] [0] [0] p(2nd#) = [0] [0] [0] p(active#) = [0 1 0] [0] [0 1 0] x_1 + [0] [0 0 0] [1] p(cons#) = [0] [0] [0] p(from#) = [0] [0] [0] p(proper#) = [0] [0] [1] p(s#) = [0] [0] [0] p(top#) = [1 0 0] [0] [1 0 0] x_1 + [0] [0 0 0] [1] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(c_4) = [0] [0] [0] p(c_5) = [1 0 0] [0] [0 0 1] x_1 + [0] [0 0 1] [0] p(c_6) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 0] [0] p(c_7) = [0] [0] [0] p(c_8) = [1 0 0] [0] [1 0 0] x_1 + [0] [0 0 0] [1] p(c_9) = [0] [0] [0] p(c_10) = [0] [0] [0] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_14) = [1 0 0] [1 0 0] [0] [0 0 0] x_1 + [0 0 0] x_2 + [0] [0 0 1] [0 0 0] [0] p(c_15) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(c_16) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_17) = [0] [0] [0] p(c_18) = [0] [0] [0] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] Following rules are strictly oriented: active#(cons(X1,X2)) = [0 1 0] [1] [0 1 0] X1 + [1] [0 0 0] [1] > [0 1 0] [0] [0 0 0] X1 + [1] [0 0 0] [1] = c_5(active#(X1)) Following rules are (at-least) weakly oriented: active#(2nd(X)) = [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] = c_3(active#(X)) active#(from(X)) = [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [0] = c_6(active#(X)) active#(s(X)) = [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] = c_8(active#(X)) proper#(2nd(X)) = [0] [0] [1] >= [0] [0] [0] = c_13(proper#(X)) proper#(cons(X1,X2)) = [0] [0] [1] >= [0] [0] [1] = c_14(proper#(X1),proper#(X2)) proper#(from(X)) = [0] [0] [1] >= [0] [0] [1] = c_15(proper#(X)) proper#(s(X)) = [0] [0] [1] >= [0] [0] [0] = c_16(proper#(X)) top#(mark(X)) = [0] [0] [1] >= [0] [0] [1] = proper#(X) top#(mark(X)) = [0] [0] [1] >= [0] [0] [1] = top#(proper(X)) top#(ok(X)) = [1 1 0] [1] [1 1 0] X + [1] [0 0 0] [1] >= [0 1 0] [0] [0 1 0] X + [0] [0 0 0] [1] = active#(X) top#(ok(X)) = [1 1 0] [1] [1 1 0] X + [1] [0 0 0] [1] >= [1 0 0] [0] [1 0 0] X + [0] [0 0 0] [1] = top#(active(X)) 2nd(mark(X)) = [0] [0] [0] >= [0] [0] [0] = mark(2nd(X)) 2nd(ok(X)) = [1 1 0] [1] [0 0 0] X + [0] [0 1 1] [1] >= [1 1 0] [1] [0 0 0] X + [0] [0 1 1] [1] = ok(2nd(X)) active(2nd(X)) = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 0 1] [0 0 1] [1 0 0] [0] [0 1 0] X + [0 0 0] Y + [0 0 0] Z + [1] [0 0 1] [0 0 1] [1 0 0] [0] >= [0] [0] [0] = mark(Y) active(cons(X1,X2)) = [0 0 1] [1 0 0] [0] [0 1 0] X1 + [0 0 0] X2 + [1] [0 0 1] [1 0 0] [0] >= [0 0 1] [1 0 0] [0] [0 1 0] X1 + [0 0 0] X2 + [1] [0 0 1] [1 0 0] [0] = cons(active(X1),X2) active(from(X)) = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = from(active(X)) active(from(X)) = [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] >= [0] [0] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [0 0 1] [0] [0 1 0] X + [0] [1 0 0] [0] >= [0 0 1] [0] [0 1 0] X + [0] [1 0 0] [0] = s(active(X)) cons(mark(X1),X2) = [1 0 0] [0] [0 0 0] X2 + [1] [1 0 0] [0] >= [0] [0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 1 1] [1 1 0] [2] [0 0 0] X1 + [0 0 0] X2 + [1] [0 1 1] [1 1 0] [2] >= [0 1 1] [1 0 0] [2] [0 0 0] X1 + [0 0 0] X2 + [0] [0 1 1] [1 0 0] [2] = ok(cons(X1,X2)) from(mark(X)) = [0] [0] [0] >= [0] [0] [0] = mark(from(X)) from(ok(X)) = [1 1 0] [1] [0 0 0] X + [0] [0 1 1] [1] >= [1 1 0] [1] [0 0 0] X + [0] [0 1 1] [1] = ok(from(X)) proper(2nd(X)) = [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] >= [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0 0 0] [0] [0 1 0] X1 + [1] [0 0 0] [0] >= [0 0 0] [0] [0 1 0] X1 + [1] [0 0 0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] >= [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] = from(proper(X)) proper(s(X)) = [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] >= [0 0 0] [0] [0 1 0] X + [0] [0 0 0] [0] = s(proper(X)) s(mark(X)) = [0] [0] [0] >= [0] [0] [0] = mark(s(X)) s(ok(X)) = [0 1 1] [1] [0 0 0] X + [0] [1 1 0] [1] >= [0 1 1] [1] [0 0 0] X + [0] [1 1 0] [1] = ok(s(X)) **** Step 1.b:5.b:1.a:6: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(s(X)) -> c_16(proper#(X)) - Weak DPs: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(from(X)) -> c_15(proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(active) = [1 0 1] [1] [0 1 0] x_1 + [0] [1 0 1] [1] p(cons) = [1 0 0] [1 0 0] [0] [0 1 0] x_1 + [0 1 0] x_2 + [0] [0 0 1] [0 0 1] [1] p(from) = [0 0 1] [0] [0 1 0] x_1 + [0] [1 0 0] [0] p(mark) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(ok) = [1 0 0] [1] [1 1 1] x_1 + [1] [0 0 1] [1] p(proper) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(s) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(top) = [0] [0] [0] p(2nd#) = [0] [0] [0] p(active#) = [0 0 0] [0] [0 0 0] x_1 + [1] [0 0 1] [1] p(cons#) = [0] [0] [0] p(from#) = [0] [0] [0] p(proper#) = [1 0 1] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(s#) = [0] [0] [0] p(top#) = [1 1 1] [0] [0 0 0] x_1 + [1] [0 1 0] [1] p(c_1) = [0] [0] [0] p(c_2) = [0] [0] [0] p(c_3) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_4) = [0] [0] [0] p(c_5) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 1 0] [1] p(c_6) = [1 0 0] [0] [0 0 0] x_1 + [1] [0 0 0] [0] p(c_7) = [0] [0] [0] p(c_8) = [1 0 0] [0] [0 0 0] x_1 + [1] [0 0 1] [0] p(c_9) = [0] [0] [0] p(c_10) = [0] [0] [0] p(c_11) = [0] [0] [0] p(c_12) = [0] [0] [0] p(c_13) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_14) = [1 0 0] [1 0 0] [0] [0 0 0] x_1 + [0 0 0] x_2 + [0] [0 0 0] [0 0 0] [1] p(c_15) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(c_16) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(c_17) = [0] [0] [0] p(c_18) = [0] [0] [0] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] Following rules are strictly oriented: proper#(cons(X1,X2)) = [1 0 1] [1 0 1] [1] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 0] [0 0 0] [1] > [1 0 1] [1 0 1] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 0] [0 0 0] [1] = c_14(proper#(X1),proper#(X2)) Following rules are (at-least) weakly oriented: active#(2nd(X)) = [0 0 0] [0] [0 0 0] X + [1] [0 0 1] [1] >= [0] [0] [0] = c_3(active#(X)) active#(cons(X1,X2)) = [0 0 0] [0 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [1] [0 0 1] [0 0 1] [2] >= [0] [1] [2] = c_5(active#(X1)) active#(from(X)) = [0 0 0] [0] [0 0 0] X + [1] [1 0 0] [1] >= [0] [1] [0] = c_6(active#(X)) active#(s(X)) = [0 0 0] [0] [0 0 0] X + [1] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [1] [0 0 1] [1] = c_8(active#(X)) proper#(2nd(X)) = [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [0] = c_13(proper#(X)) proper#(from(X)) = [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] = c_15(proper#(X)) proper#(s(X)) = [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] = c_16(proper#(X)) top#(mark(X)) = [1 0 1] [0] [0 0 0] X + [1] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] X + [0] [0 0 0] [1] = proper#(X) top#(mark(X)) = [1 0 1] [0] [0 0 0] X + [1] [0 0 0] [1] >= [1 0 1] [0] [0 0 0] X + [1] [0 0 0] [1] = top#(proper(X)) top#(ok(X)) = [2 1 2] [3] [0 0 0] X + [1] [1 1 1] [2] >= [0 0 0] [0] [0 0 0] X + [1] [0 0 1] [1] = active#(X) top#(ok(X)) = [2 1 2] [3] [0 0 0] X + [1] [1 1 1] [2] >= [2 1 2] [2] [0 0 0] X + [1] [0 1 0] [1] = top#(active(X)) 2nd(mark(X)) = [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] = mark(2nd(X)) 2nd(ok(X)) = [1 0 0] [1] [1 1 1] X + [1] [0 0 1] [1] >= [1 0 0] [1] [1 1 1] X + [1] [0 0 1] [1] = ok(2nd(X)) active(2nd(X)) = [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] >= [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [1 0 1] [1 0 1] [1 0 1] [3] [0 1 0] X + [0 1 0] Y + [0 1 0] Z + [0] [1 0 1] [1 0 1] [1 0 1] [3] >= [1 0 0] [0] [0 0 0] Y + [0] [0 0 1] [0] = mark(Y) active(cons(X1,X2)) = [1 0 1] [1 0 1] [2] [0 1 0] X1 + [0 1 0] X2 + [0] [1 0 1] [1 0 1] [2] >= [1 0 1] [1 0 0] [1] [0 1 0] X1 + [0 1 0] X2 + [0] [1 0 1] [0 0 1] [2] = cons(active(X1),X2) active(from(X)) = [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] >= [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] = from(active(X)) active(from(X)) = [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] >= [1 0 1] [0] [0 0 0] X + [0] [1 0 1] [1] = mark(cons(X,from(s(X)))) active(s(X)) = [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] >= [1 0 1] [1] [0 1 0] X + [0] [1 0 1] [1] = s(active(X)) cons(mark(X1),X2) = [1 0 0] [1 0 0] [0] [0 0 0] X1 + [0 1 0] X2 + [0] [0 0 1] [0 0 1] [1] >= [1 0 0] [1 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 1] [0 0 1] [1] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [1 0 0] [1 0 0] [2] [1 1 1] X1 + [1 1 1] X2 + [2] [0 0 1] [0 0 1] [3] >= [1 0 0] [1 0 0] [1] [1 1 1] X1 + [1 1 1] X2 + [2] [0 0 1] [0 0 1] [2] = ok(cons(X1,X2)) from(mark(X)) = [0 0 1] [0] [0 0 0] X + [0] [1 0 0] [0] >= [0 0 1] [0] [0 0 0] X + [0] [1 0 0] [0] = mark(from(X)) from(ok(X)) = [0 0 1] [1] [1 1 1] X + [1] [1 0 0] [1] >= [0 0 1] [1] [1 1 1] X + [1] [1 0 0] [1] = ok(from(X)) proper(2nd(X)) = [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [1 0 0] [1 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 1] [0 0 1] [1] >= [1 0 0] [1 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 1] [0 0 1] [1] = cons(proper(X1),proper(X2)) proper(from(X)) = [0 0 1] [0] [0 0 0] X + [0] [1 0 0] [0] >= [0 0 1] [0] [0 0 0] X + [0] [1 0 0] [0] = from(proper(X)) proper(s(X)) = [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] = s(proper(X)) s(mark(X)) = [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] >= [1 0 0] [0] [0 0 0] X + [0] [0 0 1] [0] = mark(s(X)) s(ok(X)) = [1 0 0] [1] [1 1 1] X + [1] [0 0 1] [1] >= [1 0 0] [1] [1 1 1] X + [1] [0 0 1] [1] = ok(s(X)) **** Step 1.b:5.b:1.a:7: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: proper#(s(X)) -> c_16(proper#(X)) - Weak DPs: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton (Just 1), miDimension = 4, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton (Just 1): The following argument positions are considered usable: uargs(c_3) = {1}, uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_8) = {1}, uargs(c_13) = {1}, uargs(c_14) = {1,2}, uargs(c_15) = {1}, uargs(c_16) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 1 1] [0] [0 0 0 1] [0] p(active) = [1 1 0 0] [0] [1 1 0 0] x_1 + [0] [0 0 1 0] [0] [0 0 0 1] [0] p(cons) = [1 1 0 0] [0 0 0 0] [1] [1 1 0 0] x_1 + [0 1 0 0] x_2 + [0] [0 0 1 1] [0 0 0 1] [0] [0 0 1 1] [0 0 1 0] [0] p(from) = [1 1 0 0] [1] [1 1 0 0] x_1 + [0] [0 0 1 1] [0] [0 0 1 1] [0] p(mark) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 0] [0] p(ok) = [0 0 0 0] [0] [0 0 0 0] x_1 + [0] [1 1 1 0] [1] [1 1 0 1] [1] p(proper) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 0] [0] p(s) = [1 0 0 0] [0] [0 1 0 0] x_1 + [1] [0 0 1 1] [0] [0 0 1 1] [0] p(top) = [0] [0] [0] [0] p(2nd#) = [0] [0] [0] [0] p(active#) = [1 0 0 1] [0] [1 0 0 0] x_1 + [0] [0 1 1 0] [0] [1 1 0 0] [1] p(cons#) = [0] [0] [0] [0] p(from#) = [0] [0] [0] [0] p(proper#) = [0 1 0 0] [0] [0 0 0 0] x_1 + [0] [0 1 0 0] [1] [0 0 0 0] [1] p(s#) = [0] [0] [0] [0] p(top#) = [0 1 0 1] [0] [0 0 1 1] x_1 + [0] [0 1 1 1] [1] [0 0 1 0] [1] p(c_1) = [0] [0] [0] [0] p(c_2) = [0] [0] [0] [0] p(c_3) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [0] [0 1 0 0] [1] p(c_4) = [0] [0] [0] [0] p(c_5) = [1 0 0 0] [0] [0 0 0 1] x_1 + [0] [1 0 1 0] [0] [0 1 0 1] [1] p(c_6) = [1 0 1 0] [1] [0 0 0 0] x_1 + [1] [1 0 1 0] [0] [0 0 0 1] [1] p(c_7) = [0] [0] [0] [0] p(c_8) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 1 0] [1] [0 0 0 1] [1] p(c_9) = [0] [0] [0] [0] p(c_10) = [0] [0] [0] [0] p(c_11) = [0] [0] [0] [0] p(c_12) = [0] [0] [0] [0] p(c_13) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 1 0] [0] [0 0 0 0] [1] p(c_14) = [1 0 0 0] [1 0 0 0] [0] [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0] [0 0 0 1] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [1] p(c_15) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 1 0] [0] [0 0 0 0] [1] p(c_16) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 0] [1] p(c_17) = [0] [0] [0] [0] p(c_18) = [0] [0] [0] [0] p(c_19) = [0] [0] [0] [0] p(c_20) = [0] [0] [0] [0] Following rules are strictly oriented: proper#(s(X)) = [0 1 0 0] [1] [0 0 0 0] X + [0] [0 1 0 0] [2] [0 0 0 0] [1] > [0 1 0 0] [0] [0 0 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [1] = c_16(proper#(X)) Following rules are (at-least) weakly oriented: active#(2nd(X)) = [1 0 0 1] [0] [1 0 0 0] X + [0] [0 1 1 1] [0] [1 1 0 0] [1] >= [1 0 0 1] [0] [1 0 0 0] X + [0] [0 0 0 0] [0] [1 0 0 0] [1] = c_3(active#(X)) active#(cons(X1,X2)) = [1 1 1 1] [0 0 1 0] [1] [1 1 0 0] X1 + [0 0 0 0] X2 + [1] [1 1 1 1] [0 1 0 1] [0] [2 2 0 0] [0 1 0 0] [2] >= [1 0 0 1] [0] [1 1 0 0] X1 + [1] [1 1 1 1] [0] [2 1 0 0] [2] = c_5(active#(X1)) active#(from(X)) = [1 1 1 1] [1] [1 1 0 0] X + [1] [1 1 1 1] [0] [2 2 0 0] [2] >= [1 1 1 1] [1] [0 0 0 0] X + [1] [1 1 1 1] [0] [1 1 0 0] [2] = c_6(active#(X)) active#(s(X)) = [1 0 1 1] [0] [1 0 0 0] X + [0] [0 1 1 1] [1] [1 1 0 0] [2] >= [1 0 0 1] [0] [1 0 0 0] X + [0] [0 1 1 0] [1] [1 1 0 0] [2] = c_8(active#(X)) proper#(2nd(X)) = [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] >= [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] = c_13(proper#(X)) proper#(cons(X1,X2)) = [1 1 0 0] [0 1 0 0] [0] [0 0 0 0] X1 + [0 0 0 0] X2 + [0] [1 1 0 0] [0 1 0 0] [1] [0 0 0 0] [0 0 0 0] [1] >= [0 1 0 0] [0 1 0 0] [0] [0 0 0 0] X1 + [0 0 0 0] X2 + [0] [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] [0 0 0 0] [1] = c_14(proper#(X1),proper#(X2)) proper#(from(X)) = [1 1 0 0] [0] [0 0 0 0] X + [0] [1 1 0 0] [1] [0 0 0 0] [1] >= [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] = c_15(proper#(X)) top#(mark(X)) = [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] >= [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] = proper#(X) top#(mark(X)) = [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] >= [0 1 0 0] [0] [0 0 0 0] X + [0] [0 1 0 0] [1] [0 0 0 0] [1] = top#(proper(X)) top#(ok(X)) = [1 1 0 1] [1] [2 2 1 1] X + [2] [2 2 1 1] [3] [1 1 1 0] [2] >= [1 0 0 1] [0] [1 0 0 0] X + [0] [0 1 1 0] [0] [1 1 0 0] [1] = active#(X) top#(ok(X)) = [1 1 0 1] [1] [2 2 1 1] X + [2] [2 2 1 1] [3] [1 1 1 0] [2] >= [1 1 0 1] [0] [0 0 1 1] X + [0] [1 1 1 1] [1] [0 0 1 0] [1] = top#(active(X)) 2nd(mark(X)) = [1 0 0 0] [0] [0 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 0 0 0] [0] [0 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] = mark(2nd(X)) 2nd(ok(X)) = [0 0 0 0] [0] [0 0 0 0] X + [0] [2 2 1 1] [2] [1 1 0 1] [1] >= [0 0 0 0] [0] [0 0 0 0] X + [0] [1 1 1 1] [1] [1 1 0 1] [1] = ok(2nd(X)) active(2nd(X)) = [1 1 0 0] [0] [1 1 0 0] X + [0] [0 0 1 1] [0] [0 0 0 1] [0] >= [1 1 0 0] [0] [1 1 0 0] X + [0] [0 0 1 1] [0] [0 0 0 1] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [2 2 0 0] [1 1 0 0] [0 1 0 0] [1] [2 2 0 0] X + [1 1 0 0] Y + [0 1 0 0] Z + [1] [0 0 2 2] [0 0 2 2] [0 0 1 1] [0] [0 0 1 1] [0 0 1 1] [0 0 0 1] [0] >= [1 0 0 0] [0] [0 1 0 0] Y + [0] [0 0 0 0] [0] [0 0 0 0] [0] = mark(Y) active(cons(X1,X2)) = [2 2 0 0] [0 1 0 0] [1] [2 2 0 0] X1 + [0 1 0 0] X2 + [1] [0 0 1 1] [0 0 0 1] [0] [0 0 1 1] [0 0 1 0] [0] >= [2 2 0 0] [0 0 0 0] [1] [2 2 0 0] X1 + [0 1 0 0] X2 + [0] [0 0 1 1] [0 0 0 1] [0] [0 0 1 1] [0 0 1 0] [0] = cons(active(X1),X2) active(from(X)) = [2 2 0 0] [1] [2 2 0 0] X + [1] [0 0 1 1] [0] [0 0 1 1] [0] >= [2 2 0 0] [1] [2 2 0 0] X + [0] [0 0 1 1] [0] [0 0 1 1] [0] = from(active(X)) active(from(X)) = [2 2 0 0] [1] [2 2 0 0] X + [1] [0 0 1 1] [0] [0 0 1 1] [0] >= [1 1 0 0] [1] [2 2 0 0] X + [1] [0 0 0 0] [0] [0 0 0 0] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [1 1 0 0] [1] [1 1 0 0] X + [1] [0 0 1 1] [0] [0 0 1 1] [0] >= [1 1 0 0] [0] [1 1 0 0] X + [1] [0 0 1 1] [0] [0 0 1 1] [0] = s(active(X)) cons(mark(X1),X2) = [1 1 0 0] [0 0 0 0] [1] [1 1 0 0] X1 + [0 1 0 0] X2 + [0] [0 0 0 0] [0 0 0 1] [0] [0 0 0 0] [0 0 1 0] [0] >= [1 1 0 0] [0 0 0 0] [1] [1 1 0 0] X1 + [0 1 0 0] X2 + [0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 0 0 0] [0 0 0 0] [1] [0 0 0 0] X1 + [0 0 0 0] X2 + [0] [2 2 1 1] [1 1 0 1] [3] [2 2 1 1] [1 1 1 0] [3] >= [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] X1 + [0 0 0 0] X2 + [0] [2 2 1 1] [0 1 0 1] [2] [2 2 1 1] [0 1 1 0] [2] = ok(cons(X1,X2)) from(mark(X)) = [1 1 0 0] [1] [1 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 1 0 0] [1] [1 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] = mark(from(X)) from(ok(X)) = [0 0 0 0] [1] [0 0 0 0] X + [0] [2 2 1 1] [2] [2 2 1 1] [2] >= [0 0 0 0] [0] [0 0 0 0] X + [0] [2 2 1 1] [2] [2 2 1 1] [2] = ok(from(X)) proper(2nd(X)) = [1 0 0 0] [0] [0 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 0 0 0] [0] [0 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [1 1 0 0] [0 0 0 0] [1] [1 1 0 0] X1 + [0 1 0 0] X2 + [0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] >= [1 1 0 0] [0 0 0 0] [1] [1 1 0 0] X1 + [0 1 0 0] X2 + [0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] [0 0 0 0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [1 1 0 0] [1] [1 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 1 0 0] [1] [1 1 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [0] = from(proper(X)) proper(s(X)) = [1 0 0 0] [0] [0 1 0 0] X + [1] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 0 0 0] [0] [0 1 0 0] X + [1] [0 0 0 0] [0] [0 0 0 0] [0] = s(proper(X)) s(mark(X)) = [1 0 0 0] [0] [0 1 0 0] X + [1] [0 0 0 0] [0] [0 0 0 0] [0] >= [1 0 0 0] [0] [0 1 0 0] X + [1] [0 0 0 0] [0] [0 0 0 0] [0] = mark(s(X)) s(ok(X)) = [0 0 0 0] [0] [0 0 0 0] X + [1] [2 2 1 1] [2] [2 2 1 1] [2] >= [0 0 0 0] [0] [0 0 0 0] X + [0] [1 1 1 1] [2] [1 1 1 1] [2] = ok(s(X)) **** Step 1.b:5.b:1.a:8: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: active#(2nd(X)) -> c_3(active#(X)) active#(cons(X1,X2)) -> c_5(active#(X1)) active#(from(X)) -> c_6(active#(X)) active#(s(X)) -> c_8(active#(X)) proper#(2nd(X)) -> c_13(proper#(X)) proper#(cons(X1,X2)) -> c_14(proper#(X1),proper#(X2)) proper#(from(X)) -> c_15(proper#(X)) proper#(s(X)) -> c_16(proper#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/1,c_4/0,c_5/1,c_6/1,c_7/3,c_8/1,c_9/1,c_10/1,c_11/1,c_12/1,c_13/1 ,c_14/2,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). **** Step 1.b:5.b:1.b:1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [0] p(active) = [0] p(cons) = [4] x1 + [6] p(from) = [0] p(mark) = [0] p(ok) = [0] p(proper) = [1] p(s) = [4] p(top) = [1] p(2nd#) = [0] p(active#) = [6] p(cons#) = [0] p(from#) = [0] p(proper#) = [0] p(s#) = [0] p(top#) = [6] p(c_1) = [2] x1 + [0] p(c_2) = [4] x1 + [0] p(c_3) = [1] x2 + [1] p(c_4) = [2] p(c_5) = [2] x2 + [2] p(c_6) = [2] x2 + [0] p(c_7) = [1] x1 + [1] x2 + [1] x3 + [2] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [0] p(c_11) = [2] x1 + [0] p(c_12) = [4] x1 + [0] p(c_13) = [1] x2 + [2] p(c_14) = [4] x1 + [1] x2 + [1] x3 + [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [1] p(c_17) = [4] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [1] x2 + [0] Following rules are strictly oriented: active#(from(X)) = [6] > [2] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] >= [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] >= [0] = c_2(2nd#(X)) active#(2nd(X)) = [6] >= [0] = 2nd#(active(X)) active#(2nd(X)) = [6] >= [6] = active#(X) active#(cons(X1,X2)) = [6] >= [6] = active#(X1) active#(cons(X1,X2)) = [6] >= [0] = cons#(active(X1),X2) active#(from(X)) = [6] >= [6] = active#(X) active#(from(X)) = [6] >= [0] = from#(active(X)) active#(s(X)) = [6] >= [6] = active#(X) active#(s(X)) = [6] >= [0] = s#(active(X)) cons#(mark(X1),X2) = [0] >= [0] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] >= [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [0] >= [0] = c_11(from#(X)) from#(ok(X)) = [0] >= [0] = c_12(from#(X)) proper#(2nd(X)) = [0] >= [0] = 2nd#(proper(X)) proper#(2nd(X)) = [0] >= [0] = proper#(X) proper#(cons(X1,X2)) = [0] >= [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] >= [0] = proper#(X1) proper#(cons(X1,X2)) = [0] >= [0] = proper#(X2) proper#(from(X)) = [0] >= [0] = from#(proper(X)) proper#(from(X)) = [0] >= [0] = proper#(X) proper#(s(X)) = [0] >= [0] = proper#(X) proper#(s(X)) = [0] >= [0] = s#(proper(X)) s#(mark(X)) = [0] >= [0] = c_17(s#(X)) s#(ok(X)) = [0] >= [0] = c_18(s#(X)) top#(mark(X)) = [6] >= [0] = proper#(X) top#(mark(X)) = [6] >= [6] = top#(proper(X)) top#(ok(X)) = [6] >= [6] = active#(X) top#(ok(X)) = [6] >= [6] = top#(active(X)) **** Step 1.b:5.b:1.b:2: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + 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}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [3] x1 + [0] p(active) = [1] x1 + [0] p(cons) = [2] x1 + [2] x2 + [0] p(from) = [2] x1 + [0] p(mark) = [0] p(ok) = [1] x1 + [2] p(proper) = [0] p(s) = [1] x1 + [0] p(top) = [1] x1 + [2] p(2nd#) = [0] p(active#) = [4] x1 + [4] p(cons#) = [4] x2 + [0] p(from#) = [0] p(proper#) = [0] p(s#) = [0] p(top#) = [4] x1 + [0] p(c_1) = [2] x1 + [0] p(c_2) = [4] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [4] p(c_4) = [2] p(c_5) = [2] x2 + [4] p(c_6) = [1] x2 + [1] p(c_7) = [1] x1 + [1] x2 + [1] x3 + [1] p(c_8) = [1] x1 + [4] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [6] p(c_11) = [2] x1 + [0] p(c_12) = [4] x1 + [0] p(c_13) = [1] x2 + [0] p(c_14) = [1] x1 + [1] x3 + [1] p(c_15) = [2] x1 + [0] p(c_16) = [4] x1 + [1] p(c_17) = [2] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [1] x2 + [0] Following rules are strictly oriented: cons#(ok(X1),ok(X2)) = [4] X2 + [8] > [4] X2 + [6] = c_10(cons#(X1,X2)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] >= [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] >= [0] = c_2(2nd#(X)) active#(2nd(X)) = [12] X + [4] >= [0] = 2nd#(active(X)) active#(2nd(X)) = [12] X + [4] >= [4] X + [4] = active#(X) active#(cons(X1,X2)) = [8] X1 + [8] X2 + [4] >= [4] X1 + [4] = active#(X1) active#(cons(X1,X2)) = [8] X1 + [8] X2 + [4] >= [4] X2 + [0] = cons#(active(X1),X2) active#(from(X)) = [8] X + [4] >= [4] X + [4] = active#(X) active#(from(X)) = [8] X + [4] >= [0] = from#(active(X)) active#(from(X)) = [8] X + [4] >= [8] X + [1] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [4] X + [4] >= [4] X + [4] = active#(X) active#(s(X)) = [4] X + [4] >= [0] = s#(active(X)) cons#(mark(X1),X2) = [4] X2 + [0] >= [4] X2 + [0] = c_9(cons#(X1,X2)) from#(mark(X)) = [0] >= [0] = c_11(from#(X)) from#(ok(X)) = [0] >= [0] = c_12(from#(X)) proper#(2nd(X)) = [0] >= [0] = 2nd#(proper(X)) proper#(2nd(X)) = [0] >= [0] = proper#(X) proper#(cons(X1,X2)) = [0] >= [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] >= [0] = proper#(X1) proper#(cons(X1,X2)) = [0] >= [0] = proper#(X2) proper#(from(X)) = [0] >= [0] = from#(proper(X)) proper#(from(X)) = [0] >= [0] = proper#(X) proper#(s(X)) = [0] >= [0] = proper#(X) proper#(s(X)) = [0] >= [0] = s#(proper(X)) s#(mark(X)) = [0] >= [0] = c_17(s#(X)) s#(ok(X)) = [0] >= [0] = c_18(s#(X)) top#(mark(X)) = [0] >= [0] = proper#(X) top#(mark(X)) = [0] >= [0] = top#(proper(X)) top#(ok(X)) = [4] X + [8] >= [4] X + [4] = active#(X) top#(ok(X)) = [4] X + [8] >= [4] X + [0] = top#(active(X)) 2nd(mark(X)) = [0] >= [0] = mark(2nd(X)) 2nd(ok(X)) = [3] X + [6] >= [3] X + [2] = ok(2nd(X)) active(2nd(X)) = [3] X + [0] >= [3] X + [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [6] X + [12] Y + [12] Z + [0] >= [0] = mark(Y) active(cons(X1,X2)) = [2] X1 + [2] X2 + [0] >= [2] X1 + [2] X2 + [0] = cons(active(X1),X2) active(from(X)) = [2] X + [0] >= [2] X + [0] = from(active(X)) active(from(X)) = [2] X + [0] >= [0] = mark(cons(X,from(s(X)))) active(s(X)) = [1] X + [0] >= [1] X + [0] = s(active(X)) cons(mark(X1),X2) = [2] X2 + [0] >= [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [2] X1 + [2] X2 + [8] >= [2] X1 + [2] X2 + [2] = ok(cons(X1,X2)) from(mark(X)) = [0] >= [0] = mark(from(X)) from(ok(X)) = [2] X + [4] >= [2] X + [2] = ok(from(X)) proper(2nd(X)) = [0] >= [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] >= [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] >= [0] = from(proper(X)) proper(s(X)) = [0] >= [0] = s(proper(X)) s(mark(X)) = [0] >= [0] = mark(s(X)) s(ok(X)) = [1] X + [2] >= [1] X + [2] = ok(s(X)) **** Step 1.b:5.b:1.b:3: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [0 0] x_1 + [0] [0 1] [0] p(active) = [1 0] x_1 + [0] [0 1] [0] p(cons) = [0 2] x_1 + [0 0] x_2 + [0] [0 1] [2 0] [0] p(from) = [0 0] x_1 + [0] [0 3] [0] p(mark) = [0 0] x_1 + [0] [0 1] [0] p(ok) = [1 0] x_1 + [0] [0 1] [2] p(proper) = [0] [0] p(s) = [0 0] x_1 + [0] [0 1] [0] p(top) = [0] [0] p(2nd#) = [0] [0] p(active#) = [0 1] x_1 + [3] [0 2] [0] p(cons#) = [0 0] x_2 + [0] [3 0] [0] p(from#) = [0 1] x_1 + [0] [0 2] [0] p(proper#) = [0] [0] p(s#) = [0 0] x_1 + [0] [0 2] [0] p(top#) = [0 1] x_1 + [1] [2 3] [0] p(c_1) = [1 2] x_1 + [0] [1 0] [0] p(c_2) = [2 0] x_1 + [0] [2 1] [0] p(c_3) = [2 0] x_2 + [1] [2 1] [0] p(c_4) = [0] [2] p(c_5) = [0] [2] p(c_6) = [0 0] x_1 + [2 0] x_2 + [0] [0 2] [2 0] [0] p(c_7) = [2 0] x_1 + [1 1] x_2 + [1 0] x_3 + [1] [2 0] [0 0] [0 2] [0] p(c_8) = [0 0] x_1 + [0] [0 1] [1] p(c_9) = [2 0] x_1 + [0] [1 0] [0] p(c_10) = [2 0] x_1 + [0] [0 0] [0] p(c_11) = [1 0] x_1 + [0] [0 0] [0] p(c_12) = [1 0] x_1 + [1] [0 1] [1] p(c_13) = [1 1] x_1 + [0 0] x_2 + [0] [0 1] [1 1] [0] p(c_14) = [0 2] x_3 + [1] [1 1] [0] p(c_15) = [0 2] x_1 + [1] [2 0] [1] p(c_16) = [0 2] x_1 + [0] [1 0] [2] p(c_17) = [1 0] x_1 + [0] [2 1] [0] p(c_18) = [1 0] x_1 + [0] [0 0] [1] p(c_19) = [0 0] x_1 + [1 1] x_2 + [0] [0 1] [0 0] [1] p(c_20) = [2] [0] Following rules are strictly oriented: from#(ok(X)) = [0 1] X + [2] [0 2] [4] > [0 1] X + [1] [0 2] [1] = c_12(from#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] [0] >= [0] [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] [0] >= [0] [0] = c_2(2nd#(X)) active#(2nd(X)) = [0 1] X + [3] [0 2] [0] >= [0] [0] = 2nd#(active(X)) active#(2nd(X)) = [0 1] X + [3] [0 2] [0] >= [0 1] X + [3] [0 2] [0] = active#(X) active#(cons(X1,X2)) = [0 1] X1 + [2 0] X2 + [3] [0 2] [4 0] [0] >= [0 1] X1 + [3] [0 2] [0] = active#(X1) active#(cons(X1,X2)) = [0 1] X1 + [2 0] X2 + [3] [0 2] [4 0] [0] >= [0 0] X2 + [0] [3 0] [0] = cons#(active(X1),X2) active#(from(X)) = [0 3] X + [3] [0 6] [0] >= [0 1] X + [3] [0 2] [0] = active#(X) active#(from(X)) = [0 3] X + [3] [0 6] [0] >= [0 1] X + [0] [0 2] [0] = from#(active(X)) active#(from(X)) = [0 3] X + [3] [0 6] [0] >= [0 3] X + [1] [0 4] [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [0 1] X + [3] [0 2] [0] >= [0 1] X + [3] [0 2] [0] = active#(X) active#(s(X)) = [0 1] X + [3] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = s#(active(X)) cons#(mark(X1),X2) = [0 0] X2 + [0] [3 0] [0] >= [0] [0] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0 0] X2 + [0] [3 0] [0] >= [0] [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [0 1] X + [0] [0 2] [0] >= [0 1] X + [0] [0 0] [0] = c_11(from#(X)) proper#(2nd(X)) = [0] [0] >= [0] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = proper#(X1) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = proper#(X2) proper#(from(X)) = [0] [0] >= [0] [0] = from#(proper(X)) proper#(from(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(s(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(s(X)) = [0] [0] >= [0] [0] = s#(proper(X)) s#(mark(X)) = [0 0] X + [0] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = c_17(s#(X)) s#(ok(X)) = [0 0] X + [0] [0 2] [4] >= [0] [1] = c_18(s#(X)) top#(mark(X)) = [0 1] X + [1] [0 3] [0] >= [0] [0] = proper#(X) top#(mark(X)) = [0 1] X + [1] [0 3] [0] >= [1] [0] = top#(proper(X)) top#(ok(X)) = [0 1] X + [3] [2 3] [6] >= [0 1] X + [3] [0 2] [0] = active#(X) top#(ok(X)) = [0 1] X + [3] [2 3] [6] >= [0 1] X + [1] [2 3] [0] = top#(active(X)) 2nd(mark(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = mark(2nd(X)) 2nd(ok(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = ok(2nd(X)) active(2nd(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 0] X + [0 0] Y + [0] [0 1] [0 4] [0] >= [0 0] Y + [0] [0 1] [0] = mark(Y) active(cons(X1,X2)) = [0 2] X1 + [0 0] X2 + [0] [0 1] [2 0] [0] >= [0 2] X1 + [0 0] X2 + [0] [0 1] [2 0] [0] = cons(active(X1),X2) active(from(X)) = [0 0] X + [0] [0 3] [0] >= [0 0] X + [0] [0 3] [0] = from(active(X)) active(from(X)) = [0 0] X + [0] [0 3] [0] >= [0 0] X + [0] [0 1] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = s(active(X)) cons(mark(X1),X2) = [0 2] X1 + [0 0] X2 + [0] [0 1] [2 0] [0] >= [0 0] X1 + [0 0] X2 + [0] [0 1] [2 0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 2] X1 + [0 0] X2 + [4] [0 1] [2 0] [2] >= [0 2] X1 + [0 0] X2 + [0] [0 1] [2 0] [2] = ok(cons(X1,X2)) from(mark(X)) = [0 0] X + [0] [0 3] [0] >= [0 0] X + [0] [0 3] [0] = mark(from(X)) from(ok(X)) = [0 0] X + [0] [0 3] [6] >= [0 0] X + [0] [0 3] [2] = ok(from(X)) proper(2nd(X)) = [0] [0] >= [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] >= [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] >= [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] >= [0] [0] = s(proper(X)) s(mark(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = mark(s(X)) s(ok(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = ok(s(X)) **** Step 1.b:5.b:1.b:4: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0] x_1 + [0] [0 1] [0] p(active) = [2 2] x_1 + [0] [0 1] [0] p(cons) = [1 0] x_1 + [0 0] x_2 + [0] [0 1] [2 0] [0] p(from) = [3 0] x_1 + [0] [0 3] [0] p(mark) = [1 0] x_1 + [0] [0 0] [0] p(ok) = [1 0] x_1 + [1] [1 1] [2] p(proper) = [0] [0] p(s) = [1 0] x_1 + [0] [0 2] [0] p(top) = [0] [0] p(2nd#) = [1 0] x_1 + [0] [0 0] [0] p(active#) = [2 2] x_1 + [0] [0 1] [1] p(cons#) = [0] [0] p(from#) = [3 0] x_1 + [0] [0 2] [0] p(proper#) = [0] [0] p(s#) = [0] [0] p(top#) = [0 2] x_1 + [0] [0 1] [1] p(c_1) = [1 1] x_1 + [0] [0 1] [0] p(c_2) = [1 0] x_1 + [0] [0 0] [0] p(c_3) = [1 0] x_1 + [0 2] x_2 + [2] [2 2] [0 1] [0] p(c_4) = [2] [2] p(c_5) = [0 1] x_1 + [2 0] x_2 + [0] [0 0] [2 0] [0] p(c_6) = [2 1] x_1 + [0] [2 0] [0] p(c_7) = [2 0] x_1 + [1 0] x_2 + [1 1] x_3 + [0] [0 2] [0 0] [2 0] [0] p(c_8) = [2 0] x_1 + [1 0] x_2 + [1] [1 0] [1 0] [1] p(c_9) = [2 0] x_1 + [0] [0 2] [0] p(c_10) = [2 0] x_1 + [0] [0 1] [0] p(c_11) = [1 0] x_1 + [0] [0 0] [0] p(c_12) = [1 0] x_1 + [3] [0 0] [2] p(c_13) = [1 2] x_1 + [0 0] x_2 + [0] [2 0] [0 2] [2] p(c_14) = [2 1] x_1 + [0 0] x_2 + [2] [1 1] [2 2] [0] p(c_15) = [0] [2] p(c_16) = [0 1] x_1 + [0 0] x_2 + [1] [0 0] [0 1] [2] p(c_17) = [1 0] x_1 + [0] [2 0] [0] p(c_18) = [2 0] x_1 + [0] [0 0] [0] p(c_19) = [2 0] x_2 + [0] [0 2] [0] p(c_20) = [1] [1] Following rules are strictly oriented: 2nd#(ok(X)) = [1 0] X + [1] [0 0] [0] > [1 0] X + [0] [0 0] [0] = c_2(2nd#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [1 0] X + [0] [0 0] [0] >= [1 0] X + [0] [0 0] [0] = c_1(2nd#(X)) active#(2nd(X)) = [2 2] X + [0] [0 1] [1] >= [2 2] X + [0] [0 0] [0] = 2nd#(active(X)) active#(2nd(X)) = [2 2] X + [0] [0 1] [1] >= [2 2] X + [0] [0 1] [1] = active#(X) active#(cons(X1,X2)) = [2 2] X1 + [4 0] X2 + [0] [0 1] [2 0] [1] >= [2 2] X1 + [0] [0 1] [1] = active#(X1) active#(cons(X1,X2)) = [2 2] X1 + [4 0] X2 + [0] [0 1] [2 0] [1] >= [0] [0] = cons#(active(X1),X2) active#(from(X)) = [6 6] X + [0] [0 3] [1] >= [2 2] X + [0] [0 1] [1] = active#(X) active#(from(X)) = [6 6] X + [0] [0 3] [1] >= [6 6] X + [0] [0 2] [0] = from#(active(X)) active#(from(X)) = [6 6] X + [0] [0 3] [1] >= [3 0] X + [0] [0 0] [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [2 4] X + [0] [0 2] [1] >= [2 2] X + [0] [0 1] [1] = active#(X) active#(s(X)) = [2 4] X + [0] [0 2] [1] >= [0] [0] = s#(active(X)) cons#(mark(X1),X2) = [0] [0] >= [0] [0] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] [0] >= [0] [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [3 0] X + [0] [0 0] [0] >= [3 0] X + [0] [0 0] [0] = c_11(from#(X)) from#(ok(X)) = [3 0] X + [3] [2 2] [4] >= [3 0] X + [3] [0 0] [2] = c_12(from#(X)) proper#(2nd(X)) = [0] [0] >= [0] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = proper#(X1) proper#(cons(X1,X2)) = [0] [0] >= [0] [0] = proper#(X2) proper#(from(X)) = [0] [0] >= [0] [0] = from#(proper(X)) proper#(from(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(s(X)) = [0] [0] >= [0] [0] = proper#(X) proper#(s(X)) = [0] [0] >= [0] [0] = s#(proper(X)) s#(mark(X)) = [0] [0] >= [0] [0] = c_17(s#(X)) s#(ok(X)) = [0] [0] >= [0] [0] = c_18(s#(X)) top#(mark(X)) = [0] [1] >= [0] [0] = proper#(X) top#(mark(X)) = [0] [1] >= [0] [1] = top#(proper(X)) top#(ok(X)) = [2 2] X + [4] [1 1] [3] >= [2 2] X + [0] [0 1] [1] = active#(X) top#(ok(X)) = [2 2] X + [4] [1 1] [3] >= [0 2] X + [0] [0 1] [1] = top#(active(X)) 2nd(mark(X)) = [1 0] X + [0] [0 0] [0] >= [1 0] X + [0] [0 0] [0] = mark(2nd(X)) 2nd(ok(X)) = [1 0] X + [1] [1 1] [2] >= [1 0] X + [1] [1 1] [2] = ok(2nd(X)) active(2nd(X)) = [2 2] X + [0] [0 1] [0] >= [2 2] X + [0] [0 1] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [2 2] X + [4 0] Y + [0] [0 1] [2 0] [0] >= [1 0] Y + [0] [0 0] [0] = mark(Y) active(cons(X1,X2)) = [2 2] X1 + [4 0] X2 + [0] [0 1] [2 0] [0] >= [2 2] X1 + [0 0] X2 + [0] [0 1] [2 0] [0] = cons(active(X1),X2) active(from(X)) = [6 6] X + [0] [0 3] [0] >= [6 6] X + [0] [0 3] [0] = from(active(X)) active(from(X)) = [6 6] X + [0] [0 3] [0] >= [1 0] X + [0] [0 0] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [2 4] X + [0] [0 2] [0] >= [2 2] X + [0] [0 2] [0] = s(active(X)) cons(mark(X1),X2) = [1 0] X1 + [0 0] X2 + [0] [0 0] [2 0] [0] >= [1 0] X1 + [0] [0 0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [1 0] X1 + [0 0] X2 + [1] [1 1] [2 0] [4] >= [1 0] X1 + [0 0] X2 + [1] [1 1] [2 0] [2] = ok(cons(X1,X2)) from(mark(X)) = [3 0] X + [0] [0 0] [0] >= [3 0] X + [0] [0 0] [0] = mark(from(X)) from(ok(X)) = [3 0] X + [3] [3 3] [6] >= [3 0] X + [1] [3 3] [2] = ok(from(X)) proper(2nd(X)) = [0] [0] >= [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] >= [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] >= [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] >= [0] [0] = s(proper(X)) s(mark(X)) = [1 0] X + [0] [0 0] [0] >= [1 0] X + [0] [0 0] [0] = mark(s(X)) s(ok(X)) = [1 0] X + [1] [2 2] [4] >= [1 0] X + [1] [1 2] [2] = ok(s(X)) **** Step 1.b:5.b:1.b:5: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) - Weak DPs: 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [0 0] x_1 + [0] [0 1] [0] p(active) = [0 1] x_1 + [0] [0 1] [0] p(cons) = [0 2] x_1 + [0 0] x_2 + [0] [0 2] [2 0] [0] p(from) = [0 0] x_1 + [0] [0 2] [0] p(mark) = [0 0] x_1 + [0] [0 1] [0] p(ok) = [1 0] x_1 + [0] [0 1] [2] p(proper) = [0] [0] p(s) = [1 0] x_1 + [0] [0 1] [0] p(top) = [0 0] x_1 + [0] [2 0] [1] p(2nd#) = [0] [0] p(active#) = [0 2] x_1 + [3] [0 0] [1] p(cons#) = [0] [0] p(from#) = [0] [1] p(proper#) = [0] [1] p(s#) = [0 2] x_1 + [0] [0 0] [0] p(top#) = [0 2] x_1 + [0] [0 0] [1] p(c_1) = [2 0] x_1 + [0] [1 1] [0] p(c_2) = [1 0] x_1 + [0] [0 0] [0] p(c_3) = [1 0] x_1 + [0] [0 0] [0] p(c_4) = [0] [0] p(c_5) = [1] [0] p(c_6) = [1 0] x_2 + [0] [0 1] [0] p(c_7) = [2 0] x_1 + [2 2] x_2 + [2 2] x_3 + [1] [0 1] [0 0] [0 1] [1] p(c_8) = [0 0] x_1 + [0] [0 1] [2] p(c_9) = [2 0] x_1 + [0] [0 2] [0] p(c_10) = [1 2] x_1 + [0] [0 0] [0] p(c_11) = [2 0] x_1 + [0] [1 0] [1] p(c_12) = [2 0] x_1 + [0] [1 1] [0] p(c_13) = [0 2] x_1 + [0] [0 2] [0] p(c_14) = [2 0] x_1 + [0] [1 0] [2] p(c_15) = [1 0] x_1 + [0 1] x_2 + [1] [0 1] [2 1] [0] p(c_16) = [2 0] x_1 + [0] [0 0] [0] p(c_17) = [1 0] x_1 + [0] [0 0] [0] p(c_18) = [1 0] x_1 + [1] [0 0] [0] p(c_19) = [2] [1] p(c_20) = [0 0] x_1 + [1 2] x_2 + [0] [0 2] [0 0] [1] Following rules are strictly oriented: s#(ok(X)) = [0 2] X + [4] [0 0] [0] > [0 2] X + [1] [0 0] [0] = c_18(s#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] [0] >= [0] [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] [0] >= [0] [0] = c_2(2nd#(X)) active#(2nd(X)) = [0 2] X + [3] [0 0] [1] >= [0] [0] = 2nd#(active(X)) active#(2nd(X)) = [0 2] X + [3] [0 0] [1] >= [0 2] X + [3] [0 0] [1] = active#(X) active#(cons(X1,X2)) = [0 4] X1 + [4 0] X2 + [3] [0 0] [0 0] [1] >= [0 2] X1 + [3] [0 0] [1] = active#(X1) active#(cons(X1,X2)) = [0 4] X1 + [4 0] X2 + [3] [0 0] [0 0] [1] >= [0] [0] = cons#(active(X1),X2) active#(from(X)) = [0 4] X + [3] [0 0] [1] >= [0 2] X + [3] [0 0] [1] = active#(X) active#(from(X)) = [0 4] X + [3] [0 0] [1] >= [0] [1] = from#(active(X)) active#(from(X)) = [0 4] X + [3] [0 0] [1] >= [0 4] X + [3] [0 0] [1] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [0 2] X + [3] [0 0] [1] >= [0 2] X + [3] [0 0] [1] = active#(X) active#(s(X)) = [0 2] X + [3] [0 0] [1] >= [0 2] X + [0] [0 0] [0] = s#(active(X)) cons#(mark(X1),X2) = [0] [0] >= [0] [0] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] [0] >= [0] [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [0] [1] >= [0] [1] = c_11(from#(X)) from#(ok(X)) = [0] [1] >= [0] [1] = c_12(from#(X)) proper#(2nd(X)) = [0] [1] >= [0] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [0] [1] >= [0] [1] = proper#(X) proper#(cons(X1,X2)) = [0] [1] >= [0] [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] [1] >= [0] [1] = proper#(X1) proper#(cons(X1,X2)) = [0] [1] >= [0] [1] = proper#(X2) proper#(from(X)) = [0] [1] >= [0] [1] = from#(proper(X)) proper#(from(X)) = [0] [1] >= [0] [1] = proper#(X) proper#(s(X)) = [0] [1] >= [0] [1] = proper#(X) proper#(s(X)) = [0] [1] >= [0] [0] = s#(proper(X)) s#(mark(X)) = [0 2] X + [0] [0 0] [0] >= [0 2] X + [0] [0 0] [0] = c_17(s#(X)) top#(mark(X)) = [0 2] X + [0] [0 0] [1] >= [0] [1] = proper#(X) top#(mark(X)) = [0 2] X + [0] [0 0] [1] >= [0] [1] = top#(proper(X)) top#(ok(X)) = [0 2] X + [4] [0 0] [1] >= [0 2] X + [3] [0 0] [1] = active#(X) top#(ok(X)) = [0 2] X + [4] [0 0] [1] >= [0 2] X + [0] [0 0] [1] = top#(active(X)) 2nd(mark(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = mark(2nd(X)) 2nd(ok(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = ok(2nd(X)) active(2nd(X)) = [0 1] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 2] X + [0 4] Y + [0] [0 2] [0 4] [0] >= [0 0] Y + [0] [0 1] [0] = mark(Y) active(cons(X1,X2)) = [0 2] X1 + [2 0] X2 + [0] [0 2] [2 0] [0] >= [0 2] X1 + [0 0] X2 + [0] [0 2] [2 0] [0] = cons(active(X1),X2) active(from(X)) = [0 2] X + [0] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = from(active(X)) active(from(X)) = [0 2] X + [0] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [0 1] X + [0] [0 1] [0] >= [0 1] X + [0] [0 1] [0] = s(active(X)) cons(mark(X1),X2) = [0 2] X1 + [0 0] X2 + [0] [0 2] [2 0] [0] >= [0 0] X1 + [0 0] X2 + [0] [0 2] [2 0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 2] X1 + [0 0] X2 + [4] [0 2] [2 0] [4] >= [0 2] X1 + [0 0] X2 + [0] [0 2] [2 0] [2] = ok(cons(X1,X2)) from(mark(X)) = [0 0] X + [0] [0 2] [0] >= [0 0] X + [0] [0 2] [0] = mark(from(X)) from(ok(X)) = [0 0] X + [0] [0 2] [4] >= [0 0] X + [0] [0 2] [2] = ok(from(X)) proper(2nd(X)) = [0] [0] >= [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] >= [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] >= [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] >= [0] [0] = s(proper(X)) s(mark(X)) = [0 0] X + [0] [0 1] [0] >= [0 0] X + [0] [0 1] [0] = mark(s(X)) s(ok(X)) = [1 0] X + [0] [0 1] [2] >= [1 0] X + [0] [0 1] [2] = ok(s(X)) **** Step 1.b:5.b:1.b:6: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) s#(mark(X)) -> c_17(s#(X)) - Weak DPs: 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0] x_1 + [0] [0 1] [0] p(active) = [1 0] x_1 + [0] [2 2] [2] p(cons) = [1 0] x_1 + [0 2] x_2 + [0] [0 1] [0 0] [0] p(from) = [2 0] x_1 + [0] [0 1] [0] p(mark) = [0 0] x_1 + [0] [0 1] [2] p(ok) = [1 1] x_1 + [1] [0 1] [0] p(proper) = [0] [0] p(s) = [1 0] x_1 + [0] [0 1] [0] p(top) = [0 0] x_1 + [1] [0 1] [0] p(2nd#) = [0] [0] p(active#) = [2 3] x_1 + [2] [0 0] [3] p(cons#) = [0] [2] p(from#) = [0 1] x_1 + [0] [0 0] [0] p(proper#) = [1] [2] p(s#) = [0] [0] p(top#) = [3 0] x_1 + [1] [0 0] [3] p(c_1) = [2 0] x_1 + [0] [0 0] [0] p(c_2) = [2 0] x_1 + [0] [1 2] [0] p(c_3) = [0 2] x_2 + [1] [0 1] [0] p(c_4) = [0] [2] p(c_5) = [0 0] x_1 + [0] [0 2] [0] p(c_6) = [0 0] x_1 + [0] [0 2] [0] p(c_7) = [1 0] x_1 + [1 0] x_2 + [1 0] x_3 + [0] [0 0] [0 0] [2 2] [3] p(c_8) = [2 2] x_1 + [1] [1 0] [0] p(c_9) = [1 0] x_1 + [0] [2 0] [1] p(c_10) = [1 0] x_1 + [0] [0 0] [1] p(c_11) = [1 0] x_1 + [0] [0 0] [0] p(c_12) = [1 1] x_1 + [0] [0 2] [0] p(c_13) = [1 2] x_2 + [0] [0 2] [0] p(c_14) = [0 1] x_1 + [1 2] x_2 + [0] [2 0] [0 0] [2] p(c_15) = [2 0] x_1 + [1 0] x_2 + [0] [0 2] [0 1] [0] p(c_16) = [0 0] x_1 + [0] [0 2] [2] p(c_17) = [2 0] x_1 + [0] [0 0] [0] p(c_18) = [1 0] x_1 + [0] [0 1] [0] p(c_19) = [0 0] x_2 + [2] [0 2] [0] p(c_20) = [0 0] x_1 + [2 0] x_2 + [1] [0 1] [1 0] [0] Following rules are strictly oriented: from#(mark(X)) = [0 1] X + [2] [0 0] [0] > [0 1] X + [0] [0 0] [0] = c_11(from#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] [0] >= [0] [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] [0] >= [0] [0] = c_2(2nd#(X)) active#(2nd(X)) = [2 3] X + [2] [0 0] [3] >= [0] [0] = 2nd#(active(X)) active#(2nd(X)) = [2 3] X + [2] [0 0] [3] >= [2 3] X + [2] [0 0] [3] = active#(X) active#(cons(X1,X2)) = [2 3] X1 + [0 4] X2 + [2] [0 0] [0 0] [3] >= [2 3] X1 + [2] [0 0] [3] = active#(X1) active#(cons(X1,X2)) = [2 3] X1 + [0 4] X2 + [2] [0 0] [0 0] [3] >= [0] [2] = cons#(active(X1),X2) active#(from(X)) = [4 3] X + [2] [0 0] [3] >= [2 3] X + [2] [0 0] [3] = active#(X) active#(from(X)) = [4 3] X + [2] [0 0] [3] >= [2 2] X + [2] [0 0] [0] = from#(active(X)) active#(from(X)) = [4 3] X + [2] [0 0] [3] >= [0 1] X + [0] [0 0] [3] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [2 3] X + [2] [0 0] [3] >= [2 3] X + [2] [0 0] [3] = active#(X) active#(s(X)) = [2 3] X + [2] [0 0] [3] >= [0] [0] = s#(active(X)) cons#(mark(X1),X2) = [0] [2] >= [0] [1] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] [2] >= [0] [1] = c_10(cons#(X1,X2)) from#(ok(X)) = [0 1] X + [0] [0 0] [0] >= [0 1] X + [0] [0 0] [0] = c_12(from#(X)) proper#(2nd(X)) = [1] [2] >= [0] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [1] [2] >= [1] [2] = proper#(X) proper#(cons(X1,X2)) = [1] [2] >= [0] [2] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [1] [2] >= [1] [2] = proper#(X1) proper#(cons(X1,X2)) = [1] [2] >= [1] [2] = proper#(X2) proper#(from(X)) = [1] [2] >= [0] [0] = from#(proper(X)) proper#(from(X)) = [1] [2] >= [1] [2] = proper#(X) proper#(s(X)) = [1] [2] >= [1] [2] = proper#(X) proper#(s(X)) = [1] [2] >= [0] [0] = s#(proper(X)) s#(mark(X)) = [0] [0] >= [0] [0] = c_17(s#(X)) s#(ok(X)) = [0] [0] >= [0] [0] = c_18(s#(X)) top#(mark(X)) = [1] [3] >= [1] [2] = proper#(X) top#(mark(X)) = [1] [3] >= [1] [3] = top#(proper(X)) top#(ok(X)) = [3 3] X + [4] [0 0] [3] >= [2 3] X + [2] [0 0] [3] = active#(X) top#(ok(X)) = [3 3] X + [4] [0 0] [3] >= [3 0] X + [1] [0 0] [3] = top#(active(X)) 2nd(mark(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = mark(2nd(X)) 2nd(ok(X)) = [1 1] X + [1] [0 1] [0] >= [1 1] X + [1] [0 1] [0] = ok(2nd(X)) active(2nd(X)) = [1 0] X + [0] [2 2] [2] >= [1 0] X + [0] [2 2] [2] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [1 0] X + [0 2] Y + [0] [2 2] [0 4] [2] >= [0 0] Y + [0] [0 1] [2] = mark(Y) active(cons(X1,X2)) = [1 0] X1 + [0 2] X2 + [0] [2 2] [0 4] [2] >= [1 0] X1 + [0 2] X2 + [0] [2 2] [0 0] [2] = cons(active(X1),X2) active(from(X)) = [2 0] X + [0] [4 2] [2] >= [2 0] X + [0] [2 2] [2] = from(active(X)) active(from(X)) = [2 0] X + [0] [4 2] [2] >= [0 0] X + [0] [0 1] [2] = mark(cons(X,from(s(X)))) active(s(X)) = [1 0] X + [0] [2 2] [2] >= [1 0] X + [0] [2 2] [2] = s(active(X)) cons(mark(X1),X2) = [0 0] X1 + [0 2] X2 + [0] [0 1] [0 0] [2] >= [0 0] X1 + [0] [0 1] [2] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [1 1] X1 + [0 2] X2 + [1] [0 1] [0 0] [0] >= [1 1] X1 + [0 2] X2 + [1] [0 1] [0 0] [0] = ok(cons(X1,X2)) from(mark(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = mark(from(X)) from(ok(X)) = [2 2] X + [2] [0 1] [0] >= [2 1] X + [1] [0 1] [0] = ok(from(X)) proper(2nd(X)) = [0] [0] >= [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] >= [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] >= [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] >= [0] [0] = s(proper(X)) s(mark(X)) = [0 0] X + [0] [0 1] [2] >= [0 0] X + [0] [0 1] [2] = mark(s(X)) s(ok(X)) = [1 1] X + [1] [0 1] [0] >= [1 1] X + [1] [0 1] [0] = ok(s(X)) **** Step 1.b:5.b:1.b:7: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) s#(mark(X)) -> c_17(s#(X)) - Weak DPs: 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0] x_1 + [0] [0 0] [0] p(active) = [1 0] x_1 + [1] [0 2] [2] p(cons) = [1 0] x_1 + [0 2] x_2 + [0] [2 0] [0 0] [0] p(from) = [1 0] x_1 + [0] [0 0] [0] p(mark) = [1 0] x_1 + [1] [0 0] [0] p(ok) = [1 0] x_1 + [2] [0 1] [0] p(proper) = [0] [0] p(s) = [1 0] x_1 + [0] [0 0] [0] p(top) = [1 2] x_1 + [2] [2 0] [0] p(2nd#) = [1 0] x_1 + [2] [0 0] [0] p(active#) = [1 0] x_1 + [3] [0 0] [0] p(cons#) = [0] [0] p(from#) = [1 0] x_1 + [2] [0 0] [0] p(proper#) = [2] [1] p(s#) = [0] [0] p(top#) = [1 0] x_1 + [1] [0 0] [2] p(c_1) = [1 2] x_1 + [0] [0 0] [0] p(c_2) = [1 0] x_1 + [1] [0 1] [0] p(c_3) = [2 2] x_2 + [0] [0 0] [0] p(c_4) = [0] [0] p(c_5) = [0 0] x_1 + [1 0] x_2 + [0] [0 1] [0 2] [0] p(c_6) = [0 0] x_1 + [0] [2 1] [1] p(c_7) = [2 0] x_1 + [1 0] x_2 + [1 0] x_3 + [1] [0 0] [0 1] [2 2] [0] p(c_8) = [0 0] x_1 + [0] [0 2] [0] p(c_9) = [1 1] x_1 + [0] [0 0] [0] p(c_10) = [2 0] x_1 + [0] [0 0] [0] p(c_11) = [1 0] x_1 + [1] [0 1] [0] p(c_12) = [1 0] x_1 + [1] [0 0] [0] p(c_13) = [1 0] x_1 + [1 2] x_2 + [0] [0 0] [0 2] [0] p(c_14) = [2 1] x_1 + [0 0] x_3 + [1] [2 2] [0 2] [2] p(c_15) = [0 0] x_2 + [2] [0 2] [1] p(c_16) = [0 0] x_1 + [1] [2 0] [0] p(c_17) = [2 0] x_1 + [0] [0 0] [0] p(c_18) = [2 0] x_1 + [0] [0 2] [0] p(c_19) = [0 0] x_1 + [1 2] x_2 + [0] [1 0] [1 0] [2] p(c_20) = [2 1] x_1 + [2 2] x_2 + [1] [0 0] [1 0] [0] Following rules are strictly oriented: 2nd#(mark(X)) = [1 0] X + [3] [0 0] [0] > [1 0] X + [2] [0 0] [0] = c_1(2nd#(X)) Following rules are (at-least) weakly oriented: 2nd#(ok(X)) = [1 0] X + [4] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = c_2(2nd#(X)) active#(2nd(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = 2nd#(active(X)) active#(2nd(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = active#(X) active#(cons(X1,X2)) = [1 0] X1 + [0 2] X2 + [3] [0 0] [0 0] [0] >= [1 0] X1 + [3] [0 0] [0] = active#(X1) active#(cons(X1,X2)) = [1 0] X1 + [0 2] X2 + [3] [0 0] [0 0] [0] >= [0] [0] = cons#(active(X1),X2) active#(from(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = active#(X) active#(from(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = from#(active(X)) active#(from(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = active#(X) active#(s(X)) = [1 0] X + [3] [0 0] [0] >= [0] [0] = s#(active(X)) cons#(mark(X1),X2) = [0] [0] >= [0] [0] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] [0] >= [0] [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [1 0] X + [3] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = c_11(from#(X)) from#(ok(X)) = [1 0] X + [4] [0 0] [0] >= [1 0] X + [3] [0 0] [0] = c_12(from#(X)) proper#(2nd(X)) = [2] [1] >= [2] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [2] [1] >= [2] [1] = proper#(X) proper#(cons(X1,X2)) = [2] [1] >= [0] [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [2] [1] >= [2] [1] = proper#(X1) proper#(cons(X1,X2)) = [2] [1] >= [2] [1] = proper#(X2) proper#(from(X)) = [2] [1] >= [2] [0] = from#(proper(X)) proper#(from(X)) = [2] [1] >= [2] [1] = proper#(X) proper#(s(X)) = [2] [1] >= [2] [1] = proper#(X) proper#(s(X)) = [2] [1] >= [0] [0] = s#(proper(X)) s#(mark(X)) = [0] [0] >= [0] [0] = c_17(s#(X)) s#(ok(X)) = [0] [0] >= [0] [0] = c_18(s#(X)) top#(mark(X)) = [1 0] X + [2] [0 0] [2] >= [2] [1] = proper#(X) top#(mark(X)) = [1 0] X + [2] [0 0] [2] >= [1] [2] = top#(proper(X)) top#(ok(X)) = [1 0] X + [3] [0 0] [2] >= [1 0] X + [3] [0 0] [0] = active#(X) top#(ok(X)) = [1 0] X + [3] [0 0] [2] >= [1 0] X + [2] [0 0] [2] = top#(active(X)) 2nd(mark(X)) = [1 0] X + [1] [0 0] [0] >= [1 0] X + [1] [0 0] [0] = mark(2nd(X)) 2nd(ok(X)) = [1 0] X + [2] [0 0] [0] >= [1 0] X + [2] [0 0] [0] = ok(2nd(X)) active(2nd(X)) = [1 0] X + [1] [0 0] [2] >= [1 0] X + [1] [0 0] [0] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [1 0] X + [4 0] Y + [1] [0 0] [0 0] [2] >= [1 0] Y + [1] [0 0] [0] = mark(Y) active(cons(X1,X2)) = [1 0] X1 + [0 2] X2 + [1] [4 0] [0 0] [2] >= [1 0] X1 + [0 2] X2 + [1] [2 0] [0 0] [2] = cons(active(X1),X2) active(from(X)) = [1 0] X + [1] [0 0] [2] >= [1 0] X + [1] [0 0] [0] = from(active(X)) active(from(X)) = [1 0] X + [1] [0 0] [2] >= [1 0] X + [1] [0 0] [0] = mark(cons(X,from(s(X)))) active(s(X)) = [1 0] X + [1] [0 0] [2] >= [1 0] X + [1] [0 0] [0] = s(active(X)) cons(mark(X1),X2) = [1 0] X1 + [0 2] X2 + [1] [2 0] [0 0] [2] >= [1 0] X1 + [0 2] X2 + [1] [0 0] [0 0] [0] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [1 0] X1 + [0 2] X2 + [2] [2 0] [0 0] [4] >= [1 0] X1 + [0 2] X2 + [2] [2 0] [0 0] [0] = ok(cons(X1,X2)) from(mark(X)) = [1 0] X + [1] [0 0] [0] >= [1 0] X + [1] [0 0] [0] = mark(from(X)) from(ok(X)) = [1 0] X + [2] [0 0] [0] >= [1 0] X + [2] [0 0] [0] = ok(from(X)) proper(2nd(X)) = [0] [0] >= [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] >= [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] >= [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] >= [0] [0] = s(proper(X)) s(mark(X)) = [1 0] X + [1] [0 0] [0] >= [1 0] X + [1] [0 0] [0] = mark(s(X)) s(ok(X)) = [1 0] X + [2] [0 0] [0] >= [1 0] X + [2] [0 0] [0] = ok(s(X)) **** Step 1.b:5.b:1.b:8: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) s#(mark(X)) -> c_17(s#(X)) - Weak DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [0 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(active) = [1 0 0] [0] [1 0 1] x_1 + [0] [0 0 1] [1] p(cons) = [0 0 0] [0 0 0] [1] [0 0 1] x_1 + [0 0 0] x_2 + [0] [0 0 1] [0 1 0] [0] p(from) = [0 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(mark) = [0 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [1] p(ok) = [0 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [1] p(proper) = [1] [0] [0] p(s) = [0 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(top) = [0] [0] [0] p(2nd#) = [0 0 0] [0] [0 0 1] x_1 + [0] [0 0 0] [0] p(active#) = [0 0 1] [1] [0 0 1] x_1 + [1] [0 0 0] [0] p(cons#) = [0 0 1] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(from#) = [0 0 0] [0] [0 0 1] x_1 + [0] [0 0 0] [0] p(proper#) = [1] [0] [0] p(s#) = [0 0 0] [1] [0 0 1] x_1 + [0] [0 0 0] [0] p(top#) = [0 0 1] [0] [0 0 1] x_1 + [0] [0 0 0] [0] p(c_1) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_2) = [1 0 0] [0] [0 0 0] x_1 + [1] [0 0 0] [0] p(c_3) = [0] [0] [0] p(c_4) = [0] [0] [0] p(c_5) = [0] [0] [0] p(c_6) = [0] [0] [0] p(c_7) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x_1 + [0 0 0] x_2 + [0 1 0] x_3 + [1] [0 0 0] [0 0 0] [0 0 0] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_10) = [1 0 0] [1] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_11) = [1 0 0] [0] [0 0 0] x_1 + [1] [0 0 0] [0] p(c_12) = [1 0 0] [0] [0 0 0] x_1 + [1] [0 0 0] [0] p(c_13) = [0] [0] [0] p(c_14) = [0] [0] [0] p(c_15) = [0] [0] [0] p(c_16) = [0] [0] [0] p(c_17) = [1 0 0] [0] [0 1 0] x_1 + [1] [0 0 0] [0] p(c_18) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 0] [0] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] Following rules are strictly oriented: cons#(mark(X1),X2) = [0 0 1] [1] [0 0 0] X1 + [0] [0 0 0] [0] > [0 0 1] [0] [0 0 0] X1 + [0] [0 0 0] [0] = c_9(cons#(X1,X2)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] >= [0] [0] [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] >= [0] [1] [0] = c_2(2nd#(X)) active#(2nd(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] = 2nd#(active(X)) active#(2nd(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = active#(X) active#(cons(X1,X2)) = [0 0 1] [0 1 0] [1] [0 0 1] X1 + [0 1 0] X2 + [1] [0 0 0] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X1 + [1] [0 0 0] [0] = active#(X1) active#(cons(X1,X2)) = [0 0 1] [0 1 0] [1] [0 0 1] X1 + [0 1 0] X2 + [1] [0 0 0] [0 0 0] [0] >= [0 0 1] [1] [0 0 0] X1 + [0] [0 0 0] [0] = cons#(active(X1),X2) active#(from(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = active#(X) active#(from(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] = from#(active(X)) active#(from(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = active#(X) active#(s(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 0] [1] [0 0 1] X + [1] [0 0 0] [0] = s#(active(X)) cons#(ok(X1),ok(X2)) = [0 0 1] [1] [0 0 0] X1 + [0] [0 0 0] [0] >= [0 0 1] [1] [0 0 0] X1 + [0] [0 0 0] [0] = c_10(cons#(X1,X2)) from#(mark(X)) = [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] >= [0] [1] [0] = c_11(from#(X)) from#(ok(X)) = [0 0 0] [0] [0 0 1] X + [1] [0 0 0] [0] >= [0] [1] [0] = c_12(from#(X)) proper#(2nd(X)) = [1] [0] [0] >= [0] [0] [0] = 2nd#(proper(X)) proper#(2nd(X)) = [1] [0] [0] >= [1] [0] [0] = proper#(X) proper#(cons(X1,X2)) = [1] [0] [0] >= [0] [0] [0] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [1] [0] [0] >= [1] [0] [0] = proper#(X1) proper#(cons(X1,X2)) = [1] [0] [0] >= [1] [0] [0] = proper#(X2) proper#(from(X)) = [1] [0] [0] >= [0] [0] [0] = from#(proper(X)) proper#(from(X)) = [1] [0] [0] >= [1] [0] [0] = proper#(X) proper#(s(X)) = [1] [0] [0] >= [1] [0] [0] = proper#(X) proper#(s(X)) = [1] [0] [0] >= [1] [0] [0] = s#(proper(X)) s#(mark(X)) = [0 0 0] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 0] [1] [0 0 1] X + [1] [0 0 0] [0] = c_17(s#(X)) s#(ok(X)) = [0 0 0] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 0] [1] [0 0 1] X + [0] [0 0 0] [0] = c_18(s#(X)) top#(mark(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [1] [0] [0] = proper#(X) top#(mark(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0] [0] [0] = top#(proper(X)) top#(ok(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = active#(X) top#(ok(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] >= [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [0] = top#(active(X)) 2nd(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(2nd(X)) 2nd(ok(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = ok(2nd(X)) active(2nd(X)) = [0 0 0] [0] [0 0 1] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 0 0] [0 0 0] [0] [0 0 1] X + [0 0 1] Y + [0] [0 0 1] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] Y + [0] [0 0 1] [1] = mark(Y) active(cons(X1,X2)) = [0 0 0] [0 0 0] [1] [0 0 1] X1 + [0 1 0] X2 + [1] [0 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [1] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] = cons(active(X1),X2) active(from(X)) = [0 0 0] [0] [0 0 1] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = from(active(X)) active(from(X)) = [0 0 0] [0] [0 0 1] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(cons(X,from(s(X)))) active(s(X)) = [0 0 0] [0] [0 0 1] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = s(active(X)) cons(mark(X1),X2) = [0 0 0] [0 0 0] [1] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 1] [0 1 0] [1] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 0 0] [0 0 0] [1] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [0] [0 0 1] X1 + [0 0 0] X2 + [0] [0 0 1] [0 1 0] [1] = ok(cons(X1,X2)) from(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(from(X)) from(ok(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = ok(from(X)) proper(2nd(X)) = [1] [0] [0] >= [0] [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [1] [0] [0] >= [1] [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [1] [0] [0] >= [0] [0] [0] = from(proper(X)) proper(s(X)) = [1] [0] [0] >= [0] [0] [0] = s(proper(X)) s(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(s(X)) s(ok(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = ok(s(X)) **** Step 1.b:5.b:1.b:9: MI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: s#(mark(X)) -> c_17(s#(X)) - Weak DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: MI {miKind = Automaton Nothing, miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton Nothing: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_7) = {1,2,3}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: {2nd,active,cons,from,proper,s,2nd#,active#,cons#,from#,proper#,s#,top#} TcT has computed the following interpretation: p(2nd) = [1 0 0] [0] [0 1 0] x_1 + [0] [0 0 1] [0] p(active) = [0 0 0] [0] [1 1 0] x_1 + [1] [0 0 1] [1] p(cons) = [1 0 0] [0 0 0] [0] [1 0 1] x_1 + [0 0 0] x_2 + [0] [0 0 1] [0 1 0] [0] p(from) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(mark) = [0 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [1] p(ok) = [0 0 0] [1] [0 1 0] x_1 + [0] [1 0 1] [1] p(proper) = [0] [0] [0] p(s) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(top) = [0] [0] [0] p(2nd#) = [0 0 0] [0] [1 0 0] x_1 + [0] [0 0 0] [1] p(active#) = [0 0 1] [1] [0 0 0] x_1 + [0] [0 0 0] [1] p(cons#) = [0] [0] [1] p(from#) = [0 0 0] [0] [1 0 0] x_1 + [0] [0 0 0] [1] p(proper#) = [0] [0] [1] p(s#) = [0 0 1] [0] [1 0 0] x_1 + [0] [0 0 0] [1] p(top#) = [1 1 1] [0] [1 0 1] x_1 + [0] [0 0 0] [1] p(c_1) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_2) = [1 0 0] [0] [0 0 1] x_1 + [0] [0 0 0] [0] p(c_3) = [0] [0] [0] p(c_4) = [0] [0] [0] p(c_5) = [0] [0] [0] p(c_6) = [0] [0] [0] p(c_7) = [1 0 0] [1 0 0] [1 0 0] [0] [0 0 0] x_1 + [0 0 0] x_2 + [0 0 0] x_3 + [0] [0 0 0] [0 0 0] [0 0 0] [0] p(c_8) = [0] [0] [0] p(c_9) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(c_10) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(c_11) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [1] p(c_12) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 1] [0] p(c_13) = [0] [0] [0] p(c_14) = [0] [0] [0] p(c_15) = [0] [0] [0] p(c_16) = [0] [0] [0] p(c_17) = [1 0 0] [0] [0 0 0] x_1 + [0] [0 0 0] [0] p(c_18) = [1 1 1] [0] [0 0 0] x_1 + [1] [0 0 0] [1] p(c_19) = [0] [0] [0] p(c_20) = [0] [0] [0] Following rules are strictly oriented: s#(mark(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] > [0 0 1] [0] [0 0 0] X + [0] [0 0 0] [0] = c_17(s#(X)) Following rules are (at-least) weakly oriented: 2nd#(mark(X)) = [0] [0] [1] >= [0] [0] [0] = c_1(2nd#(X)) 2nd#(ok(X)) = [0] [1] [1] >= [0] [1] [0] = c_2(2nd#(X)) active#(2nd(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0] [0] [1] = 2nd#(active(X)) active#(2nd(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] = active#(X) active#(cons(X1,X2)) = [0 0 1] [0 1 0] [1] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 0] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X1 + [0] [0 0 0] [1] = active#(X1) active#(cons(X1,X2)) = [0 0 1] [0 1 0] [1] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 0] [0 0 0] [1] >= [0] [0] [1] = cons#(active(X1),X2) active#(from(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] = active#(X) active#(from(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0] [0] [1] = from#(active(X)) active#(from(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0 0 1] [0] [0 0 0] X + [0] [0 0 0] [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] = active#(X) active#(s(X)) = [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] = s#(active(X)) cons#(mark(X1),X2) = [0] [0] [1] >= [0] [0] [1] = c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) = [0] [0] [1] >= [0] [0] [1] = c_10(cons#(X1,X2)) from#(mark(X)) = [0] [0] [1] >= [0] [0] [1] = c_11(from#(X)) from#(ok(X)) = [0] [1] [1] >= [0] [0] [1] = c_12(from#(X)) proper#(2nd(X)) = [0] [0] [1] >= [0] [0] [1] = 2nd#(proper(X)) proper#(2nd(X)) = [0] [0] [1] >= [0] [0] [1] = proper#(X) proper#(cons(X1,X2)) = [0] [0] [1] >= [0] [0] [1] = cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) = [0] [0] [1] >= [0] [0] [1] = proper#(X1) proper#(cons(X1,X2)) = [0] [0] [1] >= [0] [0] [1] = proper#(X2) proper#(from(X)) = [0] [0] [1] >= [0] [0] [1] = from#(proper(X)) proper#(from(X)) = [0] [0] [1] >= [0] [0] [1] = proper#(X) proper#(s(X)) = [0] [0] [1] >= [0] [0] [1] = proper#(X) proper#(s(X)) = [0] [0] [1] >= [0] [0] [1] = s#(proper(X)) s#(ok(X)) = [1 0 1] [1] [0 0 0] X + [1] [0 0 0] [1] >= [1 0 1] [1] [0 0 0] X + [1] [0 0 0] [1] = c_18(s#(X)) top#(mark(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [1] >= [0] [0] [1] = proper#(X) top#(mark(X)) = [0 0 1] [1] [0 0 1] X + [1] [0 0 0] [1] >= [0] [0] [1] = top#(proper(X)) top#(ok(X)) = [1 1 1] [2] [1 0 1] X + [2] [0 0 0] [1] >= [0 0 1] [1] [0 0 0] X + [0] [0 0 0] [1] = active#(X) top#(ok(X)) = [1 1 1] [2] [1 0 1] X + [2] [0 0 0] [1] >= [1 1 1] [2] [0 0 1] X + [1] [0 0 0] [1] = top#(active(X)) 2nd(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(2nd(X)) 2nd(ok(X)) = [0 0 0] [1] [0 1 0] X + [0] [1 0 1] [1] >= [0 0 0] [1] [0 1 0] X + [0] [1 0 1] [1] = ok(2nd(X)) active(2nd(X)) = [0 0 0] [0] [1 1 0] X + [1] [0 0 1] [1] >= [0 0 0] [0] [1 1 0] X + [1] [0 0 1] [1] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [0 0 0] [0 0 0] [0] [2 0 1] X + [0 0 0] Y + [1] [0 0 1] [1 0 1] [1] >= [0 0 0] [0] [0 0 0] Y + [0] [0 0 1] [1] = mark(Y) active(cons(X1,X2)) = [0 0 0] [0 0 0] [0] [2 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [0] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] = cons(active(X1),X2) active(from(X)) = [0 0 0] [0] [1 0 0] X + [1] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = from(active(X)) active(from(X)) = [0 0 0] [0] [1 0 0] X + [1] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(cons(X,from(s(X)))) active(s(X)) = [0 0 0] [0] [1 0 0] X + [1] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = s(active(X)) cons(mark(X1),X2) = [0 0 0] [0 0 0] [0] [0 0 1] X1 + [0 0 0] X2 + [1] [0 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [0] [0 0 0] X1 + [0 0 0] X2 + [0] [0 0 1] [0 1 0] [1] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [0 0 0] [0 0 0] [1] [1 0 1] X1 + [0 0 0] X2 + [2] [1 0 1] [0 1 0] [1] >= [0 0 0] [0 0 0] [1] [1 0 1] X1 + [0 0 0] X2 + [0] [1 0 1] [0 1 0] [1] = ok(cons(X1,X2)) from(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(from(X)) from(ok(X)) = [0 0 0] [1] [0 0 0] X + [0] [1 0 1] [1] >= [0 0 0] [1] [0 0 0] X + [0] [1 0 1] [1] = ok(from(X)) proper(2nd(X)) = [0] [0] [0] >= [0] [0] [0] = 2nd(proper(X)) proper(cons(X1,X2)) = [0] [0] [0] >= [0] [0] [0] = cons(proper(X1),proper(X2)) proper(from(X)) = [0] [0] [0] >= [0] [0] [0] = from(proper(X)) proper(s(X)) = [0] [0] [0] >= [0] [0] [0] = s(proper(X)) s(mark(X)) = [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] >= [0 0 0] [0] [0 0 0] X + [0] [0 0 1] [1] = mark(s(X)) s(ok(X)) = [0 0 0] [1] [0 0 0] X + [0] [1 0 1] [1] >= [0 0 0] [1] [0 0 0] X + [0] [1 0 1] [1] = ok(s(X)) **** Step 1.b:5.b:1.b:10: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: 2nd#(mark(X)) -> c_1(2nd#(X)) 2nd#(ok(X)) -> c_2(2nd#(X)) active#(2nd(X)) -> 2nd#(active(X)) active#(2nd(X)) -> active#(X) active#(cons(X1,X2)) -> active#(X1) active#(cons(X1,X2)) -> cons#(active(X1),X2) active#(from(X)) -> active#(X) active#(from(X)) -> from#(active(X)) active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) cons#(mark(X1),X2) -> c_9(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)) from#(mark(X)) -> c_11(from#(X)) from#(ok(X)) -> c_12(from#(X)) proper#(2nd(X)) -> 2nd#(proper(X)) proper#(2nd(X)) -> proper#(X) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> proper#(X2) proper#(from(X)) -> from#(proper(X)) proper#(from(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) s#(mark(X)) -> c_17(s#(X)) s#(ok(X)) -> c_18(s#(X)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(from(X)) -> from(active(X)) active(from(X)) -> mark(cons(X,from(s(X)))) active(s(X)) -> s(active(X)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(2nd(X)) -> 2nd(proper(X)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {2nd/1,active/1,cons/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,from#/1,proper#/1,s#/1 ,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/0,c_5/2,c_6/2,c_7/3,c_8/2,c_9/1,c_10/1,c_11/1,c_12/1,c_13/2 ,c_14/3,c_15/2,c_16/2,c_17/1,c_18/1,c_19/2,c_20/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^5))