WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: f(0(),y,0(),u) -> true() f(0(),y,s(z),u) -> false() f(s(x),0(),z,u) -> f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) perfectp(0()) -> false() perfectp(s(x)) -> f(x,s(0()),s(x),s(x)) - Signature: {f/4,perfectp/1} / {0/0,false/0,if/3,le/2,minus/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {f,perfectp} and constructors {0,false,if,le,minus,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(if) = {3} Following symbols are considered usable: {f,perfectp} TcT has computed the following interpretation: p(0) = 6 p(f) = 8 + x1 + 2*x4 p(false) = 10 p(if) = x3 p(le) = 8 + x1 p(minus) = x2 p(perfectp) = 13 + 3*x1 p(s) = 1 + x1 p(true) = 4 Following rules are strictly oriented: f(0(),y,0(),u) = 14 + 2*u > 4 = true() f(0(),y,s(z),u) = 14 + 2*u > 10 = false() f(s(x),0(),z,u) = 9 + 2*u + x > 8 + 2*u + x = f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) = 9 + 2*u + x > 8 + 2*u + x = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) perfectp(0()) = 31 > 10 = false() perfectp(s(x)) = 16 + 3*x > 10 + 3*x = f(x,s(0()),s(x),s(x)) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))