WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even(Cons(x,Nil())) -> False() even(Cons(x',Cons(x,xs))) -> even(xs) even(Nil()) -> True() goal(x,y) -> and(lte(x,y),even(x)) lte(Cons(x,xs),Nil()) -> False() lte(Cons(x',xs'),Cons(x,xs)) -> lte(xs',xs) lte(Nil(),y) -> True() notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() - Signature: {and/2,even/1,goal/2,lte/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,even,goal,lte,notEmpty} and constructors {Cons,False ,Nil,True} + Applied Processor: NaturalPI {shape = Linear, restrict = NoRestrict, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(and) = {1,2} Following symbols are considered usable: {and,even,goal,lte,notEmpty} TcT has computed the following interpretation: p(Cons) = 4 + x1 + x2 p(False) = 0 p(Nil) = 3 p(True) = 0 p(and) = 4 + x1 + 5*x2 p(even) = 1 + x1 p(goal) = 10 + 12*x1 + 8*x2 p(lte) = 4*x1 p(notEmpty) = 4*x1 Following rules are strictly oriented: even(Cons(x,Nil())) = 8 + x > 0 = False() even(Cons(x',Cons(x,xs))) = 9 + x + x' + xs > 1 + xs = even(xs) even(Nil()) = 4 > 0 = True() goal(x,y) = 10 + 12*x + 8*y > 9 + 9*x = and(lte(x,y),even(x)) lte(Cons(x,xs),Nil()) = 16 + 4*x + 4*xs > 0 = False() lte(Cons(x',xs'),Cons(x,xs)) = 16 + 4*x' + 4*xs' > 4*xs' = lte(xs',xs) lte(Nil(),y) = 12 > 0 = True() notEmpty(Cons(x,xs)) = 16 + 4*x + 4*xs > 0 = True() notEmpty(Nil()) = 12 > 0 = False() Following rules are (at-least) weakly oriented: and(False(),False()) = 4 >= 0 = False() and(False(),True()) = 4 >= 0 = False() and(True(),False()) = 4 >= 0 = False() and(True(),True()) = 4 >= 0 = True() WORST_CASE(?,O(n^1))