WORST_CASE(?,O(n^1)) * Step 1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: 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 + [2] p(False) = [0] p(Nil) = [0] p(True) = [8] p(add0) = [8] x1 + [12] x2 + [1] p(goal) = [8] x1 + [12] x2 + [13] p(notEmpty) = [5] x1 + [3] Following rules are strictly oriented: add0(x,Nil()) = [8] x + [1] > [1] x + [0] = x add0(x',Cons(x,xs)) = [8] x' + [12] xs + [25] > [8] x' + [12] xs + [17] = add0(Cons(Cons(Nil(),Nil()),x'),xs) goal(x,y) = [8] x + [12] y + [13] > [8] x + [12] y + [1] = add0(x,y) notEmpty(Cons(x,xs)) = [5] xs + [13] > [8] = True() notEmpty(Nil()) = [3] > [0] = False() Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))