WORST_CASE(?,O(n^1)) * Step 1: NaturalPI 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: { 2 + xs = ordered(xs) notEmpty(Cons(x,xs)) = 20 + xs > 0 = True() notEmpty(Nil()) = 24 > 0 = False() ordered(Cons(x,Nil())) = 20 > 0 = True() ordered(Cons(x',Cons(x,xs))) = 16 + xs > 14 + xs = ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) ordered(Nil()) = 13 > 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) = xs >= 0 = False() ordered[Ite](True(),Cons(x,xs)) = 7 + xs >= 2 + xs = ordered(xs) WORST_CASE(?,O(n^1))