Termination Proof using AProVE

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

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

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

Rules:

+(*(x, y), *(x, z)) -> *(x, +(y, z))
+(+(x, y), z) -> +(x, +(y, z))
+(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)

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

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

Rules:

+(*(x, y), *(x, z)) -> *(x, +(y, z))
+(+(x, y), z) -> +(x, +(y, z))
+(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)

Strategy:

innermost

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

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

five new Dependency Pairs are created:

+'(*(x, *(x'0, y'')), *(x, *(x''', z''))) -> +'(*(x'0, y''), *(x''', z''))
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(*(x, *(x'0, y'')), *(x, +(*(x''', z''), u))) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', +(x'''', y''''))), *(x, z')) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, +(x'', *(x'''0, y''''))), *(x, +(*(x''''', z''''), u))) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))

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

Rules:

+(*(x, y), *(x, z)) -> *(x, +(y, z))
+(+(x, y), z) -> +(x, +(y, z))
+(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)

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)

nine new Dependency Pairs are created:

+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(x'', +(x'''', y'''')), z')
+'(+(x, +(x'', *(x'''0, y''''))), +(*(x''''', z''''), u)) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', *(x''''', z''''))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(+(x, *(x'', +(x'''', y''''))), *(x0', z'''')) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', +(*(x''''', z''''), u))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(+(x, *(x'', +(x'''', +(x'''''', y'''''')))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x'''''', y''''''))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', *(x'''0'', y'''''')))), *(x0', +(*(x''''''', z''''''), u))) -> +'(*(x'', +(x'''', *(x'''0'', y''''''))), *(x0', +(*(x''''''', z''''''), u)))

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:

