Termination Proof using AProVE

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

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

ACK_IN(s(m), 0) -> U11(ack_in(m, s(0)))
ACK_IN(s(m), 0) -> ACK_IN(m, s(0))
ACK_IN(s(m), s(n)) -> U21(ack_in(s(m), n), m)
ACK_IN(s(m), s(n)) -> ACK_IN(s(m), n)
U21(ack_out(n), m) -> U22(ack_in(m, n))
U21(ack_out(n), m) -> ACK_IN(m, n)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

ACK_IN(s(m), s(n)) -> ACK_IN(s(m), n)
U21(ack_out(n), m) -> ACK_IN(m, n)
ACK_IN(s(m), s(n)) -> U21(ack_in(s(m), n), m)
ACK_IN(s(m), 0) -> ACK_IN(m, s(0))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(m), s(n)) -> U21(ack_in(s(m), n), m)

two new Dependency Pairs are created:

ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Forward Instantiation Transformation

Dependency Pairs:

ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(n), m) -> ACK_IN(m, n)
ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')
ACK_IN(s(m), 0) -> ACK_IN(m, s(0))
ACK_IN(s(m), s(n)) -> ACK_IN(s(m), n)

Rules:

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

Strategy:

innermost

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

ACK_IN(s(m), 0) -> ACK_IN(m, s(0))

two new Dependency Pairs are created:

ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')
ACK_IN(s(m), s(n)) -> ACK_IN(s(m), n)
U21(ack_out(n), m) -> ACK_IN(m, n)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')

Rules:

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

Strategy:

innermost

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

ACK_IN(s(m), s(n)) -> ACK_IN(s(m), n)

five new Dependency Pairs are created:

ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(n), m) -> ACK_IN(m, n)
ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))

Rules:

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

Strategy:

innermost

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

U21(ack_out(n), m) -> ACK_IN(m, n)

eight new Dependency Pairs are created:

U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(m''), s(0)) -> U21(u11(ack_in(m'', s(0))), m'')

five new Dependency Pairs are created:

ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(ack_in(s(m''''''), s(0))), s(m''''''))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''')), s(0))), s(s(m'''''')))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''')), s(0))), s(s(m'''''''')))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 6

                 ↳Rewriting Transformation

Dependency Pairs:

ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''')), s(0))), s(s(m'''''''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''')), s(0))), s(s(m'''''')))
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(ack_in(s(m''''''), s(0))), s(m''''''))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(ack_in(s(m''''''), s(0))), s(m''''''))

one new Dependency Pair is created:

ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 7

                 ↳Rewriting Transformation

