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. 



   R
     ↳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. 


   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 5
                 ↳Polynomial 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''))


Additionally, the following usable rules for innermost 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(x1, x2))=  1 + x2  
  POL(PLUS(x1, x2))=  1 + x2  
  POL(s(x1))=  0  

resulting in one new DP problem. 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳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: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 12
                 ↳Polynomial 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''))


Additionally, the following usable rules for innermost 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(x1, x2))=  1  
  POL(PLUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳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