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: { [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))