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. 



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


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



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Narrowing 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 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'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Narrowing Transformation


Dependency Pairs:

+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', *(x''', y'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(*(x, y), +(*(x, z), u)) -> +'(y, z)
+'(+(x, y), z) -> +'(y, z)
+'(*(x, y), *(x, z)) -> +'(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 Narrowing SCC transformation can be performed.
As a result of transforming the rule

+'(+(x, *(x'', y'')), +(*(x'', z''), u)) -> +'(x, +(*(x'', +(y'', z'')), u))
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Forward Instantiation Transformation


Dependency Pairs:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Forward Instantiation Transformation


Dependency Pairs:

+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), *(x0', +(*(x''0''', z'''''''), u))) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x'''0''', z'''''), u))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', *(x'''0''', z'''''))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', z''''')))
+'(+(x, *(x'0, *(x'0'', y''''))), *(x''', +(*(x''''', z''''), u))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', +(*(x''''', z''''), u)))
+'(+(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, *(x'''''', y''')))), +(*(x''0', +(*(x'''0', z'''), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), *(x, +(*(x''0', z'''''), u))) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', *(x'''0', z''')), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', +(x''', y'))), +(*(x'', z'''), u)) -> +'(x, +(*(x'', +(x''', +(y', z'''))), u))
+'(+(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x''0', z'''''), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, +(*(x'''0', z'''), u))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', *(x''', z')), u)) -> +'(x, +(*(x'', *(x''', +(y', z'))), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', *(x'''0', z''')), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x'''0', z'''), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x'''0', z''')) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), *(x, z')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, *(x'''0', z'''))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(*(x, *(x'0, y'')), *(x, +(*(x''', z''), u))) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(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'', *(x''', y'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(*(x, y), +(*(x, z), u)) -> +'(y, z)
+'(+(x, *(x'', *(x''', y'))), +(*(x'', +(*(x''', z'), u)), u)) -> +'(x, +(*(x'', +(*(x''', +(y', z')), u)), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', +(*(x'''0', z'''), u)), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), 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)
33 new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Forward Instantiation Transformation


Dependency Pairs:

+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', z'''''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', z'''''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x'''0''''', z'''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x'''0''''', z'''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', z''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', z'''''))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', *(x'''0''''', z'''''''))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', *(x'''0''''', 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''''0'', +(x'''''''', y'''''))))), *(x0', +(*(x''0''', z'''''''), u))) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x'''0''', z'''''), u))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', *(x'''0''', z'''''))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', 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'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', +(*(x'''0''', z'''''), u)), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', +(*(x'''0''', z'''''), u)), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, +(*(x''0''', z'''''''), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), +(*(x''0''', z'''''''), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', *(x'''0''', z''''')), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', *(x'''0''', z''''')), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x'''0''', z'''''), u)), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), +(*(x'''0''', z'''''), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), z')
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x'''0''', z''''')), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x'''0''', z'''''))
+'(*(x, +(x'', *(x'0'', y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'0'', y'''')), +(*(x''''', z''''), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', +(*(x'''0', z'''), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', +(x'''', y''''))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', z'''''''), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', *(x'''0''', z''''')), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x'''0''', z'''''), u))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', z''')), u)) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', *(x'''0''', z'''''))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', 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'''', 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, *(x'''''', y''')))), +(*(x, +(*(x''0', +(*(x'''0', z'''), u)), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x, +(*(x''0', z'''''), u)), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x, +(*(x''0', *(x'''0', z''')), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', +(*(x''', z'), u)), u)) -> +'(x, +(*(x'', +(*(x''', +(y', z')), u)), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', +(*(x'''0', z'''), u)), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), *(x, +(*(x''0', z'''''), u))) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(+(x, *(x'', +(x''', y'))), +(*(x'', z'''), u)) -> +'(x, +(*(x'', +(x''', +(y', z'''))), u))
+'(+(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x''0', z'''''), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, +(*(x'''0', z'''), u)), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), +(*(x, z'), u)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', *(x'''0', z''')), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', *(x''', z')), u)) -> +'(x, +(*(x'', *(x''', +(y', z'))), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', *(x'''0', z''')), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, +(*(x'''0', z'''), u))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x'''0', z'''), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x'''0', z''')) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), *(x, z')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, *(x'''0', z'''))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, *(x'''0', z''')), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', 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'', *(x''', y'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), 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, *(x'0, y'')), *(x, *(x''', z''))) -> +'(*(x'0, y''), *(x''', z''))
nine new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Forward Instantiation Transformation


