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