WORST_CASE(?,O(n^2)) * Step 1: Sum 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: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalPI 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: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): 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) = 0 p(0) = 0 p(Cons) = 1 p(False) = 0 p(Nil) = 1 p(S) = 1 p(True) = 0 p(loop) = 2 p(loop[Ite]) = 2 + 2*x1 p(match1) = 2 Following rules are strictly oriented: loop(Cons(x,xs),Nil(),pp,ss) = 2 > 0 = False() loop(Nil(),s,pp,ss) = 2 > 0 = True() Following rules are (at-least) weakly oriented: !EQ(0(),0()) = 0 >= 0 = True() !EQ(0(),S(y)) = 0 >= 0 = False() !EQ(S(x),0()) = 0 >= 0 = False() !EQ(S(x),S(y)) = 0 >= 0 = !EQ(x,y) loop(Cons(x',xs'),Cons(x,xs),pp,ss) = 2 >= 2 = loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) loop[Ite](False(),p,s,pp,Cons(x,xs)) = 2 >= 2 = loop(pp,xs,pp,xs) loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = 2 >= 2 = loop(xs',xs,pp,ss) match1(p,s) = 2 >= 2 = loop(p,s,p,s) * Step 3: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) 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(Cons(x,xs),Nil(),pp,ss) -> False() loop(Nil(),s,pp,ss) -> True() 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: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): 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) = 0 p(0) = 0 p(Cons) = x2 p(False) = 0 p(Nil) = 0 p(S) = 1 p(True) = 0 p(loop) = 2*x4 p(loop[Ite]) = x1 + 2*x5 p(match1) = 4 + 2*x2 Following rules are strictly oriented: match1(p,s) = 4 + 2*s > 2*s = loop(p,s,p,s) Following rules are (at-least) weakly oriented: !EQ(0(),0()) = 0 >= 0 = True() !EQ(0(),S(y)) = 0 >= 0 = False() !EQ(S(x),0()) = 0 >= 0 = False() !EQ(S(x),S(y)) = 0 >= 0 = !EQ(x,y) loop(Cons(x,xs),Nil(),pp,ss) = 2*ss >= 0 = False() loop(Cons(x',xs'),Cons(x,xs),pp,ss) = 2*ss >= 2*ss = loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) loop(Nil(),s,pp,ss) = 2*ss >= 0 = True() loop[Ite](False(),p,s,pp,Cons(x,xs)) = 2*xs >= 2*xs = loop(pp,xs,pp,xs) loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = 2*ss >= 2*ss = loop(xs',xs,pp,ss) * Step 4: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: loop(Cons(x',xs'),Cons(x,xs),pp,ss) -> loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) - 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(Cons(x,xs),Nil(),pp,ss) -> False() loop(Nil(),s,pp,ss) -> True() 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) match1(p,s) -> loop(p,s,p,s) - 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: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): 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) = 0 p(0) = 0 p(Cons) = 1 + x2 p(False) = 0 p(Nil) = 0 p(S) = 0 p(True) = 0 p(loop) = 1 + x1 + 2*x3*x4 + x4^2 p(loop[Ite]) = x1 + x1*x4 + x1*x5 + x2 + 2*x4*x5 + x5^2 p(match1) = 1 + 2*x1 + 3*x1*x2 + 3*x1^2 + 2*x2^2 Following rules are strictly oriented: loop(Cons(x',xs'),Cons(x,xs),pp,ss) = 2 + 2*pp*ss + ss^2 + xs' > 1 + 2*pp*ss + ss^2 + xs' = loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss) Following rules are (at-least) weakly oriented: !EQ(0(),0()) = 0 >= 0 = True() !EQ(0(),S(y)) = 0 >= 0 = False() !EQ(S(x),0()) = 0 >= 0 = False() !EQ(S(x),S(y)) = 0 >= 0 = !EQ(x,y) loop(Cons(x,xs),Nil(),pp,ss) = 2 + 2*pp*ss + ss^2 + xs >= 0 = False() loop(Nil(),s,pp,ss) = 1 + 2*pp*ss + ss^2 >= 0 = True() loop[Ite](False(),p,s,pp,Cons(x,xs)) = 1 + p + 2*pp + 2*pp*xs + 2*xs + xs^2 >= 1 + pp + 2*pp*xs + xs^2 = loop(pp,xs,pp,xs) loop[Ite](True(),Cons(x',xs'),Cons(x,xs),pp,ss) = 1 + 2*pp*ss + ss^2 + xs' >= 1 + 2*pp*ss + ss^2 + xs' = loop(xs',xs,pp,ss) match1(p,s) = 1 + 2*p + 3*p*s + 3*p^2 + 2*s^2 >= 1 + p + 2*p*s + s^2 = loop(p,s,p,s) * Step 5: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - 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(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() 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) match1(p,s) -> loop(p,s,p,s) - 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))