Dependency Pairs:

+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', z'''''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', z'''''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x'''0''''', z'''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x'''0''''', z'''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', z''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', z'''''))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', *(x'''0''''', z'''''''))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', *(x'''0''''', 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''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), *(x0', +(*(x''0''', z'''''''), u))) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x'''0''', z'''''), u))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', *(x'''0''', z'''''))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', 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'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', +(*(x'''0''', z'''''), u)), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', +(*(x'''0''', z'''''), u)), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, +(*(x''0''', z'''''''), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), +(*(x''0''', z'''''''), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', *(x'''0''', z''''')), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', *(x'''0''', z''''')), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x'''0''', z'''''), u)), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), +(*(x'''0''', z'''''), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), z')
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x'''0''', z''''')), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x'''0''', z'''''))
+'(*(x, +(x'', *(x'0'', y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'0'', y'''')), +(*(x''''', z''''), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', +(*(x'''0', z'''), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', +(x'''', y''''))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', z'''''''), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', *(x'''0''', z''''')), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x'''0''', z'''''), u))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', z''')), u)) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', *(x'''0''', z'''''))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', 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'''', y''''))), +(*(x, *(x0', z'''')), u)) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', +(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', z'''''''), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', +(x'''''''', y''''')))), *(x''''', +(*(x''0''', z'''''''), u)))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', *(x'''0''', z''''')), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x'''0''', z'''''), u)))) -> +'(*(x'0', +(x'''''', +(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x'''0''', z'''''), u)))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', +(x'''''''', y'''''))))), *(x, *(x''''', z''''))) -> +'(*(x'0', +(x'''''', +(x''''0'', +(x'''''''', y''''')))), *(x''''', z''''))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', *(x'''0''', z''''')))) -> +'(*(x'0', +(x'''''', +(x''''0'', *(x'''''''', y''''')))), *(x''''', *(x'''0''', z''''')))
+'(*(x, *(x'00, *(x'0'', y''''))), *(x, *(x'''0, +(*(x''''', z''''), u)))) -> +'(*(x'00, *(x'0'', y'''')), *(x'''0, +(*(x''''', z''''), u)))
+'(*(x, *(x'0', +(x'''''', y''''))), *(x, *(x''''', z''''))) -> +'(*(x'0', +(x'''''', y'''')), *(x''''', z''''))
+'(*(x, *(x'00, *(x'0'', y''''))), *(x, *(x'''0, *(x''''', z'''')))) -> +'(*(x'00, *(x'0'', y'''')), *(x'''0, *(x''''', z'''')))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', *(x''''', z''''))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x, +(*(x''0', +(*(x'''0', z'''), u)), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x, +(*(x''0', z'''''), u)), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x, +(*(x''0', *(x'''0', z''')), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', +(*(x''', z'), u)), u)) -> +'(x, +(*(x'', +(*(x''', +(y', z')), u)), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', +(*(x'''0', z'''), u)), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), *(x, +(*(x''0', z'''''), u))) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(+(x, *(x'', +(x''', y'))), +(*(x'', z'''), u)) -> +'(x, +(*(x'', +(x''', +(y', z'''))), u))
+'(+(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x''0', z'''''), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, +(*(x'''0', z'''), u)), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), +(*(x, z'), u)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', *(x'''0', z''')), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', *(x''', z')), u)) -> +'(x, +(*(x'', *(x''', +(y', z'))), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', *(x'''0', z''')), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, +(*(x'''0', z'''), u))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x'''0', z'''), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x'''0', z''')) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), *(x, z')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, *(x'''0', z'''))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, *(x'''0', z''')), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', 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'', *(x''', y'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(+(x, *(x'', +(x'''', y''''))), *(x0', z'''')) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), 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, *(x'0, *(x'0'', y''''))), *(x''', *(x''''', z''''))) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
nine new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 9
                 ↳Forward Instantiation Transformation


Dependency Pairs:

+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', *(x'''0''''', z''''''')), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x'''0''''', z'''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', +(*(x'''0''''', z'''''''), u)))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', z''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', z'''''))
+'(*(x, +(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y''''''')))))), +(*(x, *(x0''', *(x'''0''''', z'''''''))), u)) -> +'(+(x'', *(x'''', +(x'''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x0''', *(x'''0''''', 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''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), *(x0', +(*(x''0''', z'''''''), u))) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(+(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u))) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', +(*(x'''0''', z'''''), u))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(+(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), *(x0', z''')) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(+(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), *(x0', *(x'''0''', z'''''))) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', z''''')))
+'(*(x, +(x'', *(x'''', +(x'''''', y'''''')))), +(*(x, *(x0''', z'''''')), u)) -> +'(+(x'', *(x'''', +(x'''''', y''''''))), *(x0''', z''''''))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', *(x'''''''''', y''''''')))))), *(x'''', *(x'''''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u)))) -> +'(*(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x'''', *(x'''''', +(*(x''0''''', +(*(x'''0''''', z'''''''), u)), u))))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', +(x'''''''''', y''''''')))))), *(x'''', *(x'''''', +(*(x''0''''', z'''''''''), u)))) -> +'(*(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', +(x'''''''''', y'''''''))))), *(x'''', *(x'''''', +(*(x''0''''', z'''''''''), u))))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', *(x'''''''''', y''''''')))))), *(x'''', *(x'''''', +(*(x''0''''', *(x'''0''''', z''''''')), u)))) -> +'(*(x'0', *(x'0'''', +(x'''''''', *(x''''0'''', *(x'''''''''', y'''''''))))), *(x'''', *(x'''''', +(*(x''0''''', *(x'''0''''', z''''''')), u))))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', *(x'''''''''', y''''''')))))), *(x'''', *(x'''''', +(*(x'''0''''', z'''''''), u)))) -> +'(*(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x'''', *(x'''''', +(*(x'''0''''', z'''''''), u))))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', +(x'''''''''', y''''''')))))), *(x'''', *(x'''''', z''''''))) -> +'(*(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', +(x'''''''''', y'''''''))))), *(x'''', *(x'''''', z'''''')))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', *(x'''''''''', y''''''')))))), *(x'''', *(x'''''', *(x'''0''''', z''''''')))) -> +'(*(x'0', *(x'0'''', +(x'''''''', +(x''''0'''', *(x'''''''''', y'''''''))))), *(x'''', *(x'''''', *(x'''0''''', z'''''''))))
+'(+(x, *(x'0', *(x'0'''', *(x'0''''', y'''''')))), *(x'''', *(x'''''0, +(*(x''''''', z''''''), u)))) -> +'(*(x'0', *(x'0'''', *(x'0''''', y''''''))), *(x'''', *(x'''''0, +(*(x''''''', z''''''), u))))
+'(+(x, *(x'0', *(x'0'''', +(x'''''''', y'''''')))), *(x'''', *(x'''''', z''''''))) -> +'(*(x'0', *(x'0'''', +(x'''''''', y''''''))), *(x'''', *(x'''''', z'''''')))
+'(+(x, *(x'0', *(x'0'''', *(x'0''''', y'''''')))), *(x'''', *(x'''''0, *(x''''''', z'''''')))) -> +'(*(x'0', *(x'0'''', *(x'0''''', y''''''))), *(x'''', *(x'''''0, *(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'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', +(*(x'''0''', z'''''), u)), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', +(*(x'''0''', z'''''), u)), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, +(*(x''0''', z'''''''), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), +(*(x''0''', z'''''''), u))
+'(*(x, +(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x''0''', *(x'''0''', z''''')), u)), u)) -> +'(+(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), +(*(x''0''', *(x'''0''', z''''')), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, +(*(x'''0''', z'''''), u)), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), +(*(x'''0''', z'''''), u))
+'(*(x, +(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), z')
+'(*(x, +(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x'''0''', z''''')), u)) -> +'(+(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x'''0''', z'''''))
+'(*(x, +(x'', *(x'0'', y''''))), +(*(x, +(*(x''''', z''''), u)), u)) -> +'(+(x'', *(x'0'', y'''')), +(*(x''''', z''''), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', +(*(x'''0', z'''), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', +(x'''', y''''))), +(*(x, z'), u)) -> +'(+(x'', +(x'''', y'''')), z')
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', z'''''''), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', +(x'''''''', y''''')))), *(x0', +(*(x''0''', z'''''''), u)))
+'(*(x, *(x'', +(x'''', *(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x''0''', *(x'''0''', z''''')), u))), u)) -> +'(*(x'', +(x'''', *(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', +(*(x'''0''', z'''''), u))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', +(*(x'''0''', z'''''), u)))
+'(*(x, *(x'', +(x'''', +(x''''0'', +(x'''''''', y'''''))))), +(*(x, *(x0', z''')), u)) -> +'(*(x'', +(x'''', +(x''''0'', +(x'''''''', y''''')))), *(x0', z'''))
+'(*(x, *(x'', +(x'''', +(x''''0'', *(x'''''''', y'''''))))), +(*(x, *(x0', *(x'''0''', z'''''))), u)) -> +'(*(x'', +(x'''', +(x''''0'', *(x'''''''', y''''')))), *(x0', *(x'''0''', 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'''', y''''))), +(*(x, *(x0', z'''')), u)) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x''0''', +(*(x'''0''', z'''''), u)), u)))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', +(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', z'''''''), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', +(x'''''''', y''''')))), *(x''''', +(*(x''0''', z'''''''), u)))
+'(*(x, *(x'0', +(x'''''', *(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x''0''', *(x'''0''', z''''')), u)))) -> +'(*(x'0', +(x'''''', *(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x''0''', *(x'''0''', z''''')), u)))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', +(*(x'''0''', z'''''), u)))) -> +'(*(x'0', +(x'''''', +(x''''0'', *(x'''''''', y''''')))), *(x''''', +(*(x'''0''', z'''''), u)))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', +(x'''''''', y'''''))))), *(x, *(x''''', z''''))) -> +'(*(x'0', +(x'''''', +(x''''0'', +(x'''''''', y''''')))), *(x''''', z''''))
+'(*(x, *(x'0', +(x'''''', +(x''''0'', *(x'''''''', y'''''))))), *(x, *(x''''', *(x'''0''', z''''')))) -> +'(*(x'0', +(x'''''', +(x''''0'', *(x'''''''', y''''')))), *(x''''', *(x'''0''', z''''')))
+'(*(x, *(x'00, *(x'0'', y''''))), *(x, *(x'''0, +(*(x''''', z''''), u)))) -> +'(*(x'00, *(x'0'', y'''')), *(x'''0, +(*(x''''', z''''), u)))
+'(*(x, *(x'0', +(x'''''', y''''))), *(x, *(x''''', z''''))) -> +'(*(x'0', +(x'''''', y'''')), *(x''''', z''''))
+'(*(x, *(x'00, *(x'0'', y''''))), *(x, *(x'''0, *(x''''', z'''')))) -> +'(*(x'00, *(x'0'', y'''')), *(x'''0, *(x''''', z'''')))
+'(*(x, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', *(x''''', z''''))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x, +(*(x''0', +(*(x'''0', z'''), u)), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x, +(*(x''0', z'''''), u)), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x, +(*(x''0', *(x'''0', z''')), u)), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', +(*(x''', z'), u)), u)) -> +'(x, +(*(x'', +(*(x''', +(y', z')), u)), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', +(*(x'''0', z'''), u)), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', +(*(x'''0', z'''), u)), u))
+'(*(x, +(x'', *(x''''0, +(x'''''', y''')))), *(x, +(*(x''0', z'''''), u))) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(+(x, *(x'', +(x''', y'))), +(*(x'', z'''), u)) -> +'(x, +(*(x'', +(x''', +(y', z'''))), u))
+'(+(x, +(x'', *(x''''0, +(x'''''', y''')))), +(*(x''0', z'''''), u)) -> +'(+(x'', *(x''''0, +(x'''''', y'''))), +(*(x''0', z'''''), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, +(*(x'''0', z'''), u)), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), +(*(x, z'), u)) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, *(x'0, y'')), +(*(x''', z''), u)) -> +'(*(x'0, y''), +(*(x''', z''), u))
+'(*(x, +(x'', *(x''''0, *(x'''''', y''')))), *(x, +(*(x''0', *(x'''0', z''')), u))) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(+(x, *(x'', *(x''', y'))), +(*(x'', *(x''', z')), u)) -> +'(x, +(*(x'', *(x''', +(y', z'))), u))
+'(+(x, +(x'', *(x''''0, *(x'''''', y''')))), +(*(x''0', *(x'''0', z''')), u)) -> +'(+(x'', *(x''''0, *(x'''''', y'''))), +(*(x''0', *(x'''0', z''')), u))
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, +(*(x'''0', z'''), u))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', *(x''', y'))), +(*(x''', z'), u)) -> +'(x, +(x'', +(*(x''', +(y', z')), u)))
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x'''0', z'''), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), +(*(x'''0', z'''), u))
+'(+(x, +(x'', +(x''''0, +(x'''''', y''')))), z') -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(+(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x'''0', z''')) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(*(x, +(x'', +(x''''0, +(x'''''', y''')))), *(x, z')) -> +'(+(x'', +(x''''0, +(x'''''', y'''))), z')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), *(x, *(x'''0', z'''))) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', z'''))
+'(+(x, +(x'', +(x''', y'))), z''') -> +'(x, +(x'', +(x''', +(y', z'''))))
+'(+(x, +(x'', y'')), z'') -> +'(+(x'', y''), z'')
+'(*(x, +(x'', +(x''''0, *(x'''''', y''')))), +(*(x, *(x'''0', z''')), u)) -> +'(+(x'', +(x''''0, *(x'''''', y'''))), *(x'''0', 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'', *(x''', y'))), *(x''', z')) -> +'(x, +(x'', *(x''', +(y', z'))))
+'(*(x, +(x'', y'')), *(x, z'')) -> +'(+(x'', y''), z'')
+'(+(x, *(x'', +(x'''', y''''))), *(x0', z'''')) -> +'(*(x'', +(x'''', y'''')), *(x0', z''''))
+'(*(x, +(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y''''''')))))), +(*(x, *(x0''', +(*(x''0''''', z'''''''''), u))), u)) -> +'(+(x'', *(x'''', +(x'''''', *(x''''0'''', +(x'''''''''', y'''''''))))), *(x0''', +(*(x''0''''', 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, *(x'0, *(x'0'', y''''))), +(*(x, *(x''', *(x''''', z''''))), u)) -> +'(*(x'0, *(x'0'', y'''')), *(x''', *(x''''', z'''')))
nine new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 10
                 ↳Polynomial Ordering


Dependency Pairs:

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




The following dependency pairs can be strictly oriented:

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


Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*(x1, x2))=  1 + x2  
  POL(+(x1, x2))=  x1 + x2  
  POL(u)=  0  
  POL(+'(x1, x2))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 11
                 ↳Dependency Graph


Dependency Pairs:

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




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


   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 12
                 ↳Polynomial Ordering


Dependency Pairs:

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




The following dependency pairs can be strictly oriented:

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


Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(*(x1, x2))=  0  
  POL(+(x1, x2))=  1 + x1 + x2  
  POL(u)=  0  
  POL(+'(x1, x2))=  1 + x1  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 13
                 ↳Dependency Graph


Dependency Pair:


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




Using the Dependency Graph resulted in no new DP problems.

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