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

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

ACKIN(s(m), 0) -> U11(ackin(m, s(0)))
ACKIN(s(m), 0) -> ACKIN(m, s(0))
ACKIN(s(m), s(n)) -> U21(ackin(s(m), n), m)
ACKIN(s(m), s(n)) -> ACKIN(s(m), n)
U21(ackout(n), m) -> U22(ackin(m, n))
U21(ackout(n), m) -> ACKIN(m, n)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

ACKIN(s(m), s(n)) -> ACKIN(s(m), n)
U21(ackout(n), m) -> ACKIN(m, n)
ACKIN(s(m), s(n)) -> U21(ackin(s(m), n), m)
ACKIN(s(m), 0) -> ACKIN(m, s(0))


Rules:


ackin(0, n) -> ackout(s(n))
ackin(s(m), 0) -> u11(ackin(m, s(0)))
ackin(s(m), s(n)) -> u21(ackin(s(m), n), m)
u11(ackout(n)) -> ackout(n)
u21(ackout(n), m) -> u22(ackin(m, n))
u22(ackout(n)) -> ackout(n)


Strategy:

innermost




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

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

ACKIN(s(m''), s(0)) -> U21(u11(ackin(m'', s(0))), m'')
ACKIN(s(m''), s(s(n''))) -> U21(u21(ackin(s(m''), n''), m''), m'')

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(m''), s(s(n''))) -> U21(u21(ackin(s(m''), n''), m''), m'')
U21(ackout(n), m) -> ACKIN(m, n)
ACKIN(s(m''), s(0)) -> U21(u11(ackin(m'', s(0))), m'')
ACKIN(s(m), 0) -> ACKIN(m, s(0))
ACKIN(s(m), s(n)) -> ACKIN(s(m), n)


Rules:


ackin(0, n) -> ackout(s(n))
ackin(s(m), 0) -> u11(ackin(m, s(0)))
ackin(s(m), s(n)) -> u21(ackin(s(m), n), m)
u11(ackout(n)) -> ackout(n)
u21(ackout(n), m) -> u22(ackin(m, n))
u22(ackout(n)) -> ackout(n)


Strategy:

innermost



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