Term Rewriting System R:
[X, Y]
ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

ACKIN(s(X), 0) -> U11(ackin(X, s(0)))
ACKIN(s(X), 0) -> ACKIN(X, s(0))
ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
U21(ackout(X), Y) -> U22(ackin(Y, X))
U21(ackout(X), Y) -> ACKIN(Y, X)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)
U21(ackout(X), Y) -> ACKIN(Y, X)
ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
ACKIN(s(X), 0) -> ACKIN(X, s(0))


Rules:


ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

ACKIN(s(X), s(Y)) -> U21(ackin(s(X), Y), X)
two new Dependency Pairs are created:

ACKIN(s(X''), s(0)) -> U21(u11(ackin(X'', s(0))), X'')
ACKIN(s(X''), s(s(Y''))) -> U21(u21(ackin(s(X''), Y''), X''), X'')

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

ACKIN(s(X''), s(s(Y''))) -> U21(u21(ackin(s(X''), Y''), X''), X'')
U21(ackout(X), Y) -> ACKIN(Y, X)
ACKIN(s(X''), s(0)) -> U21(u11(ackin(X'', s(0))), X'')
ACKIN(s(X), 0) -> ACKIN(X, s(0))
ACKIN(s(X), s(Y)) -> ACKIN(s(X), Y)


Rules:


ackin(0, X) -> ackout(s(X))
ackin(s(X), 0) -> u11(ackin(X, s(0)))
ackin(s(X), s(Y)) -> u21(ackin(s(X), Y), X)
u11(ackout(X)) -> ackout(X)
u21(ackout(X), Y) -> u22(ackin(Y, X))
u22(ackout(X)) -> ackout(X)


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:00 minutes