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 w.r.t. to the implicit 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(x1, x2)) =  1 + x2 POL(PLUS(x1, x2)) =  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''))

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(plus(x1, x2)) =  1 POL(PLUS(x1, x2)) =  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