MAYBE * Step 1: DependencyPairs MAYBE + 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 2: UsableRules MAYBE + 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: 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#(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)) * Step 3: PredecessorEstimation MAYBE + 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)) - 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 4: RemoveWeakSuffixes MAYBE + 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)) - 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 5: NaturalMI MAYBE + 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: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1,2}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2,3}, uargs(c_8) = {1,2}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2,3}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2} 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] x1 + [0] p(active) = [0] p(cons) = [2] x1 + [0] p(from) = [4] x1 + [0] p(mark) = [0] p(ok) = [3] p(proper) = [0] p(s) = [1] x1 + [0] p(top) = [1] x1 + [1] p(2nd#) = [0] p(active#) = [2] p(cons#) = [0] p(from#) = [0] p(proper#) = [0] p(s#) = [0] p(top#) = [5] x1 + [0] p(c_1) = [4] x1 + [0] p(c_2) = [2] x1 + [0] p(c_3) = [1] x1 + [1] x2 + [0] p(c_4) = [2] p(c_5) = [2] x1 + [1] x2 + [0] p(c_6) = [1] x1 + [1] x2 + [0] p(c_7) = [4] x1 + [4] x2 + [1] x3 + [0] p(c_8) = [4] x1 + [1] x2 + [0] p(c_9) = [2] x1 + [0] p(c_10) = [4] x1 + [0] p(c_11) = [4] x1 + [0] p(c_12) = [4] x1 + [0] p(c_13) = [4] x1 + [4] x2 + [0] p(c_14) = [2] x1 + [4] x2 + [1] x3 + [0] p(c_15) = [1] x1 + [2] x2 + [0] p(c_16) = [4] x1 + [2] x2 + [0] p(c_17) = [2] x1 + [0] p(c_18) = [2] x1 + [0] p(c_19) = [1] x1 + [2] x2 + [0] p(c_20) = [4] x1 + [4] x2 + [5] Following rules are strictly oriented: active#(from(X)) = [2] > [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) top#(ok(X)) = [15] > [13] = c_20(top#(active(X)),active#(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)) = [2] >= [2] = c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) = [2] >= [2] = c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) = [2] >= [2] = c_6(from#(active(X)),active#(X)) active#(s(X)) = [2] >= [2] = c_8(s#(active(X)),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] = c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) = [0] >= [0] = c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) = [0] >= [0] = c_15(from#(proper(X)),proper#(X)) proper#(s(X)) = [0] >= [0] = c_16(s#(proper(X)),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] = c_19(top#(proper(X)),proper#(X)) 2nd(mark(X)) = [0] >= [0] = mark(2nd(X)) 2nd(ok(X)) = [6] >= [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)) = [6] >= [3] = ok(cons(X1,X2)) from(mark(X)) = [0] >= [0] = mark(from(X)) from(ok(X)) = [12] >= [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)) = [3] >= [3] = ok(s(X)) * Step 6: NaturalMI MAYBE + 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#(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)) - Weak DPs: active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(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: NaturalMI {miDimension = 1, miDegree = 0, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2}, uargs(c_5) = {1,2}, uargs(c_6) = {1,2}, uargs(c_7) = {1,2,3}, uargs(c_8) = {1,2}, uargs(c_9) = {1}, uargs(c_10) = {1}, uargs(c_11) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1,2}, uargs(c_14) = {1,2,3}, uargs(c_15) = {1,2}, uargs(c_16) = {1,2}, uargs(c_17) = {1}, uargs(c_18) = {1}, uargs(c_19) = {1,2}, uargs(c_20) = {1,2} 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) = [1] p(cons) = [1] x1 + [0] p(from) = [1] x1 + [0] p(mark) = [1] p(ok) = [4] p(proper) = [0] p(s) = [1] x1 + [0] p(top) = [2] x1 + [2] p(2nd#) = [0] p(active#) = [0] p(cons#) = [0] p(from#) = [0] p(proper#) = [0] p(s#) = [0] p(top#) = [2] x1 + [4] p(c_1) = [4] x1 + [0] p(c_2) = [4] x1 + [0] p(c_3) = [2] x1 + [2] x2 + [0] p(c_4) = [0] p(c_5) = [4] x1 + [4] x2 + [0] p(c_6) = [4] x1 + [1] x2 + [0] p(c_7) = [1] x1 + [2] x2 + [1] x3 + [0] p(c_8) = [1] x1 + [1] x2 + [0] p(c_9) = [2] x1 + [0] p(c_10) = [4] x1 + [0] p(c_11) = [4] x1 + [0] p(c_12) = [4] x1 + [0] p(c_13) = [1] x1 + [4] x2 + [0] p(c_14) = [2] x1 + [4] x2 + [2] x3 + [0] p(c_15) = [2] x1 + [1] x2 + [0] p(c_16) = [4] x1 + [1] x2 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [4] x1 + [0] p(c_19) = [1] x1 + [2] x2 + [0] p(c_20) = [2] x1 + [4] x2 + [0] Following rules are strictly oriented: top#(mark(X)) = [6] > [4] = c_19(top#(proper(X)),proper#(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)) = [0] >= [0] = c_3(2nd#(active(X)),active#(X)) active#(cons(X1,X2)) = [0] >= [0] = c_5(cons#(active(X1),X2),active#(X1)) active#(from(X)) = [0] >= [0] = c_6(from#(active(X)),active#(X)) active#(from(X)) = [0] >= [0] = c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) = [0] >= [0] = c_8(s#(active(X)),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] = c_13(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) = [0] >= [0] = c_14(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) = [0] >= [0] = c_15(from#(proper(X)),proper#(X)) proper#(s(X)) = [0] >= [0] = c_16(s#(proper(X)),proper#(X)) s#(mark(X)) = [0] >= [0] = c_17(s#(X)) s#(ok(X)) = [0] >= [0] = c_18(s#(X)) top#(ok(X)) = [12] >= [12] = c_20(top#(active(X)),active#(X)) 2nd(mark(X)) = [1] >= [1] = mark(2nd(X)) 2nd(ok(X)) = [4] >= [4] = ok(2nd(X)) active(2nd(X)) = [1] >= [1] = 2nd(active(X)) active(2nd(cons(X,cons(Y,Z)))) = [1] >= [1] = mark(Y) active(cons(X1,X2)) = [1] >= [1] = cons(active(X1),X2) active(from(X)) = [1] >= [1] = from(active(X)) active(from(X)) = [1] >= [1] = mark(cons(X,from(s(X)))) active(s(X)) = [1] >= [1] = s(active(X)) cons(mark(X1),X2) = [1] >= [1] = mark(cons(X1,X2)) cons(ok(X1),ok(X2)) = [4] >= [4] = ok(cons(X1,X2)) from(mark(X)) = [1] >= [1] = mark(from(X)) from(ok(X)) = [4] >= [4] = 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)) = [1] >= [1] = mark(s(X)) s(ok(X)) = [4] >= [4] = ok(s(X)) * Step 7: Failure MAYBE + 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#(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: active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),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: EmptyProcessor + Details: The problem is still open. MAYBE