WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: goal(xs) -> ordered(xs) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() ordered(Cons(x,Nil())) -> True() ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) ordered(Nil()) -> True() - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) ordered[Ite](False(),xs) -> False() ordered[Ite](True(),Cons(x',Cons(x,xs))) -> ordered(xs) - Signature: {</2,goal/1,notEmpty/1,ordered/1,ordered[Ite]/2} / {0/0,Cons/2,False/0,Nil/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {<,goal,notEmpty,ordered,ordered[Ite]} and constructors {0 ,Cons,False,Nil,S,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, 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(ordered[Ite]) = {1} Following symbols are considered usable: {<,goal,notEmpty,ordered,ordered[Ite]} TcT has computed the following interpretation: p(0) = [1] p(<) = [0] p(Cons) = [1] x2 + [8] p(False) = [0] p(Nil) = [15] p(S) = [1] x1 + [1] p(True) = [0] p(goal) = [1] x1 + [3] p(notEmpty) = [2] x1 + [0] p(ordered) = [1] x1 + [1] p(ordered[Ite]) = [8] x1 + [1] x2 + [0] Following rules are strictly oriented: goal(xs) = [1] xs + [3] > [1] xs + [1] = ordered(xs) notEmpty(Cons(x,xs)) = [2] xs + [16] > [0] = True() notEmpty(Nil()) = [30] > [0] = False() ordered(Cons(x,Nil())) = [24] > [0] = True() ordered(Cons(x',Cons(x,xs))) = [1] xs + [17] > [1] xs + [16] = ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) ordered(Nil()) = [16] > [0] = True() Following rules are (at-least) weakly oriented: <(x,0()) = [0] >= [0] = False() <(0(),S(y)) = [0] >= [0] = True() <(S(x),S(y)) = [0] >= [0] = <(x,y) ordered[Ite](False(),xs) = [1] xs + [0] >= [0] = False() ordered[Ite](True(),Cons(x',Cons(x,xs))) = [1] xs + [16] >= [1] xs + [1] = ordered(xs) WORST_CASE(?,O(n^1))