Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

+'(+(x, y), z) -> +'(x, +(y, z))
+'(+(x, y), z) -> +'(y, z)
+'(f(x), f(y)) -> +'(x, y)
+'(f(x), +(f(y), z)) -> +'(f(+(x, y)), z)
+'(f(x), +(f(y), z)) -> +'(x, y)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

+'(f(x), +(f(y), z)) -> +'(x, y)
+'(+(x, y), z) -> +'(y, z)
+'(f(x), f(y)) -> +'(x, y)
+'(+(x, y), z) -> +'(x, +(y, z))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(+(x, y), z) -> +'(x, +(y, z))

three new Dependency Pairs are created:

+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(+(x, f(x'')), f(y'')) -> +'(x, f(+(x'', y'')))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(x, +(f(+(x'', y'')), z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(f(x), f(y)) -> +'(x, y)
+'(+(x, y), z) -> +'(y, z)
+'(f(x), +(f(y), z)) -> +'(x, y)

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))

three new Dependency Pairs are created:

+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(x), +(f(y), z)) -> +'(x, y)
+'(+(x, y), z) -> +'(y, z)
+'(f(x), f(y)) -> +'(x, y)

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(+(x, y), z) -> +'(y, z)

six new Dependency Pairs are created:

+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, f(x'')), f(y'')) -> +'(f(x''), f(y''))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(+(x, f(x'')), f(y'')) -> +'(f(x''), f(y''))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(x), +(f(y), z)) -> +'(x, y)
+'(f(x), f(y)) -> +'(x, y)
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(f(x), f(y)) -> +'(x, y)

11 new Dependency Pairs are created:

