WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) - Signature: {minus/2,quot/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {minus,quot} and constructors {0,s} + 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(quot) = {1}, uargs(s) = {1} Following symbols are considered usable: {minus,quot} TcT has computed the following interpretation: p(0) = 1 p(minus) = 1 + x1 p(quot) = 12 + 2*x1 + x2 p(s) = 3 + x1 Following rules are strictly oriented: minus(x,0()) = 1 + x > x = x minus(s(x),s(y)) = 4 + x > 1 + x = minus(x,y) quot(0(),s(y)) = 17 + y > 1 = 0() quot(s(x),s(y)) = 21 + 2*x + y > 20 + 2*x + y = s(quot(minus(x,y),s(y))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))