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