WORST_CASE(?,O(n^1)) * Step 1: NaturalMI 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: 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(not) = {1}, uargs(s) = {1} Following symbols are considered usable: {+,not,odd} TcT has computed the following interpretation: p(+) = [2] x1 + [2] x2 + [0] p(0) = [6] p(false) = [9] p(not) = [1] x1 + [8] p(odd) = [2] x1 + [4] p(s) = [1] x1 + [8] p(true) = [7] Following rules are strictly oriented: +(x,0()) = [2] x + [12] > [1] x + [0] = x +(x,s(y)) = [2] x + [2] y + [16] > [2] x + [2] y + [8] = s(+(x,y)) +(s(x),y) = [2] x + [2] y + [16] > [2] x + [2] y + [8] = s(+(x,y)) not(false()) = [17] > [7] = true() not(true()) = [15] > [9] = false() odd(0()) = [16] > [9] = false() odd(s(x)) = [2] x + [20] > [2] x + [12] = not(odd(x)) Following rules are (at-least) weakly oriented: WORST_CASE(?,O(n^1))