WORST_CASE(?,O(n^3)) * Step 1: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: ifMinus(false(),s(X),Y) -> s(minus(X,Y)) ifMinus(true(),s(X),Y) -> 0() le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) minus(0(),Y) -> 0() minus(s(X),Y) -> ifMinus(le(s(X),Y),s(X),Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) - Signature: {ifMinus/3,le/2,minus/2,quot/2} / {0/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {ifMinus,le,minus,quot} and constructors {0,false,s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, 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(ifMinus) = {1}, uargs(quot) = {1}, uargs(s) = {1} Following symbols are considered usable: {ifMinus,le,minus,quot} TcT has computed the following interpretation: p(0) = [0] [0] [1] p(false) = [0] [0] [0] p(ifMinus) = [1 0 0] [1 1 1] [0] [0 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 1] [0] p(le) = [0 0 1] [0] [0 0 0] x1 + [0] [0 0 0] [0] p(minus) = [1 1 2] [1] [0 1 0] x1 + [0] [0 0 1] [0] p(quot) = [2 3 2] [2] [0 1 0] x1 + [0] [0 0 1] [0] p(s) = [1 2 1] [0] [0 1 1] x1 + [0] [0 0 1] [2] p(true) = [0] [0] [0] Following rules are strictly oriented: ifMinus(false(),s(X),Y) = [1 3 3] [2] [0 1 1] X + [0] [0 0 1] [2] > [1 3 3] [1] [0 1 1] X + [0] [0 0 1] [2] = s(minus(X,Y)) ifMinus(true(),s(X),Y) = [1 3 3] [2] [0 1 1] X + [0] [0 0 1] [2] > [0] [0] [1] = 0() le(0(),Y) = [1] [0] [0] > [0] [0] [0] = true() le(s(X),0()) = [0 0 1] [2] [0 0 0] X + [0] [0 0 0] [0] > [0] [0] [0] = false() le(s(X),s(Y)) = [0 0 1] [2] [0 0 0] X + [0] [0 0 0] [0] > [0 0 1] [0] [0 0 0] X + [0] [0 0 0] [0] = le(X,Y) minus(0(),Y) = [3] [0] [1] > [0] [0] [1] = 0() minus(s(X),Y) = [1 3 4] [5] [0 1 1] X + [0] [0 0 1] [2] > [1 3 4] [4] [0 1 1] X + [0] [0 0 1] [2] = ifMinus(le(s(X),Y),s(X),Y) quot(0(),s(Y)) = [4] [0] [1] > [0] [0] [1] = 0() quot(s(X),s(Y)) = [2 7 7] [6] [0 1 1] X + [0] [0 0 1] [2] > [2 7 7] [4] [0 1 1] X + [0] [0 0 1] [2] = s(quot(minus(X,Y),s(Y))) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^3))