Dependency Pairs:

ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''')), s(0))), s(s(m'''''''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''')), s(0))), s(s(m'''''')))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''')), s(0))), s(s(m'''''')))

one new Dependency Pair is created:

ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 8

                 ↳Rewriting Transformation

Dependency Pairs:

ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''')), s(0))), s(s(m'''''''')))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''')), s(0))), s(s(m'''''''')))

one new Dependency Pair is created:

ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''')), 0), s(m''''''''))), s(s(m'''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 9

                 ↳Rewriting Transformation

Dependency Pairs:

ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''')), 0), s(m''''''''))), s(s(m'''''''')))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(s(m''''')), s(0)) -> U21(u11(ack_in(s(m'''''), s(0))), s(m'''''))

one new Dependency Pair is created:

ACK_IN(s(s(m''''')), s(0)) -> U21(u11(u21(ack_in(s(m'''''), 0), m''''')), s(m'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 10

                 ↳Rewriting Transformation

Dependency Pairs:

ACK_IN(s(s(m''''')), s(0)) -> U21(u11(u21(ack_in(s(m'''''), 0), m''''')), s(m'''''))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''')), 0), s(m''''''''))), s(s(m'''''''')))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(ack_in(s(s(m'''''''''')), s(0))), s(s(m'''''''''')))

one new Dependency Pair is created:

ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''''')), 0), s(m''''''''''))), s(s(m'''''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''''')), 0), s(m''''''''''))), s(s(m'''''''''')))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''')), 0), s(m''''''''))), s(s(m'''''''')))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(u21(ack_in(s(m'''''), 0), m''''')), s(m'''''))

Rules:

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

Strategy:

innermost

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

ACK_IN(s(m''), s(s(n''))) -> U21(u21(ack_in(s(m''), n''), m''), m'')

five new Dependency Pairs are created:

ACK_IN(s(s(m'''''')), s(s(n'''))) -> U21(u21(ack_in(s(s(m'''''')), n'''), s(m'''''')), s(m''''''))
ACK_IN(s(s(s(m''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''))), n'''), s(s(m''''''))), s(s(m'''''')))
ACK_IN(s(s(s(m''''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''''))), n'''), s(s(m''''''''))), s(s(m'''''''')))
ACK_IN(s(s(m''''')), s(s(n'''))) -> U21(u21(ack_in(s(s(m''''')), n'''), s(m''''')), s(m'''''))
ACK_IN(s(s(s(m''''''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''''''))), n'''), s(s(m''''''''''))), s(s(m'''''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 12

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

ACK_IN(s(s(s(m''''''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''''''))), n'''), s(s(m''''''''''))), s(s(m'''''''''')))
ACK_IN(s(s(m''''')), s(s(n'''))) -> U21(u21(ack_in(s(s(m''''')), n'''), s(m''''')), s(m'''''))
ACK_IN(s(s(s(m''''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''''))), n'''), s(s(m''''''''))), s(s(m'''''''')))
ACK_IN(s(s(m''''')), s(0)) -> U21(u11(u21(ack_in(s(m'''''), 0), m''''')), s(m'''''))
U21(ack_out(s(0)), s(s(m''''''''))) -> ACK_IN(s(s(m'''''''')), s(0))
ACK_IN(s(s(s(m''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''')), 0), s(m''''''''))), s(s(m'''''''')))
U21(ack_out(s(0)), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), s(0))
ACK_IN(s(s(s(m''''''))), s(s(n'''))) -> U21(u21(ack_in(s(s(s(m''''''))), n'''), s(s(m''''''))), s(s(m'''''')))
ACK_IN(s(m'), s(s(s(n'''')))) -> ACK_IN(s(m'), s(s(n'''')))
U21(ack_out(s(s(s(n'''''')))), s(m''')) -> ACK_IN(s(m'''), s(s(s(n''''''))))
ACK_IN(s(s(m'''''')), s(s(n'''))) -> U21(u21(ack_in(s(s(m'''''')), n'''), s(m'''''')), s(m''''''))
U21(ack_out(s(s(0))), s(m''')) -> ACK_IN(s(m'''), s(s(0)))
U21(ack_out(0), s(s(m''''''))) -> ACK_IN(s(s(m'''''')), 0)
U21(ack_out(0), s(s(m''''))) -> ACK_IN(s(s(m'''')), 0)
ACK_IN(s(s(s(m''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''')), 0), s(m''''''))), s(s(m'''''')))
ACK_IN(s(m'), s(s(0))) -> ACK_IN(s(m'), s(0))
ACK_IN(s(m''), s(s(n''))) -> ACK_IN(s(m''), s(n''))
U21(ack_out(s(s(n''''))), s(m'''')) -> ACK_IN(s(m''''), s(s(n'''')))
ACK_IN(s(s(m'''''')), s(0)) -> U21(u11(u21(ack_in(s(m''''''), 0), m'''''')), s(m''''''))
ACK_IN(s(s(m'''')), 0) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(m'''''')), s(0)) -> ACK_IN(s(s(m'''''')), 0)
ACK_IN(s(s(m'')), 0) -> ACK_IN(s(m''), s(0))
ACK_IN(s(s(m'''')), s(0)) -> ACK_IN(s(s(m'''')), 0)
U21(ack_out(s(0)), s(m'''')) -> ACK_IN(s(m''''), s(0))
ACK_IN(s(s(s(m''''''''''))), s(0)) -> U21(u11(u21(ack_in(s(s(m'''''''''')), 0), s(m''''''''''))), s(s(m'''''''''')))

Rules:

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

Strategy:

innermost

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