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)] -(0)-> A(0) Cons :: [A(0) x A(1)] -(1)-> A(1) Cons :: [A(0) x A(2)] -(2)-> A(2) False :: [] -(0)-> A(0) False :: [] -(0)-> A(4) Nil :: [] -(0)-> A(1) Nil :: [] -(0)-> A(2) S :: [A(0)] -(0)-> A(0) True :: [] -(0)-> A(0) goal :: [A(2)] -(7)-> A(0) notEmpty :: [A(1)] -(2)-> A(0) ordered :: [A(2)] -(6)-> A(0) ordered[Ite] :: [A(0) x A(2)] -(4)-> A(0) 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 :: [] -(1)-> 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)] -(1)-> A(1) True_A :: [] -(1)-> 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: {