YES
(VAR n m)
(RULES 
ack_in(0,n) -> ack_out(s(n))
ack_in(s(m),0) -> u11(ack_in(m,s(0)))
u11(ack_out(n)) -> ack_out(n)
ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m)
u21(ack_out(n),m) -> u22(ack_in(m,n))
u22(ack_out(n)) -> ack_out(n)
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for ack_prolog:

-> Dependency pairs:
nF_ack_in(s(m),0) -> nF_u11(ack_in(m,s(0)))
nF_ack_in(s(m),0) -> nF_ack_in(m,s(0))
nF_ack_in(s(m),s(n)) -> nF_u21(ack_in(s(m),n),m)
nF_ack_in(s(m),s(n)) -> nF_ack_in(s(m),n)
nF_u21(ack_out(n),m) -> nF_u22(ack_in(m,n))
nF_u21(ack_out(n),m) -> nF_ack_in(m,n)

-> Proof of termination for ack_prolog_1:
-> -> Dependency pairs in cycle:
nF_ack_in(s(m),0) -> nF_ack_in(m,s(0))
nF_u21(ack_out(n),m) -> nF_ack_in(m,n)
nF_ack_in(s(m),s(n)) -> nF_u21(ack_in(s(m),n),m)
nF_ack_in(s(m),s(n)) -> nF_ack_in(s(m),n)

Dependency pairs oriented using subterm criterion.

-> -> Dependency pairs in cycle:
nF_ack_in(s(m),s(n)) -> nF_ack_in(s(m),n)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.