Termination Proof using AProVE

Term Rewriting System R:
[x, y]
plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

PLUS(s(s(x)), y) -> PLUS(x, s(y))
PLUS(x, s(s(y))) -> PLUS(s(x), y)
ACK(s(x), 0) -> ACK(x, s(0))
ACK(s(x), s(y)) -> ACK(x, plus(y, ack(s(x), y)))
ACK(s(x), s(y)) -> PLUS(y, ack(s(x), y))
ACK(s(x), s(y)) -> ACK(s(x), y)

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳Nar

Dependency Pairs:

PLUS(x, s(s(y))) -> PLUS(s(x), y)
PLUS(s(s(x)), y) -> PLUS(x, s(y))

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

PLUS(x, s(s(y))) -> PLUS(s(x), y)
PLUS(s(s(x)), y) -> PLUS(x, s(y))

There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

POL(PLUS(x₁, x₂)) = 1 + x₁ + x₂

POL(s(x₁)) = 1 + x₁

resulting in one new DP problem.
Used Argument Filtering System:

PLUS(x₁, x₂) -> PLUS(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳Dependency Graph

       →DP Problem 2

         ↳Nar

Dependency Pair:

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Narrowing Transformation

Dependency Pairs:

ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x), s(y)) -> ACK(x, plus(y, ack(s(x), y)))
ACK(s(x), 0) -> ACK(x, s(0))

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

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

ACK(s(x), s(y)) -> ACK(x, plus(y, ack(s(x), y)))

five new Dependency Pairs are created:

ACK(s(x0), s(s(s(x'')))) -> ACK(x0, s(plus(x'', s(ack(s(x0), s(s(x'')))))))
ACK(s(x'), s(s(0))) -> ACK(x', s(ack(s(x'), s(0))))
ACK(s(x'), s(0)) -> ACK(x', ack(s(x'), 0))
ACK(s(x''), s(0)) -> ACK(x'', plus(0, ack(x'', s(0))))
ACK(s(x''), s(s(y''))) -> ACK(x'', plus(s(y''), ack(x'', plus(y'', ack(s(x''), y'')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Forward Instantiation Transformation

Dependency Pairs:

ACK(s(x''), s(s(y''))) -> ACK(x'', plus(s(y''), ack(x'', plus(y'', ack(s(x''), y'')))))
ACK(s(x''), s(0)) -> ACK(x'', plus(0, ack(x'', s(0))))
ACK(s(x'), s(s(0))) -> ACK(x', s(ack(s(x'), s(0))))
ACK(s(x0), s(s(s(x'')))) -> ACK(x0, s(plus(x'', s(ack(s(x0), s(s(x'')))))))
ACK(s(x'), s(0)) -> ACK(x', ack(s(x'), 0))
ACK(s(x), 0) -> ACK(x, s(0))
ACK(s(x), s(y)) -> ACK(s(x), y)

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

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

ACK(s(x), 0) -> ACK(x, s(0))

three new Dependency Pairs are created:

ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(s(x''')), 0) -> ACK(s(x'''), s(0))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))
ACK(s(s(x''')), 0) -> ACK(s(x'''), s(0))
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(x''), s(0)) -> ACK(x'', plus(0, ack(x'', s(0))))
ACK(s(x'), s(0)) -> ACK(x', ack(s(x'), 0))
ACK(s(x'), s(s(0))) -> ACK(x', s(ack(s(x'), s(0))))
ACK(s(x0), s(s(s(x'')))) -> ACK(x0, s(plus(x'', s(ack(s(x0), s(s(x'')))))))
ACK(s(x), s(y)) -> ACK(s(x), y)
ACK(s(x''), s(s(y''))) -> ACK(x'', plus(s(y''), ack(x'', plus(y'', ack(s(x''), y'')))))

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

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

ACK(s(x), s(y)) -> ACK(s(x), y)

eight new Dependency Pairs are created:

ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
ACK(s(x'), s(s(s(s(x''''))))) -> ACK(s(x'), s(s(s(x''''))))
ACK(s(x'), s(s(s(0)))) -> ACK(s(x'), s(s(0)))
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(s(x''''')), s(0)) -> ACK(s(s(x''''')), 0)
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 6

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

ACK(s(x'), s(s(s(y'''')))) -> ACK(s(x'), s(s(y'''')))
ACK(s(x'), s(s(0))) -> ACK(s(x'), s(0))
ACK(s(x'), s(s(s(0)))) -> ACK(s(x'), s(s(0)))
ACK(s(x'), s(s(s(s(x''''))))) -> ACK(s(x'), s(s(s(x''''))))
ACK(s(x''), s(s(y''))) -> ACK(s(x''), s(y''))
ACK(s(s(x'''''')), s(0)) -> ACK(s(s(x'''''')), 0)
ACK(s(s(x''''')), s(0)) -> ACK(s(s(x''''')), 0)
ACK(s(s(x''')), 0) -> ACK(s(x'''), s(0))
ACK(s(s(x'''')), s(0)) -> ACK(s(s(x'''')), 0)
ACK(s(s(x'')), 0) -> ACK(s(x''), s(0))
ACK(s(x''), s(s(y''))) -> ACK(x'', plus(s(y''), ack(x'', plus(y'', ack(s(x''), y'')))))
ACK(s(x''), s(0)) -> ACK(x'', plus(0, ack(x'', s(0))))
ACK(s(x'), s(s(0))) -> ACK(x', s(ack(s(x'), s(0))))
ACK(s(x0), s(s(s(x'')))) -> ACK(x0, s(plus(x'', s(ack(s(x0), s(s(x'')))))))
ACK(s(x'), s(0)) -> ACK(x', ack(s(x'), 0))
ACK(s(s(x'''')), 0) -> ACK(s(x''''), s(0))

Rules:

plus(s(s(x)), y) -> s(plus(x, s(y)))
plus(x, s(s(y))) -> s(plus(s(x), y))
plus(s(0), y) -> s(y)
plus(0, y) -> y
ack(0, y) -> s(y)
ack(s(x), 0) -> ack(x, s(0))
ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y)))

Strategy:

innermost

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

POL(PLUS(x₁, x₂))	= 1 + x₁ + x₂
POL(s(x₁))	= 1 + x₁