WORST_CASE(?,O(n^1)) * Step 1: NaturalPI 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: 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(.) = {2}, uargs(cond) = {2} Following symbols are considered usable: {admit,cond} TcT has computed the following interpretation: p(.) = 1 + x2 p(=) = 0 p(admit) = 4 + x1 + 8*x2 p(carry) = 11 p(cond) = 5 + 4*x1 + x2 p(nil) = 2 p(sum) = 1 + x3 p(true) = 3 p(w) = 1 Following rules are strictly oriented: admit(x,.(u,.(v,.(w(),z)))) = 28 + x + 8*z > 23 + 8*z = cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) admit(x,nil()) = 20 + x > 2 = nil() cond(true(),y) = 17 + y > y = y Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))