Termination Proof using AProVE

Term Rewriting System R:
[X, Y, Z, X1, X2, X3, X4]
plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

PLUS(s(X), plus(Y, Z)) -> PLUS(X, plus(s(s(Y)), Z))
PLUS(s(X), plus(Y, Z)) -> PLUS(s(s(Y)), Z)
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X2, X4)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) -> PLUS(s(s(Y)), Z)
PLUS(s(X), plus(Y, Z)) -> PLUS(X, plus(s(s(Y)), Z))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(X), plus(Y, Z)) -> PLUS(X, plus(s(s(Y)), Z))

two new Dependency Pairs are created:

PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(X), plus(Y, Z)) -> PLUS(s(s(Y)), Z)
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(X), plus(Y, Z)) -> PLUS(s(s(Y)), Z)

three new Dependency Pairs are created:

PLUS(s(X), plus(Y0, plus(Y'', Z''))) -> PLUS(s(s(Y0)), plus(Y'', Z''))
PLUS(s(X), plus(Y', plus(X2'', plus(X3'', X4'')))) -> PLUS(s(s(Y')), plus(X2'', plus(X3'', X4'')))
PLUS(s(X), plus(Y', plus(Y''', Z'''))) -> PLUS(s(s(Y')), plus(Y''', Z'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(X), plus(Y', plus(Y''', Z'''))) -> PLUS(s(s(Y')), plus(Y''', Z'''))
PLUS(s(X), plus(Y', plus(X2'', plus(X3'', X4'')))) -> PLUS(s(s(Y')), plus(X2'', plus(X3'', X4'')))
PLUS(s(X), plus(Y0, plus(Y'', Z''))) -> PLUS(s(s(Y0)), plus(Y'', Z''))
PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X1, plus(X3, plus(X2, X4)))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X1, plus(X3, plus(X2, X4)))

four new Dependency Pairs are created:

PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(X), plus(Y', plus(X2'', plus(X3'', X4'')))) -> PLUS(s(s(Y')), plus(X2'', plus(X3'', X4'')))
PLUS(s(X), plus(Y0, plus(Y'', Z''))) -> PLUS(s(s(Y0)), plus(Y'', Z''))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))
PLUS(s(X), plus(Y', plus(Y''', Z'''))) -> PLUS(s(s(Y')), plus(Y''', Z'''))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(X1), plus(X2, plus(X3, X4))) -> PLUS(X3, plus(X2, X4))

six new Dependency Pairs are created:

PLUS(s(X1), plus(X2', plus(s(X1''), X4'))) -> PLUS(s(X1''), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X'''')), X4'))) -> PLUS(s(s(X'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X1'''')), X4'))) -> PLUS(s(s(X1'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(X''), X4'))) -> PLUS(s(X''), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(s(X''''''))), X4'))) -> PLUS(s(s(s(X''''''))), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(s(X1''''''))), X4'))) -> PLUS(s(s(s(X1''''''))), plus(X2', X4'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Argument Filtering and Ordering

Dependency Pairs:

PLUS(s(X1), plus(X2', plus(s(s(s(X1''''''))), X4'))) -> PLUS(s(s(s(X1''''''))), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(s(X''''''))), X4'))) -> PLUS(s(s(s(X''''''))), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(X''), X4'))) -> PLUS(s(X''), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X1'''')), X4'))) -> PLUS(s(s(X1'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X'''')), X4'))) -> PLUS(s(s(X'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(X1''), X4'))) -> PLUS(s(X1''), plus(X2', X4'))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(X), plus(Y', plus(Y''', Z'''))) -> PLUS(s(s(Y')), plus(Y''', Z'''))
PLUS(s(X), plus(Y', plus(X2'', plus(X3'', X4'')))) -> PLUS(s(s(Y')), plus(X2'', plus(X3'', X4'')))
PLUS(s(X), plus(Y0, plus(Y'', Z''))) -> PLUS(s(s(Y0)), plus(Y'', Z''))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

PLUS(s(X1), plus(X2', plus(s(s(s(X1''''''))), X4'))) -> PLUS(s(s(s(X1''''''))), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(s(X''''''))), X4'))) -> PLUS(s(s(s(X''''''))), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(X''), X4'))) -> PLUS(s(X''), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X1'''')), X4'))) -> PLUS(s(s(X1'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(s(X'''')), X4'))) -> PLUS(s(s(X'''')), plus(X2', X4'))
PLUS(s(X1), plus(X2', plus(s(X1''), X4'))) -> PLUS(s(X1''), plus(X2', X4'))
PLUS(s(X), plus(Y', plus(Y''', Z'''))) -> PLUS(s(s(Y')), plus(Y''', Z'''))
PLUS(s(X), plus(Y', plus(X2'', plus(X3'', X4'')))) -> PLUS(s(s(Y')), plus(X2'', plus(X3'', X4'')))
PLUS(s(X), plus(Y0, plus(Y'', Z''))) -> PLUS(s(s(Y0)), plus(Y'', Z''))

The following usable rules for innermost w.r.t. to the AFS can be oriented:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(s(x₁)) = x₁

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

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

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(X'')), plus(Y', Z')) -> PLUS(s(X''), plus(s(s(Y')), Z'))

four new Dependency Pairs are created:

PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(X1'')), plus(Y', Z')) -> PLUS(s(X1''), plus(s(s(Y')), Z'))

six new Dependency Pairs are created:

PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(X1'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X1''), plus(X3', plus(X2', X4')))

eight new Dependency Pairs are created:

PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(X'')), plus(X2', plus(X3', X4'))) -> PLUS(s(X''), plus(X3', plus(X2', X4')))

nine new Dependency Pairs are created:

PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(s(X''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X'''')), plus(X3', plus(X2', X4')))

10 new Dependency Pairs are created:

PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

Dependency Pairs:

PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

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

PLUS(s(s(s(X1''''))), plus(X2', plus(X3', X4'))) -> PLUS(s(s(X1'''')), plus(X3', plus(X2', X4')))

12 new Dependency Pairs are created:

PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(s(X''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(s(X1''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 12

                 ↳Argument Filtering and Ordering

Dependency Pairs:

PLUS(s(s(s(s(s(s(s(s(s(X1''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(s(X''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

PLUS(s(s(s(s(s(s(s(s(s(X1''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(s(X''''''''''''''''))))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(s(X'''''''''''''''')))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X1'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X1''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(s(X'''''''''''''')))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(s(X''''''''''''''))))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X1''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X1'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(s(X''''''''''''))))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(s(X'''''''''''')))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X1'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X1''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(s(X'''''''''')))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(s(X''''''''''))))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X1'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X''''''''))))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(s(X'''''''')))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(X1'''''')))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(s(X1''''''))), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(X1''''))), plus(X2'', plus(X3'', X4''))) -> PLUS(s(s(X1'''')), plus(X3'', plus(X2'', X4'')))
PLUS(s(s(s(s(s(X1''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X1'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(s(X''''''''))))), plus(Y'', Z'')) -> PLUS(s(s(s(s(X'''''''')))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X''''))), plus(Y'', Z'')) -> PLUS(s(s(X'''')), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X1'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X1''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(s(X'''''')))), plus(Y'', Z'')) -> PLUS(s(s(s(X''''''))), plus(s(s(Y'')), Z''))
PLUS(s(s(s(X1''''))), plus(Y'', Z'')) -> PLUS(s(s(X1'''')), plus(s(s(Y'')), Z''))

The following usable rules for innermost w.r.t. to the AFS can be oriented:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

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₁)
plus(x₁, x₂) -> x₂

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 13

                 ↳Dependency Graph

Dependency Pair:

Rules:

plus(s(X), plus(Y, Z)) -> plus(X, plus(s(s(Y)), Z))
plus(s(X1), plus(X2, plus(X3, X4))) -> plus(X1, plus(X3, plus(X2, X4)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:38 minutes

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