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

             ↳Forward Instantiation 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 Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

four 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'''', y''''))), z') -> +'(+(x'', +(x'''', y'''')), z')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(x'', +(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'')
+'(f(x), +(f(y), z)) -> +'(x, y)
+'(f(x), f(y)) -> +'(x, y)
+'(+(x, +(x'', y'')), z'') -> +'(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

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)

six 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'''', 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'''''', y'''''')))), f(y')) -> +'(+(x'', +(x'''', +(x'''''', y''''''))), y')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

+'(f(+(x'', +(x'''', +(x'''''', y'''''')))), f(y')) -> +'(+(x'', +(x'''', +(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''''))
+'(f(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(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, f(x'')), f(y'')) -> +'(f(x''), f(y''))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(x), +(f(y), z)) -> +'(x, y)
+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(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

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)

11 new Dependency Pairs are created:

+'(f(f(x'')), +(f(+(f(y''), z'')), z)) -> +'(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'''''', y'''''')))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(x'''''', y''''''))), y')
+'(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'''''', 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'''''''', y''''''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(x'''''''', y'''''''')))), f(y'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

+'(f(f(+(x'''', +(x'''''', +(x'''''''', y''''''''))))), +(f(f(y''')), z)) -> +'(f(+(x'''', +(x'''''', +(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(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'''''', y'''''')))), +(f(y'), z)) -> +'(+(x'', +(x'''', +(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''''))
+'(+(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(+(x'', f(x''''))), f(f(y''''))) -> +'(+(x'', f(x'''')), f(y''''))
+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(x'', +(x'''', y'''')), z')
+'(f(+(x'', +(x'''', y''''))), f(y')) -> +'(+(x'', +(x'''', y'''')), y')
+'(+(x, f(x'')), f(y'')) -> +'(f(x''), f(y''))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(f(+(x'', +(x'''', y''''))), +(f(y'), z)) -> +'(+(x'', +(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'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(f(+(x'', +(x'''', +(x'''''', y'''''')))), f(y')) -> +'(+(x'', +(x'''', +(x'''''', y''''''))), 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

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