+'(+(x, *(x'', +(x'''', *(x'''0'', y'''''')))), *(x0', +(*(x''''''', z''''''), u))) -> +'(*(x'', +(x'''', *(x'''0'', y''''''))), *(x0', +(*(x''''''', z''''''), u)))
+'(+(x, *(x'', +(x'''', +(x'''''', y'''''')))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x'''''', y''''''))), *(x0', z'''))
+'(*(x, *(x'0, y'')), *(x, +(*(x''', z''), u))) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', +(*(x''''', z''''), u))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(*(x, +(x'', +(x'''', y''''))), *(x, z')) -> +'(+(x'', +(x'''', y'''')), z')
+'(+(x, *(x'', +(x'''', y''''))), *(x0', z'''')) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', *(x''''', z''''))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(+(x, +(x'', *(x'''0, y''''))), +(*(x''''', z''''), u)) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(x'', +(x'''', y'''')), z')
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(*(x, *(x'0, y'')), *(x, *(x''', z''))) -> +'(*(x'0, y''), *(x''', z''))
+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(*(x, y), +(*(x, z), u)) -> +'(y, z)
+'(+(x, *(x'', y'')), +(*(x'', z''), u)) -> +'(x, +(*(x'', +(y'', z'')), u))
+'(*(x, +(x'', *(x'''0, y''''))), *(x, +(*(x''''', z''''), u))) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))

Rules:

+(*(x, y), *(x, z)) -> *(x, +(y, z))
+(+(x, y), z) -> +(x, +(y, z))
+(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)

Strategy:

innermost

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

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

16 new Dependency Pairs are created:

+'(*(x, *(x'0, y'')), +(*(x, +(*(x''', z''), u)), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', +(x'''', y''''))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, +(x'', *(x'''0, y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', *(x''''', z''''))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(*(x, *(x'', +(x'''', y''''))), +(*(x, *(x0', z'''')), u)) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', +(*(x''''', z''''), u))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(*(x, *(x'', +(x'''', +(x'''''', y'''''')))), +(*(x, *(x0', z''')), u)) -> +'(*(x'', +(x'''', +(x'''''', y''''''))), *(x0', z'''))
+'(*(x, *(x'', +(x'''', *(x'''0'', y'''''')))), +(*(x, *(x0', +(*(x''''''', z''''''), u))), u)) -> +'(*(x'', +(x'''', *(x'''0'', y''''''))), *(x0', +(*(x''''''', z''''''), u)))
+'(*(x, +(x'', *(x'0'', y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'0'', y'''')), +(*(x''''', z''''), u))
+'(*(x, +(x'', +(x'''', +(x'''''', y'''''')))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', +(x'''''', y''''''))), z')
+'(*(x, +(x'', +(x'''', *(x'''0'', y'''''')))), +(*(x, +(*(x''''''', z''''''), u)), u)) -> +'(+(x'', +(x'''', *(x'''0'', y''''''))), +(*(x''''''', z''''''), u))
+'(*(x, +(x'', *(x'0'', *(x'0'''', y'''''')))), +(*(x, *(x''''', *(x''''''', z''''''))), u)) -> +'(+(x'', *(x'0'', *(x'0'''', y''''''))), *(x''''', *(x''''''', z'''''')))
+'(*(x, +(x'', *(x'''', +(x'''''', y'''''')))), +(*(x, *(x0''', z'''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', y''''''))), *(x0''', z''''''))
+'(*(x, +(x'', *(x'0'', *(x'0'''', y'''''')))), +(*(x, *(x''''', +(*(x''''''', z''''''), u))), u)) -> +'(+(x'', *(x'0'', *(x'0'''', y''''''))), *(x''''', +(*(x''''''', z''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x'''''''', y''''''''))))), +(*(x, *(x0''', z''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x'''''''', y'''''''')))), *(x0''', z'''''))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x'''0'''', y''''''''))))), +(*(x, *(x0''', +(*(x''''''''', z''''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x'''0'''', y'''''''')))), *(x0''', +(*(x''''''''', z''''''''), u)))

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:

+'(*(x, +(x'', *(x'''', +(x'''''', *(x'''0'''', y''''''''))))), +(*(x, *(x0''', +(*(x''''''''', z''''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x'''0'''', y'''''''')))), *(x0''', +(*(x''''''''', z''''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x'''''''', y''''''''))))), +(*(x, *(x0''', z''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x'''''''', y'''''''')))), *(x0''', z'''''))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', +(*(x''''', z''''), u))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(*(x, +(x'', *(x'0'', *(x'0'''', y'''''')))), +(*(x, *(x''''', +(*(x''''''', z''''''), u))), u)) -> +'(+(x'', *(x'0'', *(x'0'''', y''''''))), *(x''''', +(*(x''''''', z''''''), u)))
+'(+(x, *(x'', +(x'''', +(x'''''', y'''''')))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x'''''', y''''''))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', y''''))), *(x0', z'''')) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, +(x'', *(x'''', +(x'''''', y'''''')))), +(*(x, *(x0''', z'''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', y''''''))), *(x0''', z''''''))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', *(x''''', z''''))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(*(x, +(x'', *(x'0'', *(x'0'''', y'''''')))), +(*(x, *(x''''', *(x''''''', z''''''))), u)) -> +'(+(x'', *(x'0'', *(x'0'''', y''''''))), *(x''''', *(x''''''', z'''''')))
+'(*(x, +(x'', +(x'''', *(x'''0'', y'''''')))), +(*(x, +(*(x''''''', z''''''), u)), u)) -> +'(+(x'', +(x'''', *(x'''0'', y''''''))), +(*(x''''''', z''''''), u))
+'(*(x, +(x'', +(x'''', +(x'''''', y'''''')))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', +(x'''''', y''''''))), z')
+'(*(x, +(x'', *(x'0'', y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'0'', y'''')), +(*(x''''', z''''), u))
+'(*(x, *(x'', +(x'''', *(x'''0'', y'''''')))), +(*(x, *(x0', +(*(x''''''', z''''''), u))), u)) -> +'(*(x'', +(x'''', *(x'''0'', y''''''))), *(x0', +(*(x''''''', z''''''), u)))
+'(*(x, *(x'', +(x'''', +(x'''''', y'''''')))), +(*(x, *(x0', z''')), u)) -> +'(*(x'', +(x'''', +(x'''''', y''''''))), *(x0', z'''))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', +(*(x''''', z''''), u))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(*(x, +(x'', *(x'''0, y''''))), *(x, +(*(x''''', z''''), u))) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(*(x, *(x'', +(x'''', y''''))), +(*(x, *(x0', z'''')), u)) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', *(x''''', z''''))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(*(x, +(x'', *(x'''0, y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(+(x, +(x'', *(x'''0, y''''))), +(*(x''''', z''''), u)) -> +'(+(x'', *(x'''0, y'''')), +(*(x''''', z''''), u))
+'(+(x, +(x'', +(x'''', y''''))), z') -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, +(x'', +(x'''', y''''))), *(x, z')) -> +'(+(x'', +(x'''', y'''')), z')
+'(+(x, *(x'', y'')), +(*(x'', z''), u)) -> +'(x, +(*(x'', +(y'', z'')), u))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', +(x'''', y''''))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, *(x'0, y'')), +(*(x, +(*(x''', z''), u)), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, *(x'0, y'')), *(x, +(*(x''', z''), u))) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, *(x'0, y'')), *(x, *(x''', z''))) -> +'(*(x'0, y''), *(x''', z''))
+'(+(x, +(x'', y'')), z'') -> +'(x, +(x'', +(y'', z'')))
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(+(x, *(x'', +(x'''', *(x'''0'', y'''''')))), *(x0', +(*(x''''''', z''''''), u))) -> +'(*(x'', +(x'''', *(x'''0'', y''''''))), *(x0', +(*(x''''''', z''''''), u)))

Rules:

+(*(x, y), *(x, z)) -> *(x, +(y, z))
+(+(x, y), z) -> +(x, +(y, z))
+(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)

Strategy:

innermost

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