MAYBE * Step 1: WeightGap MAYBE + Considered Problem: - Strict TRS: ack(0(),y) -> s(y) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) - Signature: {ack/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack} and constructors {0,s} + 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(ack) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(ack) = [1] x2 + [1] p(s) = [1] x1 + [13] Following rules are strictly oriented: ack(s(x),s(y)) = [1] y + [14] > [1] y + [2] = ack(x,ack(s(x),y)) Following rules are (at-least) weakly oriented: ack(0(),y) = [1] y + [1] >= [1] y + [13] = s(y) ack(s(x),0()) = [3] >= [16] = ack(x,s(0())) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 2: Failure MAYBE + Considered Problem: - Strict TRS: ack(0(),y) -> s(y) ack(s(x),0()) -> ack(x,s(0())) - Weak TRS: ack(s(x),s(y)) -> ack(x,ack(s(x),y)) - Signature: {ack/2} / {0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {ack} and constructors {0,s} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE