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,xs)) -> ordered(xs) - Signature: { [4] xs + [9] = ordered(xs) notEmpty(Cons(x,xs)) = [5] xs + [16] > [0] = True() notEmpty(Nil()) = [16] > [0] = False() ordered(Cons(x,Nil())) = [25] > [0] = True() ordered(Cons(x',Cons(x,xs))) = [4] xs + [25] > [4] xs + [17] = ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) ordered(Nil()) = [17] > [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) = [4] xs + [1] >= [0] = False() ordered[Ite](True(),Cons(x,xs)) = [4] xs + [9] >= [4] xs + [9] = ordered(xs) WORST_CASE(?,O(n^1))