WORST_CASE(?,O(n^1)) * Step 1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) -> nil() cond(true(),y) -> y - Signature: {admit/2,cond/2} / {./2,=/2,carry/3,nil/0,sum/3,true/0,w/0} - Obligation: innermost runtime complexity wrt. defined symbols {admit,cond} and constructors {.,=,carry,nil,sum,true,w} + 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: uargs(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = [1] x1 + [1] x2 + [0] p(=) = [6] p(admit) = [4] x1 + [8] x2 + [2] p(carry) = [1] x3 + [0] p(cond) = [1] x1 + [1] x2 + [0] p(nil) = [0] p(sum) = [1] x1 + [1] p(true) = [3] p(w) = [1] Following rules are strictly oriented: admit(x,.(u,.(v,.(w(),z)))) = [8] u + [8] v + [4] x + [8] z + [10] > [1] u + [5] v + [8] z + [9] = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) = [4] x + [2] > [0] = nil() cond(true(),y) = [1] y + [3] > [1] y + [0] = y Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))