WORST_CASE(?,O(n^5)) * Step 1: DependencyPairs WORST_CASE(?,O(n^5)) + Considered Problem: - Strict TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,f/3,proper/1,top/1} / {b/0,c/0,mark/1,ok/1} - Obligation: innermost runtime complexity wrt. defined symbols {active,f,proper,top} and constructors {b,c,mark,ok} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs active#(c()) -> c_1() active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(b()) -> c_6() proper#(c()) -> c_7() proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: active#(c()) -> c_1() active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(b()) -> c_6() proper#(c()) -> c_7() proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,3,6,7} by application of Pre({1,3,6,7}) = {2,8,9,10}. Here rules are labelled as follows: 1: active#(c()) -> c_1() 2: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) 3: active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) 4: f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) 5: f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) 6: proper#(b()) -> c_6() 7: proper#(c()) -> c_7() 8: proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) 9: top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) 10: top#(ok(X)) -> c_10(top#(active(X)),active#(X)) * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) - Weak DPs: active#(c()) -> c_1() active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) proper#(b()) -> c_6() proper#(c()) -> c_7() - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) -->_1 f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)):3 -->_1 f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)):2 -->_2 active#(f(b(),X,c())) -> c_3(f#(X,c(),X)):8 -->_2 active#(c()) -> c_1():7 -->_2 active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)):1 2:S:f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) -->_1 f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)):3 -->_1 f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)):2 3:S:f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) -->_1 f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)):3 -->_1 f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)):2 4:S:proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) -->_4 proper#(c()) -> c_7():10 -->_3 proper#(c()) -> c_7():10 -->_2 proper#(c()) -> c_7():10 -->_4 proper#(b()) -> c_6():9 -->_3 proper#(b()) -> c_6():9 -->_2 proper#(b()) -> c_6():9 -->_4 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):4 -->_3 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):4 -->_2 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):4 -->_1 f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)):3 -->_1 f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)):2 5:S:top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_10(top#(active(X)),active#(X)):6 -->_2 proper#(c()) -> c_7():10 -->_2 proper#(b()) -> c_6():9 -->_1 top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)):5 -->_2 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):4 6:S:top#(ok(X)) -> c_10(top#(active(X)),active#(X)) -->_2 active#(f(b(),X,c())) -> c_3(f#(X,c(),X)):8 -->_2 active#(c()) -> c_1():7 -->_1 top#(ok(X)) -> c_10(top#(active(X)),active#(X)):6 -->_1 top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)):5 -->_2 active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)):1 7:W:active#(c()) -> c_1() 8:W:active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) 9:W:proper#(b()) -> c_6() 10:W:proper#(c()) -> c_7() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 9: proper#(b()) -> c_6() 10: proper#(c()) -> c_7() 7: active#(c()) -> c_1() 8: active#(f(b(),X,c())) -> c_3(f#(X,c(),X)) * Step 4: UsableRules WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) * Step 5: DecomposeDG WORST_CASE(?,O(n^5)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) and a lower component active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) Further, following extension rules are added to the lower component. top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) ** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_10(top#(active(X)),active#(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_10(top#(active(X)),active#(X)):2 -->_1 top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)):1 2:S:top#(ok(X)) -> c_10(top#(active(X)),active#(X)) -->_1 top#(ok(X)) -> c_10(top#(active(X)),active#(X)):2 -->_1 top#(mark(X)) -> c_9(top#(proper(X)),proper#(X)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: top#(mark(X)) -> c_9(top#(proper(X))) top#(ok(X)) -> c_10(top#(active(X))) ** Step 5.a:2: MI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: top#(mark(X)) -> c_9(top#(proper(X))) top#(ok(X)) -> c_10(top#(active(X))) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: MI {miKind = Automaton (Just 3), miDimension = 4, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton (Just 3): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [0 0 1 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 1] [0] p(b) = [1] [0] [0] [0] p(c) = [0] [0] [1] [1] p(f) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] x_1 + [0 0 0 0] x_2 + [0 0 0 0] x_3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] p(mark) = [1 0 1 0] [0] [0 0 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 1] [1] p(ok) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 1 0] [0] [0 0 0 1] [0] p(proper) = [1 0 0 0] [0] [0 0 0 1] x_1 + [0] [0 0 1 0] [0] [0 0 0 1] [0] p(top) = [0] [0] [0] [0] p(active#) = [0] [0] [0] [0] p(f#) = [0] [0] [0] [0] p(proper#) = [0] [0] [0] [0] p(top#) = [0 0 0 1] [0] [0 0 0 0] x_1 + [0] [0 0 0 0] [1] [0 0 0 0] [1] p(c_1) = [0] [0] [0] [0] p(c_2) = [0] [0] [0] [0] p(c_3) = [0] [0] [0] [0] p(c_4) = [0] [0] [0] [0] p(c_5) = [0] [0] [0] [0] p(c_6) = [0] [0] [0] [0] p(c_7) = [0] [0] [0] [0] p(c_8) = [0] [0] [0] [0] p(c_9) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 0 0] [1] [0 0 0 0] [1] p(c_10) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 0 1] [0] [0 0 1 0] [0] Following rules are strictly oriented: top#(mark(X)) = [0 0 0 1] [1] [0 0 0 0] X + [0] [0 0 0 0] [1] [0 0 0 0] [1] > [0 0 0 1] [0] [0 0 0 0] X + [0] [0 0 0 0] [1] [0 0 0 0] [1] = c_9(top#(proper(X))) Following rules are (at-least) weakly oriented: top#(ok(X)) = [0 0 0 1] [0] [0 0 0 0] X + [0] [0 0 0 0] [1] [0 0 0 0] [1] >= [0 0 0 1] [0] [0 0 0 0] X + [0] [0 0 0 0] [1] [0 0 0 0] [1] = c_10(top#(active(X))) active(c()) = [1] [0] [0] [1] >= [1] [0] [0] [1] = mark(b()) active(f(X1,X2,X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [0 0 1 1] [0 0 1 1] [0] = f(X1,active(X2),X3) active(f(b(),X,c())) = [0 0 0 0] [0] [0 0 0 0] X + [1] [0 0 0 0] [0] [1 0 1 1] [3] >= [0 0 0 0] [0] [0 0 0 0] X + [0] [0 0 0 0] [0] [1 0 1 1] [3] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [1] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [1] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [0 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] = ok(f(X1,X2,X3)) proper(b()) = [1] [0] [0] [0] >= [1] [0] [0] [0] = ok(b()) proper(c()) = [0] [1] [1] [1] >= [0] [0] [1] [1] = ok(c()) proper(f(X1,X2,X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 0 1 1] X2 + [0 0 1 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 0 0 0] X2 + [0 0 0 0] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 0 1 1] [0 0 1 1] [0] = f(proper(X1),proper(X2),proper(X3)) ** Step 5.a:3: MI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: top#(ok(X)) -> c_10(top#(active(X))) - Weak DPs: top#(mark(X)) -> c_9(top#(proper(X))) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: MI {miKind = Automaton (Just 2), miDimension = 4, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules} + Details: We apply a matrix interpretation of kind Automaton (Just 2): The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [0 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 1] [0] p(b) = [1] [0] [0] [0] p(c) = [0] [1] [0] [1] p(f) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] x_1 + [1 1 0 1] x_2 + [0 1 0 1] x_3 + [0] [0 0 0 0] [0 0 1 0] [0 0 0 0] [0] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] p(mark) = [0 0 0 0] [0] [0 0 0 1] x_1 + [1] [0 0 0 0] [0] [1 1 0 0] [0] p(ok) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 0 0] [1] [0 0 0 1] [0] p(proper) = [1 0 0 0] [0] [0 0 0 1] x_1 + [0] [0 0 0 0] [1] [0 1 0 0] [0] p(top) = [0] [0] [0] [0] p(active#) = [0] [0] [0] [0] p(f#) = [0] [0] [0] [0] p(proper#) = [0] [0] [0] [0] p(top#) = [0 1 1 0] [1] [0 0 0 0] x_1 + [1] [0 1 0 0] [0] [0 0 0 0] [1] p(c_1) = [0] [0] [0] [0] p(c_2) = [0] [0] [0] [0] p(c_3) = [0] [0] [0] [0] p(c_4) = [0] [0] [0] [0] p(c_5) = [0] [0] [0] [0] p(c_6) = [0] [0] [0] [0] p(c_7) = [0] [0] [0] [0] p(c_8) = [0] [0] [0] [0] p(c_9) = [1 0 0 0] [0] [0 0 0 0] x_1 + [0] [0 0 0 0] [0] [0 0 0 0] [1] p(c_10) = [1 0 0 0] [0] [0 1 0 0] x_1 + [0] [0 0 1 0] [0] [0 0 0 0] [0] Following rules are strictly oriented: top#(ok(X)) = [0 1 0 0] [2] [0 0 0 0] X + [1] [0 1 0 0] [0] [0 0 0 0] [1] > [0 1 0 0] [1] [0 0 0 0] X + [1] [0 1 0 0] [0] [0 0 0 0] [0] = c_10(top#(active(X))) Following rules are (at-least) weakly oriented: top#(mark(X)) = [0 0 0 1] [2] [0 0 0 0] X + [1] [0 0 0 1] [1] [0 0 0 0] [1] >= [0 0 0 1] [2] [0 0 0 0] X + [0] [0 0 0 0] [0] [0 0 0 0] [1] = c_9(top#(proper(X))) active(c()) = [0] [1] [0] [1] >= [0] [1] [0] [1] = mark(b()) active(f(X1,X2,X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [0 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [0 1 0 1] [0 1 0 1] [0] = f(X1,active(X2),X3) active(f(b(),X,c())) = [0 0 0 0] [0] [1 1 0 1] X + [3] [0 0 0 0] [0] [1 1 0 1] [3] >= [0 0 0 0] [0] [1 1 0 1] X + [3] [0 0 0 0] [0] [1 1 0 1] [2] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 1 0 1] [0 1 0 1] [1] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [1] [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] = ok(f(X1,X2,X3)) proper(b()) = [1] [0] [1] [0] >= [1] [0] [1] [0] = ok(b()) proper(c()) = [0] [1] [1] [1] >= [0] [1] [1] [1] = ok(c()) proper(f(X1,X2,X3)) = [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] >= [0 0 0 0] [0 0 0 0] [0 0 0 0] [0] [1 0 0 0] X1 + [1 1 0 1] X2 + [0 1 0 1] X3 + [0] [0 0 0 0] [0 0 0 0] [0 0 0 0] [1] [1 0 0 0] [1 1 0 1] [0 1 0 1] [0] = f(proper(X1),proper(X2),proper(X3)) ** Step 5.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: top#(mark(X)) -> c_9(top#(proper(X))) top#(ok(X)) -> c_10(top#(active(X))) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/1,c_10/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 5.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) and a lower component f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) Further, following extension rules are added to the lower component. active#(f(X1,X2,X3)) -> active#(X2) active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) -> proper#(X1) proper#(f(X1,X2,X3)) -> proper#(X2) proper#(f(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) *** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)) -->_2 active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)):1 2:S:proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)),proper#(X1),proper#(X2),proper#(X3)) -->_4 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):2 -->_3 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):2 -->_2 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):2 3:W:top#(mark(X)) -> proper#(X) -->_1 proper#(f(X1,X2,X3)) -> c_8(f#(proper(X1),proper(X2),proper(X3)) ,proper#(X1) ,proper#(X2) ,proper#(X3)):2 4:W:top#(mark(X)) -> top#(proper(X)) -->_1 top#(ok(X)) -> top#(active(X)):6 -->_1 top#(ok(X)) -> active#(X):5 -->_1 top#(mark(X)) -> top#(proper(X)):4 -->_1 top#(mark(X)) -> proper#(X):3 5:W:top#(ok(X)) -> active#(X) -->_1 active#(f(X1,X2,X3)) -> c_2(f#(X1,active(X2),X3),active#(X2)):1 6:W:top#(ok(X)) -> top#(active(X)) -->_1 top#(ok(X)) -> top#(active(X)):6 -->_1 top#(ok(X)) -> active#(X):5 -->_1 top#(mark(X)) -> top#(proper(X)):4 -->_1 top#(mark(X)) -> proper#(X):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: active#(f(X1,X2,X3)) -> c_2(active#(X2)) proper#(f(X1,X2,X3)) -> c_8(proper#(X1),proper#(X2),proper#(X3)) *** Step 5.b:1.a:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: active#(f(X1,X2,X3)) -> c_2(active#(X2)) proper#(f(X1,X2,X3)) -> c_8(proper#(X1),proper#(X2),proper#(X3)) - Weak DPs: top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/1,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/3,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_8) = {1,2,3} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [1] x1 + [0] p(b) = [2] p(c) = [2] p(f) = [8] x2 + [8] x3 + [12] p(mark) = [1] x1 + [0] p(ok) = [1] x1 + [0] p(proper) = [1] x1 + [0] p(top) = [1] x1 + [0] p(active#) = [2] x1 + [3] p(f#) = [1] x2 + [2] x3 + [1] p(proper#) = [0] p(top#) = [9] x1 + [4] p(c_1) = [1] p(c_2) = [8] x1 + [2] p(c_3) = [2] p(c_4) = [2] x1 + [2] p(c_5) = [2] x1 + [8] p(c_6) = [2] p(c_7) = [0] p(c_8) = [8] x1 + [2] x2 + [4] x3 + [0] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [4] x1 + [8] x2 + [1] Following rules are strictly oriented: active#(f(X1,X2,X3)) = [16] X2 + [16] X3 + [27] > [16] X2 + [26] = c_2(active#(X2)) Following rules are (at-least) weakly oriented: proper#(f(X1,X2,X3)) = [0] >= [0] = c_8(proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) = [9] X + [4] >= [0] = proper#(X) top#(mark(X)) = [9] X + [4] >= [9] X + [4] = top#(proper(X)) top#(ok(X)) = [9] X + [4] >= [2] X + [3] = active#(X) top#(ok(X)) = [9] X + [4] >= [9] X + [4] = top#(active(X)) active(c()) = [2] >= [2] = mark(b()) active(f(X1,X2,X3)) = [8] X2 + [8] X3 + [12] >= [8] X2 + [8] X3 + [12] = f(X1,active(X2),X3) active(f(b(),X,c())) = [8] X + [28] >= [8] X + [28] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [8] X2 + [8] X3 + [12] >= [8] X2 + [8] X3 + [12] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [8] X2 + [8] X3 + [12] >= [8] X2 + [8] X3 + [12] = ok(f(X1,X2,X3)) proper(b()) = [2] >= [2] = ok(b()) proper(c()) = [2] >= [2] = ok(c()) proper(f(X1,X2,X3)) = [8] X2 + [8] X3 + [12] >= [8] X2 + [8] X3 + [12] = f(proper(X1),proper(X2),proper(X3)) *** Step 5.b:1.a:3: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: proper#(f(X1,X2,X3)) -> c_8(proper#(X1),proper#(X2),proper#(X3)) - Weak DPs: active#(f(X1,X2,X3)) -> c_2(active#(X2)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/1,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/3,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_8) = {1,2,3} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [1] x1 + [0] p(b) = [4] p(c) = [4] p(f) = [2] x1 + [6] x2 + [4] x3 + [1] p(mark) = [1] x1 + [0] p(ok) = [1] x1 + [0] p(proper) = [1] x1 + [0] p(top) = [1] x1 + [0] p(active#) = [2] x1 + [3] p(f#) = [2] p(proper#) = [1] x1 + [0] p(top#) = [2] x1 + [3] p(c_1) = [0] p(c_2) = [1] x1 + [1] p(c_3) = [4] x1 + [1] p(c_4) = [1] p(c_5) = [0] p(c_6) = [1] p(c_7) = [1] p(c_8) = [2] x1 + [1] x2 + [4] x3 + [0] p(c_9) = [1] p(c_10) = [2] Following rules are strictly oriented: proper#(f(X1,X2,X3)) = [2] X1 + [6] X2 + [4] X3 + [1] > [2] X1 + [1] X2 + [4] X3 + [0] = c_8(proper#(X1),proper#(X2),proper#(X3)) Following rules are (at-least) weakly oriented: active#(f(X1,X2,X3)) = [4] X1 + [12] X2 + [8] X3 + [5] >= [2] X2 + [4] = c_2(active#(X2)) top#(mark(X)) = [2] X + [3] >= [1] X + [0] = proper#(X) top#(mark(X)) = [2] X + [3] >= [2] X + [3] = top#(proper(X)) top#(ok(X)) = [2] X + [3] >= [2] X + [3] = active#(X) top#(ok(X)) = [2] X + [3] >= [2] X + [3] = top#(active(X)) active(c()) = [4] >= [4] = mark(b()) active(f(X1,X2,X3)) = [2] X1 + [6] X2 + [4] X3 + [1] >= [2] X1 + [6] X2 + [4] X3 + [1] = f(X1,active(X2),X3) active(f(b(),X,c())) = [6] X + [25] >= [6] X + [25] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [2] X1 + [6] X2 + [4] X3 + [1] >= [2] X1 + [6] X2 + [4] X3 + [1] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [2] X1 + [6] X2 + [4] X3 + [1] >= [2] X1 + [6] X2 + [4] X3 + [1] = ok(f(X1,X2,X3)) proper(b()) = [4] >= [4] = ok(b()) proper(c()) = [4] >= [4] = ok(c()) proper(f(X1,X2,X3)) = [2] X1 + [6] X2 + [4] X3 + [1] >= [2] X1 + [6] X2 + [4] X3 + [1] = f(proper(X1),proper(X2),proper(X3)) *** Step 5.b:1.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: active#(f(X1,X2,X3)) -> c_2(active#(X2)) proper#(f(X1,X2,X3)) -> c_8(proper#(X1),proper#(X2),proper#(X3)) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/1,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/3,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 5.b:1.b:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) - Weak DPs: active#(f(X1,X2,X3)) -> active#(X2) active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) -> proper#(X1) proper#(f(X1,X2,X3)) -> proper#(X2) proper#(f(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [0] p(b) = [0] p(c) = [0] p(f) = [1] x2 + [0] p(mark) = [1] x1 + [0] p(ok) = [1] x1 + [1] p(proper) = [1] p(top) = [1] p(active#) = [6] p(f#) = [4] x2 + [0] p(proper#) = [4] p(top#) = [6] p(c_1) = [4] p(c_2) = [0] p(c_3) = [1] x1 + [2] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [0] p(c_6) = [0] p(c_7) = [1] p(c_8) = [1] x2 + [2] p(c_9) = [1] x1 + [1] x2 + [0] p(c_10) = [1] x1 + [1] x2 + [4] Following rules are strictly oriented: f#(ok(X1),ok(X2),ok(X3)) = [4] X2 + [4] > [4] X2 + [0] = c_5(f#(X1,X2,X3)) Following rules are (at-least) weakly oriented: active#(f(X1,X2,X3)) = [6] >= [6] = active#(X2) active#(f(X1,X2,X3)) = [6] >= [0] = f#(X1,active(X2),X3) f#(X1,mark(X2),X3) = [4] X2 + [0] >= [4] X2 + [0] = c_4(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) = [4] >= [4] = f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) = [4] >= [4] = proper#(X1) proper#(f(X1,X2,X3)) = [4] >= [4] = proper#(X2) proper#(f(X1,X2,X3)) = [4] >= [4] = proper#(X3) top#(mark(X)) = [6] >= [4] = proper#(X) top#(mark(X)) = [6] >= [6] = top#(proper(X)) top#(ok(X)) = [6] >= [6] = active#(X) top#(ok(X)) = [6] >= [6] = top#(active(X)) active(c()) = [0] >= [0] = mark(b()) active(f(X1,X2,X3)) = [0] >= [0] = f(X1,active(X2),X3) active(f(b(),X,c())) = [0] >= [0] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [1] X2 + [0] >= [1] X2 + [0] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [1] X2 + [1] >= [1] X2 + [1] = ok(f(X1,X2,X3)) proper(b()) = [1] >= [1] = ok(b()) proper(c()) = [1] >= [1] = ok(c()) proper(f(X1,X2,X3)) = [1] >= [1] = f(proper(X1),proper(X2),proper(X3)) *** Step 5.b:1.b:2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) - Weak DPs: active#(f(X1,X2,X3)) -> active#(X2) active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) -> proper#(X1) proper#(f(X1,X2,X3)) -> proper#(X2) proper#(f(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_4) = {1}, uargs(c_5) = {1} Following symbols are considered usable: {active,f,proper,active#,f#,proper#,top#} TcT has computed the following interpretation: p(active) = [1] p(b) = [0] p(c) = [0] p(f) = [1] x2 + [0] p(mark) = [1] x1 + [1] p(ok) = [1] x1 + [1] p(proper) = [1] p(top) = [4] p(active#) = [1] p(f#) = [1] x2 + [0] p(proper#) = [2] p(top#) = [2] x1 + [0] p(c_1) = [1] p(c_2) = [1] x2 + [1] p(c_3) = [1] p(c_4) = [1] x1 + [0] p(c_5) = [1] x1 + [1] p(c_6) = [2] p(c_7) = [1] p(c_8) = [1] x1 + [2] x2 + [4] p(c_9) = [1] x2 + [1] p(c_10) = [0] Following rules are strictly oriented: f#(X1,mark(X2),X3) = [1] X2 + [1] > [1] X2 + [0] = c_4(f#(X1,X2,X3)) Following rules are (at-least) weakly oriented: active#(f(X1,X2,X3)) = [1] >= [1] = active#(X2) active#(f(X1,X2,X3)) = [1] >= [1] = f#(X1,active(X2),X3) f#(ok(X1),ok(X2),ok(X3)) = [1] X2 + [1] >= [1] X2 + [1] = c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) = [2] >= [1] = f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) = [2] >= [2] = proper#(X1) proper#(f(X1,X2,X3)) = [2] >= [2] = proper#(X2) proper#(f(X1,X2,X3)) = [2] >= [2] = proper#(X3) top#(mark(X)) = [2] X + [2] >= [2] = proper#(X) top#(mark(X)) = [2] X + [2] >= [2] = top#(proper(X)) top#(ok(X)) = [2] X + [2] >= [1] = active#(X) top#(ok(X)) = [2] X + [2] >= [2] = top#(active(X)) active(c()) = [1] >= [1] = mark(b()) active(f(X1,X2,X3)) = [1] >= [1] = f(X1,active(X2),X3) active(f(b(),X,c())) = [1] >= [1] = mark(f(X,c(),X)) f(X1,mark(X2),X3) = [1] X2 + [1] >= [1] X2 + [1] = mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) = [1] X2 + [1] >= [1] X2 + [1] = ok(f(X1,X2,X3)) proper(b()) = [1] >= [1] = ok(b()) proper(c()) = [1] >= [1] = ok(c()) proper(f(X1,X2,X3)) = [1] >= [1] = f(proper(X1),proper(X2),proper(X3)) *** Step 5.b:1.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: active#(f(X1,X2,X3)) -> active#(X2) active#(f(X1,X2,X3)) -> f#(X1,active(X2),X3) f#(X1,mark(X2),X3) -> c_4(f#(X1,X2,X3)) f#(ok(X1),ok(X2),ok(X3)) -> c_5(f#(X1,X2,X3)) proper#(f(X1,X2,X3)) -> f#(proper(X1),proper(X2),proper(X3)) proper#(f(X1,X2,X3)) -> proper#(X1) proper#(f(X1,X2,X3)) -> proper#(X2) proper#(f(X1,X2,X3)) -> proper#(X3) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) - Weak TRS: active(c()) -> mark(b()) active(f(X1,X2,X3)) -> f(X1,active(X2),X3) active(f(b(),X,c())) -> mark(f(X,c(),X)) f(X1,mark(X2),X3) -> mark(f(X1,X2,X3)) f(ok(X1),ok(X2),ok(X3)) -> ok(f(X1,X2,X3)) proper(b()) -> ok(b()) proper(c()) -> ok(c()) proper(f(X1,X2,X3)) -> f(proper(X1),proper(X2),proper(X3)) - Signature: {active/1,f/3,proper/1,top/1,active#/1,f#/3,proper#/1,top#/1} / {b/0,c/0,mark/1,ok/1,c_1/0,c_2/2,c_3/1,c_4/1 ,c_5/1,c_6/0,c_7/0,c_8/4,c_9/2,c_10/2} - Obligation: innermost runtime complexity wrt. defined symbols {active#,f#,proper#,top#} and constructors {b,c,mark,ok} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^5))