WORST_CASE(?,O(n^1)) * Step 1: NaturalMI 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: 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(if) = {3} Following symbols are considered usable: {f,perfectp} TcT has computed the following interpretation: p(0) = [0] p(f) = [10] x1 + [1] p(false) = [0] p(if) = [1] x3 + [2] p(le) = [1] x2 + [0] p(minus) = [0] p(perfectp) = [10] x1 + [1] p(s) = [1] x1 + [3] p(true) = [0] Following rules are strictly oriented: f(0(),y,0(),u) = [1] > [0] = true() f(0(),y,s(z),u) = [1] > [0] = false() f(s(x),0(),z,u) = [10] x + [31] > [10] x + [1] = f(x,u,minus(z,s(x)),u) f(s(x),s(y),z,u) = [10] x + [31] > [10] x + [3] = if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u)) perfectp(0()) = [1] > [0] = false() perfectp(s(x)) = [10] x + [31] > [10] x + [1] = f(x,s(0()),s(x),s(x)) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))