WORST_CASE(?,O(1)) * Step 1: Sum WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(1(),y) -> y *(i(x),x) -> 1() - Signature: {*/2} / {0/0,1/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: NaturalMI WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(1(),y) -> y *(i(x),x) -> 1() - Signature: {*/2} / {0/0,1/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(*) = {2} Following symbols are considered usable: {*} TcT has computed the following interpretation: p(*) = [1] x1 + [1] x2 + [1] p(0) = [8] p(1) = [6] p(i) = [8] Following rules are strictly oriented: *(x,0()) = [1] x + [9] > [8] = 0() *(1(),y) = [1] y + [7] > [1] y + [0] = y *(i(x),x) = [1] x + [9] > [6] = 1() Following rules are (at-least) weakly oriented: *(*(x,y),z) = [1] x + [1] y + [1] z + [2] >= [1] x + [1] y + [1] z + [2] = *(x,*(y,z)) * Step 3: NaturalMI WORST_CASE(?,O(1)) + Considered Problem: - Strict TRS: *(*(x,y),z) -> *(x,*(y,z)) - Weak TRS: *(x,0()) -> 0() *(1(),y) -> y *(i(x),x) -> 1() - Signature: {*/2} / {0/0,1/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(*) = {2} Following symbols are considered usable: {*} TcT has computed the following interpretation: p(*) = [5] x1 + [1] x2 + [4] p(0) = [12] p(1) = [5] p(i) = [4] Following rules are strictly oriented: *(*(x,y),z) = [25] x + [5] y + [1] z + [24] > [5] x + [5] y + [1] z + [8] = *(x,*(y,z)) Following rules are (at-least) weakly oriented: *(x,0()) = [5] x + [16] >= [12] = 0() *(1(),y) = [1] y + [29] >= [1] y + [0] = y *(i(x),x) = [1] x + [24] >= [5] = 1() * Step 4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(x,0()) -> 0() *(*(x,y),z) -> *(x,*(y,z)) *(1(),y) -> y *(i(x),x) -> 1() - Signature: {*/2} / {0/0,1/0,i/1} - Obligation: innermost runtime complexity wrt. defined symbols {*} and constructors {0,1,i} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(1))