WORST_CASE(?,O(n^1)) * Step 1: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(0) = [0] p(<) = [8] p(Cons) = [1] x1 + [1] x2 + [3] p(False) = [0] p(Nil) = [3] p(S) = [1] x1 + [0] p(True) = [0] p(goal) = [10] x1 + [4] p(notEmpty) = [3] x1 + [6] p(ordered) = [1] p(ordered[Ite]) = [1] x1 + [6] Following rules are strictly oriented: goal(xs) = [10] xs + [4] > [1] = ordered(xs) notEmpty(Cons(x,xs)) = [3] x + [3] xs + [15] > [0] = True() notEmpty(Nil()) = [15] > [0] = False() ordered(Cons(x,Nil())) = [1] > [0] = True() ordered(Nil()) = [1] > [0] = True() Following rules are (at-least) weakly oriented: <(x,0()) = [8] >= [0] = False() <(0(),S(y)) = [8] >= [0] = True() <(S(x),S(y)) = [8] >= [8] = <(x,y) ordered(Cons(x',Cons(x,xs))) = [1] >= [14] = ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) ordered[Ite](False(),xs) = [6] >= [0] = False() ordered[Ite](True(),Cons(x',Cons(x,xs))) = [6] >= [1] = ordered(xs) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ordered(Cons(x',Cons(x,xs))) -> ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) goal(xs) -> ordered(xs) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() ordered(Cons(x,Nil())) -> True() ordered(Nil()) -> True() 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 = Just any strict-rules} + 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) = [2] p(<) = [0] p(Cons) = [1] x1 + [1] x2 + [1] p(False) = [0] p(Nil) = [2] p(S) = [2] p(True) = [0] p(goal) = [4] x1 + [12] p(notEmpty) = [10] p(ordered) = [4] x1 + [8] p(ordered[Ite]) = [8] x1 + [4] x2 + [0] Following rules are strictly oriented: ordered(Cons(x',Cons(x,xs))) = [4] x + [4] x' + [4] xs + [16] > [4] x + [4] x' + [4] xs + [8] = ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) 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) goal(xs) = [4] xs + [12] >= [4] xs + [8] = ordered(xs) notEmpty(Cons(x,xs)) = [10] >= [0] = True() notEmpty(Nil()) = [10] >= [0] = False() ordered(Cons(x,Nil())) = [4] x + [20] >= [0] = True() ordered(Nil()) = [16] >= [0] = True() ordered[Ite](False(),xs) = [4] xs + [0] >= [0] = False() ordered[Ite](True(),Cons(x',Cons(x,xs))) = [4] x + [4] x' + [4] xs + [8] >= [4] xs + [8] = ordered(xs) * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: <(x,0()) -> False() <(0(),S(y)) -> True() <(S(x),S(y)) -> <(x,y) 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() 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))