WORST_CASE(?,O(n^2)) * Step 1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: loop(Cons(x,xs),Nil(),pp,ss) -> False() loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) loop(Nil(),s,pp,ss) -> True() match1(p,s) -> loop(p,s,p,s) - Weak TRS: !EQ(0(),0()) -> True() !EQ(0(),S(y)) -> False() !EQ(S(x),0()) -> False() !EQ(S(x),S(y)) -> !EQ(x,y) loop[Ite](False(),p,s,pp,Cons(x,xs)) -> loop(pp,xs,pp,xs) loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) -> loop(xs',xs,pp,ss) - Signature: {!EQ/2,loop/4,loop[Ite]/5,match1/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {!EQ,loop,loop[Ite],match1} and constructors {0,Cons,False ,Nil,S,True} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(loop[Ite]) = {1} Following symbols are considered usable: {!EQ,loop,loop[Ite],match1} TcT has computed the following interpretation: p(!EQ) = [2] [1] p(0) = [1] [0] p(Cons) = [1 1] x2 + [0] [0 1] [6] p(False) = [1] [0] p(Nil) = [0] [0] p(S) = [1 0] x1 + [0] [0 0] [0] p(True) = [1] [0] p(loop) = [0 1] x2 + [0 0] x3 + [4 2] x4 + [6] [0 0] [0 6] [0 0] [4] p(loop[Ite]) = [2 1] x1 + [0 1] x3 + [0 0] x4 + [4 2] x5 + [0] [0 0] [0 0] [0 6] [0 0] [4] p(match1) = [1 0] x1 + [4 3] x2 + [7] [0 7] [0 4] [6] Following rules are strictly oriented: loop(Cons(x,xs),Nil(),pp,ss) = [0 0] pp + [4 2] ss + [6] [0 6] [0 0] [4] > [1] [0] = False() loop(Cons(x',xs'),Cons(x,xs),pp,ss) = [0 0] pp + [4 2] ss + [0 1] xs + [12] [0 6] [0 0] [0 0] [4] > [0 0] pp + [4 2] ss + [0 1] xs + [11] [0 6] [0 0] [0 0] [4] = loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) loop(Nil(),s,pp,ss) = [0 0] pp + [0 1] s + [4 2] ss + [6] [0 6] [0 0] [0 0] [4] > [1] [0] = True() match1(p,s) = [1 0] p + [4 3] s + [7] [0 7] [0 4] [6] > [0 0] p + [4 3] s + [6] [0 6] [0 0] [4] = loop(p,s,p,s) Following rules are (at-least) weakly oriented: !EQ(0(),0()) = [2] [1] >= [1] [0] = True() !EQ(0(),S(y)) = [2] [1] >= [1] [0] = False() !EQ(S(x),0()) = [2] [1] >= [1] [0] = False() !EQ(S(x),S(y)) = [2] [1] >= [2] [1] = !EQ(x,y) loop[Ite](False(),p,s,pp,Cons(x,xs)) = [0 0] pp + [0 1] s + [4 6] xs + [14] [0 6] [0 0] [0 0] [4] >= [0 0] pp + [4 3] xs + [6] [0 6] [0 0] [4] = loop(pp,xs,pp,xs) loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = [0 0] pp + [4 2] ss + [0 1] xs + [8] [0 6] [0 0] [0 0] [4] >= [0 0] pp + [4 2] ss + [0 1] xs + [6] [0 6] [0 0] [0 0] [4] = loop(xs',xs,pp,ss) WORST_CASE(?,O(n^2))