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,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,cons1/2,from/1,proper/1,s/1,top/1} / {mark/1,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {2nd,active,cons,cons1,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,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(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,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(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,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,cons1/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,cons1#/2,from#/1,proper#/1 ,s#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/2,c_5/0,c_6/2,c_7/2,c_8/2,c_9/2,c_10/3,c_11/2,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/3,c_21/3,c_22/2,c_23/2,c_24/1,c_25/1,c_26/2,c_27/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,cons1#,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,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(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,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(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,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,cons1/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,cons1#/2,from#/1,proper#/1 ,s#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/2,c_5/0,c_6/2,c_7/2,c_8/2,c_9/2,c_10/3,c_11/2,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/3,c_21/3,c_22/2,c_23/2,c_24/1,c_25/1,c_26/2,c_27/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,cons1#,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 {5} by application of Pre({5}) = {3,6,7,8,9,11,27}. 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,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) 5: active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() 6: active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) 7: active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) 8: active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) 9: active#(from(X)) -> c_9(from#(active(X)),active#(X)) 10: active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) 11: active#(s(X)) -> c_11(s#(active(X)),active#(X)) 12: cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) 13: cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) 14: cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) 15: cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) 16: cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) 17: from#(mark(X)) -> c_17(from#(X)) 18: from#(ok(X)) -> c_18(from#(X)) 19: proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) 20: proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 21: proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 22: proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) 23: proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) 24: s#(mark(X)) -> c_24(s#(X)) 25: s#(ok(X)) -> c_25(s#(X)) 26: top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) 27: top#(ok(X)) -> c_27(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#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(top#(active(X)),active#(X)) - Weak DPs: active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() - Weak TRS: 2nd(mark(X)) -> mark(2nd(X)) 2nd(ok(X)) -> ok(2nd(X)) active(2nd(X)) -> 2nd(active(X)) active(2nd(cons(X,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,cons1/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,cons1#/2,from#/1,proper#/1 ,s#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/2,c_5/0,c_6/2,c_7/2,c_8/2,c_9/2,c_10/3,c_11/2,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/3,c_21/3,c_22/2,c_23/2,c_24/1,c_25/1,c_26/2,c_27/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,cons1#,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_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_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#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) -->_2 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_2 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_2 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 5:S:active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):12 -->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):11 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 6:S:active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 7:S:active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 8:S:active#(from(X)) -> c_9(from#(active(X)),active#(X)) -->_1 from#(ok(X)) -> c_18(from#(X)):17 -->_1 from#(mark(X)) -> c_17(from#(X)):16 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 9:S:active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) -->_3 s#(ok(X)) -> c_25(s#(X)):24 -->_3 s#(mark(X)) -> c_24(s#(X)):23 -->_2 from#(ok(X)) -> c_18(from#(X)):17 -->_2 from#(mark(X)) -> c_17(from#(X)):16 -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):12 -->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):11 10:S:active#(s(X)) -> c_11(s#(active(X)),active#(X)) -->_1 s#(ok(X)) -> c_25(s#(X)):24 -->_1 s#(mark(X)) -> c_24(s#(X)):23 -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 11:S:cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):12 -->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):11 12:S:cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):12 -->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):11 13:S:cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 14:S:cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 15:S:cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 16:S:from#(mark(X)) -> c_17(from#(X)) -->_1 from#(ok(X)) -> c_18(from#(X)):17 -->_1 from#(mark(X)) -> c_17(from#(X)):16 17:S:from#(ok(X)) -> c_18(from#(X)) -->_1 from#(ok(X)) -> c_18(from#(X)):17 -->_1 from#(mark(X)) -> c_17(from#(X)):16 18:S:proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_1 2nd#(ok(X)) -> c_2(2nd#(X)):2 -->_1 2nd#(mark(X)) -> c_1(2nd#(X)):1 19:S:proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_3 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_3 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_3 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_3 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_1 cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)):12 -->_1 cons#(mark(X1),X2) -> c_12(cons#(X1,X2)):11 20:S:proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_3 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_3 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_3 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_3 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_1 cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)):15 -->_1 cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)):14 -->_1 cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)):13 21:S:proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 -->_1 from#(ok(X)) -> c_18(from#(X)):17 -->_1 from#(mark(X)) -> c_17(from#(X)):16 22:S:proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_25(s#(X)):24 -->_1 s#(mark(X)) -> c_24(s#(X)):23 -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 23:S:s#(mark(X)) -> c_24(s#(X)) -->_1 s#(ok(X)) -> c_25(s#(X)):24 -->_1 s#(mark(X)) -> c_24(s#(X)):23 24:S:s#(ok(X)) -> c_25(s#(X)) -->_1 s#(ok(X)) -> c_25(s#(X)):24 -->_1 s#(mark(X)) -> c_24(s#(X)):23 25:S:top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_27(top#(active(X)),active#(X)):26 -->_1 top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)):25 -->_2 proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)):22 -->_2 proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)):21 -->_2 proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):20 -->_2 proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):19 -->_2 proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)):18 26:S:top#(ok(X)) -> c_27(top#(active(X)),active#(X)) -->_2 active#(2nd(cons1(X,cons(Y,Z)))) -> c_5():27 -->_1 top#(ok(X)) -> c_27(top#(active(X)),active#(X)):26 -->_1 top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)):25 -->_2 active#(s(X)) -> c_11(s#(active(X)),active#(X)):10 -->_2 active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)):9 -->_2 active#(from(X)) -> c_9(from#(active(X)),active#(X)):8 -->_2 active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)):7 -->_2 active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)):6 -->_2 active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)):5 -->_2 active#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)):4 -->_2 active#(2nd(X)) -> c_3(2nd#(active(X)),active#(X)):3 27:W:active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 27: active#(2nd(cons1(X,cons(Y,Z)))) -> c_5() * Step 5: 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#(2nd(cons(X,X1))) -> c_4(2nd#(cons1(X,X1)),cons1#(X,X1)) active#(cons(X1,X2)) -> c_6(cons#(active(X1),X2),active#(X1)) active#(cons1(X1,X2)) -> c_7(cons1#(X1,active(X2)),active#(X2)) active#(cons1(X1,X2)) -> c_8(cons1#(active(X1),X2),active#(X1)) active#(from(X)) -> c_9(from#(active(X)),active#(X)) active#(from(X)) -> c_10(cons#(X,from(s(X))),from#(s(X)),s#(X)) active#(s(X)) -> c_11(s#(active(X)),active#(X)) cons#(mark(X1),X2) -> c_12(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_13(cons#(X1,X2)) cons1#(X1,mark(X2)) -> c_14(cons1#(X1,X2)) cons1#(mark(X1),X2) -> c_15(cons1#(X1,X2)) cons1#(ok(X1),ok(X2)) -> c_16(cons1#(X1,X2)) from#(mark(X)) -> c_17(from#(X)) from#(ok(X)) -> c_18(from#(X)) proper#(2nd(X)) -> c_19(2nd#(proper(X)),proper#(X)) proper#(cons(X1,X2)) -> c_20(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons1(X1,X2)) -> c_21(cons1#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_22(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_23(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_24(s#(X)) s#(ok(X)) -> c_25(s#(X)) top#(mark(X)) -> c_26(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_27(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,X1))) -> mark(2nd(cons1(X,X1))) active(2nd(cons1(X,cons(Y,Z)))) -> mark(Y) active(cons(X1,X2)) -> cons(active(X1),X2) active(cons1(X1,X2)) -> cons1(X1,active(X2)) active(cons1(X1,X2)) -> cons1(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)) cons1(X1,mark(X2)) -> mark(cons1(X1,X2)) cons1(mark(X1),X2) -> mark(cons1(X1,X2)) cons1(ok(X1),ok(X2)) -> ok(cons1(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(cons1(X1,X2)) -> cons1(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,cons1/2,from/1,proper/1,s/1,top/1,2nd#/1,active#/1,cons#/2,cons1#/2,from#/1,proper#/1 ,s#/1,top#/1} / {mark/1,ok/1,c_1/1,c_2/1,c_3/2,c_4/2,c_5/0,c_6/2,c_7/2,c_8/2,c_9/2,c_10/3,c_11/2,c_12/1 ,c_13/1,c_14/1,c_15/1,c_16/1,c_17/1,c_18/1,c_19/2,c_20/3,c_21/3,c_22/2,c_23/2,c_24/1,c_25/1,c_26/2,c_27/2} - Obligation: innermost runtime complexity wrt. defined symbols {2nd#,active#,cons#,cons1#,from#,proper#,s# ,top#} and constructors {mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE