MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) 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: {active/1,cons/2,first/2,from/1,proper/1,s/1,top/1} / {0/0,mark/1,nil/0,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {active,cons,first,from,proper,s,top} and constructors {0 ,mark,nil,ok} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(0(),X)) -> c_4() active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(0()) -> c_16() proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(nil()) -> c_20() proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(0(),X)) -> c_4() active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(0()) -> c_16() proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(nil()) -> c_20() proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) - Weak TRS: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) 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: {active/1,cons/2,first/2,from/1,proper/1,s/1,top/1,active#/1,cons#/2,first#/2,from#/1,proper#/1,s#/1 ,top#/1} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,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/1,c_14/1,c_15/1,c_16/0,c_17/3,c_18/3,c_19/2,c_20/0,c_21/2,c_22/1,c_23/1,c_24/2,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,first#,from#,proper#,s# ,top#} and constructors {0,mark,nil,ok} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(0(),X)) -> c_4() active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(0()) -> c_16() proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(nil()) -> c_20() proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(0(),X)) -> c_4() active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(0()) -> c_16() proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(nil()) -> c_20() proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) - Weak TRS: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {active/1,cons/2,first/2,from/1,proper/1,s/1,top/1,active#/1,cons#/2,first#/2,from#/1,proper#/1,s#/1 ,top#/1} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,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/1,c_14/1,c_15/1,c_16/0,c_17/3,c_18/3,c_19/2,c_20/0,c_21/2,c_22/1,c_23/1,c_24/2,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,first#,from#,proper#,s# ,top#} and constructors {0,mark,nil,ok} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {4,16,20} by application of Pre({4,16,20}) = {1,2,3,6,8,17,18,19,21,24,25}. Here rules are labelled as follows: 1: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) 2: active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) 3: active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) 4: active#(first(0(),X)) -> c_4() 5: active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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: first#(X1,mark(X2)) -> c_11(first#(X1,X2)) 12: first#(mark(X1),X2) -> c_12(first#(X1,X2)) 13: first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) 14: from#(mark(X)) -> c_14(from#(X)) 15: from#(ok(X)) -> c_15(from#(X)) 16: proper#(0()) -> c_16() 17: proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 18: proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 19: proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) 20: proper#(nil()) -> c_20() 21: proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) 22: s#(mark(X)) -> c_22(s#(X)) 23: s#(ok(X)) -> c_23(s#(X)) 24: top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) 25: top#(ok(X)) -> c_25(top#(active(X)),active#(X)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) - Weak DPs: active#(first(0(),X)) -> c_4() proper#(0()) -> c_16() proper#(nil()) -> c_20() - Weak TRS: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {active/1,cons/2,first/2,from/1,proper/1,s/1,top/1,active#/1,cons#/2,first#/2,from#/1,proper#/1,s#/1 ,top#/1} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,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/1,c_14/1,c_15/1,c_16/0,c_17/3,c_18/3,c_19/2,c_20/0,c_21/2,c_22/1,c_23/1,c_24/2,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,first#,from#,proper#,s# ,top#} and constructors {0,mark,nil,ok} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:active#(cons(X1,X2)) -> c_1(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#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(first(0(),X)) -> c_4():23 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 2:S:active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):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#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(0(),X)) -> c_4():23 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 3:S:active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):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#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(0(),X)) -> c_4():23 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 4:S:active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) -->_2 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_2 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_2 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):10 -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 5:S:active#(from(X)) -> c_6(from#(active(X)),active#(X)) -->_1 from#(ok(X)) -> c_15(from#(X)):14 -->_1 from#(mark(X)) -> c_14(from#(X)):13 -->_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#(first(0(),X)) -> c_4():23 -->_2 active#(from(X)) -> c_6(from#(active(X)),active#(X)):5 -->_2 active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 6:S:active#(from(X)) -> c_7(cons#(X,from(s(X))),from#(s(X)),s#(X)) -->_3 s#(ok(X)) -> c_23(s#(X)):20 -->_3 s#(mark(X)) -> c_22(s#(X)):19 -->_2 from#(ok(X)) -> c_15(from#(X)):14 -->_2 from#(mark(X)) -> c_14(from#(X)):13 -->_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_23(s#(X)):20 -->_1 s#(mark(X)) -> c_22(s#(X)):19 -->_2 active#(first(0(),X)) -> c_4():23 -->_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#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 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:first#(X1,mark(X2)) -> c_11(first#(X1,X2)) -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):10 11:S:first#(mark(X1),X2) -> c_12(first#(X1,X2)) -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):10 12:S:first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):10 13:S:from#(mark(X)) -> c_14(from#(X)) -->_1 from#(ok(X)) -> c_15(from#(X)):14 -->_1 from#(mark(X)) -> c_14(from#(X)):13 14:S:from#(ok(X)) -> c_15(from#(X)) -->_1 from#(ok(X)) -> c_15(from#(X)):14 -->_1 from#(mark(X)) -> c_14(from#(X)):13 15:S:proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_2 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_3 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_2 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_3 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_3 proper#(nil()) -> c_20():25 -->_2 proper#(nil()) -> c_20():25 -->_3 proper#(0()) -> c_16():24 -->_2 proper#(0()) -> c_16():24 -->_3 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 cons#(ok(X1),ok(X2)) -> c_10(cons#(X1,X2)):9 -->_1 cons#(mark(X1),X2) -> c_9(cons#(X1,X2)):8 16:S:proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_2 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_3 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_2 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_3 proper#(nil()) -> c_20():25 -->_2 proper#(nil()) -> c_20():25 -->_3 proper#(0()) -> c_16():24 -->_2 proper#(0()) -> c_16():24 -->_3 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_3 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)):12 -->_1 first#(mark(X1),X2) -> c_12(first#(X1,X2)):11 -->_1 first#(X1,mark(X2)) -> c_11(first#(X1,X2)):10 17:S:proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_2 proper#(nil()) -> c_20():25 -->_2 proper#(0()) -> c_16():24 -->_2 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_2 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_1 from#(ok(X)) -> c_15(from#(X)):14 -->_1 from#(mark(X)) -> c_14(from#(X)):13 18:S:proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_23(s#(X)):20 -->_1 s#(mark(X)) -> c_22(s#(X)):19 -->_2 proper#(nil()) -> c_20():25 -->_2 proper#(0()) -> c_16():24 -->_2 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_2 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_2 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 19:S:s#(mark(X)) -> c_22(s#(X)) -->_1 s#(ok(X)) -> c_23(s#(X)):20 -->_1 s#(mark(X)) -> c_22(s#(X)):19 20:S:s#(ok(X)) -> c_23(s#(X)) -->_1 s#(ok(X)) -> c_23(s#(X)):20 -->_1 s#(mark(X)) -> c_22(s#(X)):19 21:S:top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_25(top#(active(X)),active#(X)):22 -->_2 proper#(nil()) -> c_20():25 -->_2 proper#(0()) -> c_16():24 -->_1 top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)):21 -->_2 proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)):18 -->_2 proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)):17 -->_2 proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):16 -->_2 proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 22:S:top#(ok(X)) -> c_25(top#(active(X)),active#(X)) -->_2 active#(first(0(),X)) -> c_4():23 -->_1 top#(ok(X)) -> c_25(top#(active(X)),active#(X)):22 -->_1 top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)):21 -->_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#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)):4 -->_2 active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)):3 -->_2 active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)):2 -->_2 active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)):1 23:W:active#(first(0(),X)) -> c_4() 24:W:proper#(0()) -> c_16() 25:W:proper#(nil()) -> c_20() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 24: proper#(0()) -> c_16() 25: proper#(nil()) -> c_20() 23: active#(first(0(),X)) -> c_4() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: active#(cons(X1,X2)) -> c_1(cons#(active(X1),X2),active#(X1)) active#(first(X1,X2)) -> c_2(first#(X1,active(X2)),active#(X2)) active#(first(X1,X2)) -> c_3(first#(active(X1),X2),active#(X1)) active#(first(s(X),cons(Y,Z))) -> c_5(cons#(Y,first(X,Z)),first#(X,Z)) 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)) first#(X1,mark(X2)) -> c_11(first#(X1,X2)) first#(mark(X1),X2) -> c_12(first#(X1,X2)) first#(ok(X1),ok(X2)) -> c_13(first#(X1,X2)) from#(mark(X)) -> c_14(from#(X)) from#(ok(X)) -> c_15(from#(X)) proper#(cons(X1,X2)) -> c_17(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(first(X1,X2)) -> c_18(first#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(from(X)) -> c_19(from#(proper(X)),proper#(X)) proper#(s(X)) -> c_21(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_22(s#(X)) s#(ok(X)) -> c_23(s#(X)) top#(mark(X)) -> c_24(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_25(top#(active(X)),active#(X)) - Weak TRS: active(cons(X1,X2)) -> cons(active(X1),X2) active(first(X1,X2)) -> first(X1,active(X2)) active(first(X1,X2)) -> first(active(X1),X2) active(first(0(),X)) -> mark(nil()) active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) 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)) first(X1,mark(X2)) -> mark(first(X1,X2)) first(mark(X1),X2) -> mark(first(X1,X2)) first(ok(X1),ok(X2)) -> ok(first(X1,X2)) from(mark(X)) -> mark(from(X)) from(ok(X)) -> ok(from(X)) proper(0()) -> ok(0()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(first(X1,X2)) -> first(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {active/1,cons/2,first/2,from/1,proper/1,s/1,top/1,active#/1,cons#/2,first#/2,from#/1,proper#/1,s#/1 ,top#/1} / {0/0,mark/1,nil/0,ok/1,c_1/2,c_2/2,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/1,c_14/1,c_15/1,c_16/0,c_17/3,c_18/3,c_19/2,c_20/0,c_21/2,c_22/1,c_23/1,c_24/2,c_25/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,cons#,first#,from#,proper#,s# ,top#} and constructors {0,mark,nil,ok} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE