WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: add0(x,Nil()) -> x add0(x',Cons(x,xs)) -> add0(Cons(Cons(Nil(),Nil()),x'),xs) goal(x,y) -> add0(x,y) notEmpty(Cons(x,xs)) -> True() notEmpty(Nil()) -> False() - Signature: {add0/2,goal/2,notEmpty/1} / {Cons/2,False/0,Nil/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {add0,goal,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: none Following symbols are considered usable: {add0,goal,notEmpty} TcT has computed the following interpretation: p(Cons) = 1 + x2 p(False) = 4 p(Nil) = 1 p(True) = 1 p(add0) = 14*x1 + 15*x2 p(goal) = 10 + 15*x1 + 15*x2 p(notEmpty) = 14 + 2*x1 Following rules are strictly oriented: add0(x,Nil()) = 15 + 14*x > x = x add0(x',Cons(x,xs)) = 15 + 14*x' + 15*xs > 14 + 14*x' + 15*xs = add0(Cons(Cons(Nil(),Nil()),x'),xs) goal(x,y) = 10 + 15*x + 15*y > 14*x + 15*y = add0(x,y) notEmpty(Cons(x,xs)) = 16 + 2*xs > 1 = True() notEmpty(Nil()) = 16 > 4 = False() Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))