WORST_CASE(?,O(n^1)) * Step 1: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) - Signature: {ackin/2,u21/2} / {ackout/1,s/1,u22/1} - Obligation: innermost runtime complexity wrt. defined symbols {ackin,u21} and constructors {ackout,s,u22} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(u21) = {1}, uargs(u22) = {1} Following symbols are considered usable: {ackin,u21} TcT has computed the following interpretation: p(ackin) = 2 p(ackout) = 10 p(s) = 1 p(u21) = x1 p(u22) = x1 Following rules are strictly oriented: u21(ackout(X),Y) = 10 > 2 = u22(ackin(Y,X)) Following rules are (at-least) weakly oriented: ackin(s(X),s(Y)) = 2 >= 2 = u21(ackin(s(X),Y),X) * Step 2: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) - Weak TRS: u21(ackout(X),Y) -> u22(ackin(Y,X)) - Signature: {ackin/2,u21/2} / {ackout/1,s/1,u22/1} - Obligation: innermost runtime complexity wrt. defined symbols {ackin,u21} and constructors {ackout,s,u22} + 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(u21) = {1}, uargs(u22) = {1} Following symbols are considered usable: {ackin,u21} TcT has computed the following interpretation: p(ackin) = [1] x2 + [1] p(ackout) = [1] x1 + [0] p(s) = [1] x1 + [8] p(u21) = [1] x1 + [3] p(u22) = [1] x1 + [0] Following rules are strictly oriented: ackin(s(X),s(Y)) = [1] Y + [9] > [1] Y + [4] = u21(ackin(s(X),Y),X) Following rules are (at-least) weakly oriented: u21(ackout(X),Y) = [1] X + [3] >= [1] X + [1] = u22(ackin(Y,X)) * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) - Signature: {ackin/2,u21/2} / {ackout/1,s/1,u22/1} - Obligation: innermost runtime complexity wrt. defined symbols {ackin,u21} and constructors {ackout,s,u22} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))