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