+'(f(f(x'')), f(f(y''))) -> +'(f(x''), f(y''))
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(+(x, f(x'')), f(y'')) -> +'(f(x''), f(y''))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(f(y''))) -> +'(f(x''), f(y''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(x), +(f(y), z)) -> +'(x, y)
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(f(x), +(f(y), z)) -> +'(x, y)

21 new Dependency Pairs are created:

+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), +(f(y'), z)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(f(y''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(+(f(y'''), z''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', f(x''''))), +(f(f(y'''')), z)) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', f(x''''))), +(f(+(f(y''''), z'''')), z)) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(f(y''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(+(f(y'''''), z''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(f(f(x''''))), +(f(f(f(y''''))), z)) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(f(f(x''''))), +(f(f(+(f(y''''), z''''))), z)) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(f(y'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(+(f(y'''''), z'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y'''))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(f(y''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(+(f(y''''''), z''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y'''))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(y'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(+(f(y'''''''), z'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

Dependency Pairs:

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(+(x, f(x'')), f(y'')) -> +'(f(x''), f(y''))

11 new Dependency Pairs are created:

+'(+(x, f(f(x''''))), f(f(y''''))) -> +'(f(f(x'''')), f(f(y'''')))
+'(+(x, f(f(x''''))), f(+(f(y''''), z''''))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(+(x, f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y''')) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(+(x, f(+(x'''', +(x'''''', y'''''')))), f(y'''')) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(+(x, f(+(x'''', f(x'''''')))), f(f(y''''''))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(+(x, f(+(x'''', f(x'''''')))), f(+(f(y''''''), z''''''))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(y'''')) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(y'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(+(f(y'''''''), z'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(y'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y'''))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(+(f(y''''''), z''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(f(y''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(+(f(y'''''), z'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(f(y'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), +(f(f(+(f(y''''), z''''))), z)) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(f(x''''))), +(f(f(f(y''''))), z)) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(+(f(y'''''), z''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(f(y''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', f(x''''))), +(f(+(f(y''''), z'''')), z)) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(+(f(y'''''''), z'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(y'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(y'''')) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(f(+(x'', f(x''''))), +(f(f(y'''')), z)) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(+(f(y'''), z''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(f(y''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(+(x, f(+(x'''', f(x'''''')))), f(+(f(y''''''), z''''''))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(+(x, f(+(x'''', f(x'''''')))), f(f(y''''''))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(+(x, f(+(x'''', +(x'''''', y'''''')))), f(y'''')) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(+(x, f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y''')) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(+(x, f(f(x''''))), f(+(f(y''''), z''''))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(+(x, f(f(x''''))), f(f(y''''))) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), +(f(y'), z)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(f(y''))) -> +'(f(x''), f(y''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(+(f(y'''''''), z'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(f(f(x'')), f(f(y''))) -> +'(f(x''), f(y''))

11 new Dependency Pairs are created:

+'(f(f(f(x''''))), f(f(f(y'''')))) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(f(f(x''''))), f(f(+(f(y''''), z'''')))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(f(y'''))) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(f(y''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(+(f(y'''''), z''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(f(f(+(x'''', f(x'''''')))), f(f(f(y'''''')))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', f(x'''''')))), f(f(+(f(y''''''), z'''''')))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(f(y''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(+(f(y'''''''), z''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(+(f(y'''''''), z'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y'''))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(+(f(y''''''), z''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(f(y''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(+(f(y'''''), z'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(f(y'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), +(f(f(+(f(y''''), z''''))), z)) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(+(f(y'''''''), z''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(f(y''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(f(f(f(x''''))), +(f(f(f(y''''))), z)) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(+(f(y'''''), z''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(f(y''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', f(x''''))), +(f(+(f(y''''), z'''')), z)) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(+(f(y'''''''), z'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(y'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(y'''')) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(+(x, f(+(x'''', f(x'''''')))), f(+(f(y''''''), z''''''))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(+(x, f(+(x'''', f(x'''''')))), f(f(y''''''))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(+(x, f(+(x'''', +(x'''''', y'''''')))), f(y'''')) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(+(x, f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y''')) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(+(x, f(f(x''''))), f(+(f(y''''), z''''))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(+(x'', f(x''''))), +(f(f(y'''')), z)) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(+(f(y'''), z''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(f(y''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(f(+(x'''', f(x'''''')))), f(f(+(f(y''''''), z'''''')))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), f(f(f(y'''''')))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(+(f(y'''''), z''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(f(y''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(f(y'''))) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), f(f(+(f(y''''), z'''')))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(f(x''''))), f(f(f(y'''')))) -> +'(f(f(x'''')), f(f(y'''')))
+'(+(x, f(f(x''''))), f(f(y''''))) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), +(f(y'), z)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(y'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

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

+'(f(f(f(x''''))), +(f(f(f(y''''))), z)) -> +'(f(f(x'''')), f(f(y'''')))

11 new Dependency Pairs are created:

+'(f(f(f(f(x'''''')))), +(f(f(f(f(y'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(f(y''''''))))
+'(f(f(f(f(x'''''')))), +(f(f(f(+(f(y''''''), z'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(+(f(y''''''), z''''''))))
+'(f(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(f(y'''''))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(f(y''''')))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(f(y''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(f(y'''''''))))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(+(f(y'''''''), z''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(+(f(y'''''''), z'''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', y''''''''))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', y'''''''')))), f(f(y'''''')))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(f(y'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(f(y''''''''))))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(+(f(y''''''''), z'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(+(f(y''''''''), z''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y'''''''''))))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y''''''''')))))), f(f(y'''''')))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(f(y''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(f(y'''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(+(f(y'''''''''), z''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(+(f(y'''''''''), z'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 9

                 ↳Polynomial Ordering

Dependency Pairs:

+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(+(f(y'''''''''), z''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(+(f(y'''''''''), z'''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(f(y''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(f(y'''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y'''''''''))))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y''''''''')))))), f(f(y'''''')))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(+(f(y''''''''), z'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(+(f(y''''''''), z''''''''))))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(f(y'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(f(y''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', y''''''''))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', y'''''''')))), f(f(y'''''')))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(+(f(y'''''''), z''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(+(f(y'''''''), z'''''''))))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(f(y''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(f(y'''''''))))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(+(f(y'''''''), z''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(f(y''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(f(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(f(y'''''))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(f(y''''')))
+'(f(f(f(f(x'''''')))), +(f(f(f(+(f(y''''''), z'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(+(f(y''''''), z''''''))))
+'(f(f(f(f(x'''''')))), +(f(f(f(f(y'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(f(y''''''))))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(y'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y'''))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(+(f(y''''''), z''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(f(y''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(+(f(y'''''), z'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(f(y'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), +(f(f(+(f(y''''), z''''))), z)) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(+(f(y'''''), z''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(f(y''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', f(x''''))), +(f(+(f(y''''), z'''')), z)) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(+(f(y'''''''), z'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(y'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(y'''')) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(+(x, f(+(x'''', f(x'''''')))), f(+(f(y''''''), z''''''))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(+(x, f(+(x'''', f(x'''''')))), f(f(y''''''))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(+(x, f(+(x'''', +(x'''''', y'''''')))), f(y'''')) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(+(x, f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y''')) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(+(x, f(f(x''''))), f(+(f(y''''), z''''))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(+(x'', f(x''''))), +(f(f(y'''')), z)) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(+(f(y'''), z''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(f(y''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(f(+(x'''', f(x'''''')))), f(f(+(f(y''''''), z'''''')))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), f(f(f(y'''''')))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(+(f(y'''''), z''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(f(y''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(f(y'''))) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), f(f(+(f(y''''), z'''')))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(f(x''''))), f(f(f(y'''')))) -> +'(f(f(x'''')), f(f(y'''')))
+'(+(x, f(f(x''''))), f(f(y''''))) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), +(f(y'), z)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(+(f(y'''''''), z'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(+(f(y'''''''''), z''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(+(f(y'''''''''), z'''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x''''''''''''))))))), +(f(f(f(f(y''''''''')))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', f(x'''''''''''')))))), f(f(f(y'''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y'''''''''))))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', +(x''''0'''''', +(x'''''''''''', y''''''''')))))), f(f(y'''''')))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(+(f(y''''''''), z'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(+(f(y''''''''), z''''''''))))
+'(f(f(f(+(x'''''', f(x''''''''))))), +(f(f(f(f(y'''''''')))), z)) -> +'(f(f(+(x'''''', f(x'''''''')))), f(f(f(y''''''''))))
+'(f(f(f(+(x'''''', +(x'''''''', y''''''''))))), +(f(f(f(y''''''))), z)) -> +'(f(f(+(x'''''', +(x'''''''', y'''''''')))), f(f(y'''''')))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(+(f(y'''''''), z''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(+(f(y'''''''), z'''''''))))
+'(f(f(f(+(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(f(y''''''')))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(f(y'''''''))))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(+(f(y'''''''), z''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(f(y''''''')))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(f(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(f(y'''''))), z)) -> +'(f(f(+(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(f(y''''')))
+'(f(f(f(f(x'''''')))), +(f(f(f(+(f(y''''''), z'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(+(f(y''''''), z''''''))))
+'(f(f(f(f(x'''''')))), +(f(f(f(f(y'''''')))), z)) -> +'(f(f(f(x''''''))), f(f(f(y''''''))))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(f(y'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y'''))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(+(f(y''''''), z''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), +(f(f(f(y''''''))), z)) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y'''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(+(f(y'''''), z'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), +(f(f(f(y'''''))), z)) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), +(f(f(+(f(y''''), z''''))), z)) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(+(f(y'''''), z''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), +(f(f(y''''')), z)) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(+(x'', f(x''''))), +(f(+(f(y''''), z'''')), z)) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(+(x'', f(x''''))), +(f(f(y'''')), z)) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(x'''', y'''')), y')
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(+(f(y'''), z''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), +(f(f(y''')), z)) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(f(+(x'', f(x''''))), f(+(f(y''''), z''''))) -> +'(+(x'', f(x'''')), +(f(y''''), z''''))
+'(f(f(+(x'''', f(x'''''')))), f(f(+(f(y''''''), z'''''')))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(f(f(+(x'''', f(x'''''')))), f(f(f(y'''''')))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(f(f(+(x'''', +(x'''''', y'''''')))), f(f(y''''))) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(+(f(y'''''), z''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(f(f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(f(y''''')))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), +(f(y'''''), z'''''))
+'(f(+(x'', +(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(+(x'', +(x'''', +(x''''0'', f(x'''''''')))), f(y'''''))
+'(f(+(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y')) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), y')
+'(f(f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(f(y'''))) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(f(f(f(x''''))), f(f(+(f(y''''), z'''')))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(f(f(f(x''''))), f(f(f(y'''')))) -> +'(f(f(x'''')), f(f(y'''')))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(+(x, +(x'', f(x'''))), +(f(y'), z')) -> +'(x, +(x'', +(f(+(x''', y')), z')))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(+(f(y'''), z'''))) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(f(+(x'', +(x''''0, f(x'''''')))), f(f(y'''))) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', f(x'''))), f(y')) -> +'(x, +(x'', f(+(x''', y'))))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), +(f(y'), z)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(f(x''), +(f(y''), z''))
+'(f(f(x'')), f(+(f(y''), z''))) -> +'(f(x''), +(f(y''), z''))
+'(f(+(x'', +(x''''0, +(x'''''', y''')))), f(y')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), y')
+'(f(f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), +(f(f(+(f(y'''''''), z'''''''))), z)) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))

Additionally, the following usable rules for innermost can be oriented:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 10

                 ↳Dependency Graph

Dependency Pairs:

+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(+(f(y'''''''), z'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(+(f(y'''''''), z''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', f(x'''''''''')))))), f(f(y'''''''))) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', f(x''''''''''))))), f(f(y''''''')))
+'(+(x, f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), f(y'''')) -> +'(f(+(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), f(y''''))
+'(+(x, f(+(x'''', f(x'''''')))), f(+(f(y''''''), z''''''))) -> +'(f(+(x'''', f(x''''''))), f(+(f(y''''''), z'''''')))
+'(+(x, f(+(x'''', f(x'''''')))), f(f(y''''''))) -> +'(f(+(x'''', f(x''''''))), f(f(y'''''')))
+'(+(x, f(+(x'''', +(x'''''', y'''''')))), f(y'''')) -> +'(f(+(x'''', +(x'''''', y''''''))), f(y''''))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(+(f(y'''''), z'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(+(f(y'''''), z''''')))
+'(+(x, f(+(x'''', +(x''''0'', f(x''''''''))))), f(f(y'''''))) -> +'(f(+(x'''', +(x''''0'', f(x'''''''')))), f(f(y''''')))
+'(+(x, f(+(x'''', +(x''''0'', +(x'''''''', y'''''))))), f(y''')) -> +'(f(+(x'''', +(x''''0'', +(x'''''''', y''''')))), f(y'''))
+'(+(x, f(f(x''''))), f(+(f(y''''), z''''))) -> +'(f(f(x'''')), f(+(f(y''''), z'''')))
+'(+(x, f(x'')), +(f(y''), z'')) -> +'(f(x''), +(f(y''), z''))
+'(+(x, f(f(x''''))), f(f(y''''))) -> +'(f(f(x'''')), f(f(y'''')))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))
+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 11

                 ↳Polynomial Ordering

Dependency Pairs:

+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

+'(+(x, +(x'', +(x''''0, f(x'''''')))), f(y''')) -> +'(+(x'', +(x''''0, f(x''''''))), f(y'''))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, +(x'', +(x''''0, f(x'''''')))), +(f(y'''), z''')) -> +'(+(x'', +(x''''0, f(x''''''))), +(f(y'''), z'''))

Additionally, the following usable rules for innermost can be oriented:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(f(x₁)) = 0

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 12

                 ↳Dependency Graph

Dependency Pair:

Rules:

+(+(x, y), z) -> +(x, +(y, z))
+(f(x), f(y)) -> f(+(x, y))
+(f(x), +(f(y), z)) -> +(f(+(x, y)), z)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

POL(+(x₁, x₂))	= x₁ + x₂
POL(f(x₁))	= 1 + x₁
POL(+'(x₁, x₂))	= 1 + x₁

POL(+(x₁, x₂))	= 1 + x₁ + x₂
POL(f(x₁))	= 0
POL(+'(x₁, x₂))	= 1 + x₁ + x₂