WORST_CASE(?,O(n^1)) * Step 1: Ara 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: { A(0) < :: [A(0) x A(0)] -(1)-> A(13) Cons :: [A(0) x A(3)] -(3)-> A(3) Cons :: [A(0) x A(6)] -(6)-> A(6) False :: [] -(0)-> A(10) False :: [] -(0)-> A(15) False :: [] -(0)-> A(12) Nil :: [] -(0)-> A(3) Nil :: [] -(0)-> A(6) S :: [A(0)] -(0)-> A(0) True :: [] -(0)-> A(10) True :: [] -(0)-> A(15) True :: [] -(0)-> A(13) goal :: [A(8)] -(15)-> A(0) notEmpty :: [A(3)] -(9)-> A(0) ordered :: [A(6)] -(8)-> A(6) ordered[Ite] :: [A(10) x A(6)] -(2)-> A(6) Cost-free Signatures used: -------------------------- 0 :: [] -(0)-> A_cf(0) < :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Cons :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) False :: [] -(0)-> A_cf(0) Nil :: [] -(0)-> A_cf(0) S :: [A_cf(0)] -(0)-> A_cf(0) True :: [] -(0)-> A_cf(0) ordered :: [A_cf(0)] -(0)-> A_cf(0) ordered[Ite] :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0) Base Constructor Signatures used: --------------------------------- 0_A :: [] -(0)-> A(1) Cons_A :: [A(0) x A(1)] -(1)-> A(1) False_A :: [] -(0)-> A(1) Nil_A :: [] -(0)-> A(1) S_A :: [A(0)] -(0)-> A(1) True_A :: [] -(0)-> A(1) * Step 2: Open MAYBE - 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: { 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: {