* Step 1: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(ackin) = [1] x2 + [0] p(ackout) = [1] x1 + [1] p(s) = [1] x1 + [0] p(u21) = [1] x1 + [0] p(u22) = [1] x1 + [0] Following rules are strictly oriented: u21(ackout(X),Y) = [1] X + [1] > [1] X + [0] = u22(ackin(Y,X)) Following rules are (at-least) weakly oriented: ackin(s(X),s(Y)) = [1] Y + [0] >= [1] Y + [0] = u21(ackin(s(X),Y),X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: WeightGap 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following nonconstant growth matrix-interpretation: 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: all TcT has computed the following interpretation: p(ackin) = [1] x2 + [0] p(ackout) = [1] x1 + [0] p(s) = [1] x1 + [1] p(u21) = [1] x1 + [0] p(u22) = [1] x1 + [0] Following rules are strictly oriented: ackin(s(X),s(Y)) = [1] Y + [1] > [1] Y + [0] = u21(ackin(s(X),Y),X) Following rules are (at-least) weakly oriented: u21(ackout(X),Y) = [1] X + [0] >= [1] X + [0] = u22(ackin(Y,X)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * 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))