WORST_CASE(?,O(n^1)) * Step 1: Sum WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2} / {*/2,u/0} - Obligation: innermost runtime complexity wrt. defined symbols {+} and constructors {*,u} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: DependencyPairs WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2} / {*/2,u/0} - Obligation: innermost runtime complexity wrt. defined symbols {+} and constructors {*,u} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs +#(*(x,y),*(x,z)) -> c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)) +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) Weak DPs and mark the set of starting terms. * Step 3: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(*(x,y),*(x,z)) -> c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)) +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) - Weak TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2,+#/2} / {*/2,u/0,c_1/1,c_2/2,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {+#} and constructors {*,u} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:+#(*(x,y),*(x,z)) -> c_1(+#(y,z)) -->_1 +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)):2 -->_1 +#(*(x,y),*(x,z)) -> c_1(+#(y,z)):1 2:S:+#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)) -->_2 +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)):3 -->_2 +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)):2 -->_2 +#(*(x,y),*(x,z)) -> c_1(+#(y,z)):1 3:S:+#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) -->_2 +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)):3 -->_1 +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)):3 -->_2 +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)):2 -->_1 +#(*(x,y),+(*(x,z),u())) -> c_2(+#(*(x,+(y,z)),u()),+#(y,z)):2 -->_2 +#(*(x,y),*(x,z)) -> c_1(+#(y,z)):1 -->_1 +#(*(x,y),*(x,z)) -> c_1(+#(y,z)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: +#(*(x,y),+(*(x,z),u())) -> c_2(+#(y,z)) * Step 4: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(*(x,y),*(x,z)) -> c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) -> c_2(+#(y,z)) +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) - Weak TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2,+#/2} / {*/2,u/0,c_1/1,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {+#} and constructors {*,u} + 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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2} Following symbols are considered usable: {+#} TcT has computed the following interpretation: p(*) = [1] x2 + [4] p(+) = [2] x1 + [2] x2 + [0] p(u) = [1] p(+#) = [4] x1 + [0] p(c_1) = [1] x1 + [8] p(c_2) = [1] x1 + [11] p(c_3) = [2] x1 + [2] x2 + [0] Following rules are strictly oriented: +#(*(x,y),*(x,z)) = [4] y + [16] > [4] y + [8] = c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) = [4] y + [16] > [4] y + [11] = c_2(+#(y,z)) Following rules are (at-least) weakly oriented: +#(+(x,y),z) = [8] x + [8] y + [0] >= [8] x + [8] y + [0] = c_3(+#(x,+(y,z)),+#(y,z)) * Step 5: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) - Weak DPs: +#(*(x,y),*(x,z)) -> c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) -> c_2(+#(y,z)) - Weak TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2,+#/2} / {*/2,u/0,c_1/1,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {+#} and constructors {*,u} + 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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_3) = {1,2} Following symbols are considered usable: {+#} TcT has computed the following interpretation: p(*) = [1] x1 + [1] x2 + [0] p(+) = [4] x1 + [4] x2 + [4] p(u) = [0] p(+#) = [4] x1 + [2] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [4] x1 + [4] x2 + [0] Following rules are strictly oriented: +#(+(x,y),z) = [16] x + [16] y + [18] > [16] x + [16] y + [16] = c_3(+#(x,+(y,z)),+#(y,z)) Following rules are (at-least) weakly oriented: +#(*(x,y),*(x,z)) = [4] x + [4] y + [2] >= [4] y + [2] = c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) = [4] x + [4] y + [2] >= [4] y + [2] = c_2(+#(y,z)) * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: +#(*(x,y),*(x,z)) -> c_1(+#(y,z)) +#(*(x,y),+(*(x,z),u())) -> c_2(+#(y,z)) +#(+(x,y),z) -> c_3(+#(x,+(y,z)),+#(y,z)) - Weak TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) +(+(x,y),z) -> +(x,+(y,z)) - Signature: {+/2,+#/2} / {*/2,u/0,c_1/1,c_2/1,c_3/2} - Obligation: innermost runtime complexity wrt. defined symbols {+#} and constructors {*,u} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))