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

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

:'(:(:(:(C, x), y), z), u) -> :'(:(x, z), :(:(:(x, y), z), u))
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(x, y)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, z), :(:(:(x, y), z), u))


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))


Strategy:

innermost




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

:'(:(:(:(C, x), y), z), u) -> :'(:(x, z), :(:(:(x, y), z), u))
four new Dependency Pairs are created:

:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(:(:(C, x''), y''), z'''), y), z''), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(:(C, x''), y''), z''), z), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Rewriting Transformation


Dependency Pairs:

:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(:(C, x''), y''), z''), z), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(:(:(C, x''), y''), z'''), y), z''), u))
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, x), y), z), u) -> :'(x, y)


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))


Strategy:

innermost




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

:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(:(:(C, x''), y''), z'''), y), z''), u))
one new Dependency Pair is created:

:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(x'', z'''), :(:(:(x'', y''), z'''), y)), z''), u))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(x'', z'''), :(:(:(x'', y''), z'''), y)), z''), u))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(:(C, x''), y''), z''), z), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))


Strategy:

innermost




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

:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(:(C, x''), y''), z''), z), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))
one new Dependency Pair is created:

:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(x'', z''), :(:(:(x'', y''), z''), z)), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(x'', z''), :(:(:(x'', y''), z''), z)), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, x), y), z), u) -> :'(x, z)
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(x'', z'''), :(:(:(x'', y''), z'''), y)), z''), u))


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(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

:'(:(:(:(C, x), y), z), u) -> :'(x, z)
five new Dependency Pairs are created:

:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(:(C, x''), y''), z'''), z'')
:'(:(:(:(C, :(:(:(C, :(C, x'''')), y''''), z'''')), y), z'), u) -> :'(:(:(:(C, :(C, x'''')), y''''), z''''), z')
:'(:(:(:(C, :(:(:(C, :(:(C, x''''), y'''')), y0''), z'''')), y), z'), u) -> :'(:(:(:(C, :(:(C, x''''), y'''')), y0''), z''''), z')
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0')), y), z'), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0'), z')
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0)), y), z''), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0), z'')

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0)), y), z''), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0), z'')
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0')), y), z'), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0'), z')
:'(:(:(:(C, :(:(:(C, :(:(C, x''''), y'''')), y0''), z'''')), y), z'), u) -> :'(:(:(:(C, :(:(C, x''''), y'''')), y0''), z''''), z')
:'(:(:(:(C, :(:(:(C, :(C, x'''')), y''''), z'''')), y), z'), u) -> :'(:(:(:(C, :(C, x'''')), y''''), z''''), z')
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(:(C, x''), y''), z'''), z'')
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(x'', z'''), :(:(:(x'', y''), z'''), y)), z''), u))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, x), y), z), u) -> :'(x, y)
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(x'', z''), :(:(:(x'', y''), z''), z)), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(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

:'(:(:(:(C, x), y), z), u) -> :'(x, y)
nine new Dependency Pairs are created:

:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(C, x''), y''), z''), y0)
:'(:(:(:(C, :(:(:(C, :(C, x'''')), y''''), z'''')), y'), z), u) -> :'(:(:(:(C, :(C, x'''')), y''''), z''''), y')
:'(:(:(:(C, :(:(:(C, :(:(C, x''''), y'''')), y0''), z'''')), y'), z), u) -> :'(:(:(:(C, :(:(C, x''''), y'''')), y0''), z''''), y')
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0'), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'')), y'), z), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z''), y')
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(C, x'''''')), y''''''), z'''''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(C, x'''''')), y''''''), z'''''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(C, x''''''), y'''''')), y0''''), z'''''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(C, x''''''), y'''''')), y0''''), z'''''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z''''''')), y''''), z''0''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z''''''')), y''''), z''0''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z'''''')), y0''''), z'0'')), y''), z'''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z'''''')), y0''''), z'0'')), y''), z''''), y0)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Rw
             ...
               →DP Problem 6
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z'''''')), y0''''), z'0'')), y''), z'''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z'''''')), y0''''), z'0'')), y''), z''''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z''''''')), y''''), z''0''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(:(C, x''''''), y''''''), z''''''')), y''''), z''0''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(:(C, x''''''), y'''''')), y0''''), z'''''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(:(C, x''''''), y'''''')), y0''''), z'''''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, :(C, x'''''')), y''''''), z'''''')), y''), z''')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, :(C, x'''''')), y''''''), z'''''')), y''), z'''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'')), y'), z), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z''), y')
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0')), y0), z), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0'), y0)
:'(:(:(:(C, :(:(:(C, :(:(C, x''''), y'''')), y0''), z'''')), y'), z), u) -> :'(:(:(:(C, :(:(C, x''''), y'''')), y0''), z''''), y')
:'(:(:(:(C, :(:(:(C, :(C, x'''')), y''''), z'''')), y'), z), u) -> :'(:(:(:(C, :(C, x'''')), y''''), z''''), y')
:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(:(C, x''), y''), z''), y0)
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0')), y), z'), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z''''')), y''), z''0'), z')
:'(:(:(:(C, :(:(:(C, :(:(C, x''''), y'''')), y0''), z'''')), y), z'), u) -> :'(:(:(:(C, :(:(C, x''''), y'''')), y0''), z''''), z')
:'(:(:(:(C, :(:(:(C, :(C, x'''')), y''''), z'''')), y), z'), u) -> :'(:(:(:(C, :(C, x'''')), y''''), z''''), z')
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(:(C, x''), y''), z'''), z'')
:'(:(:(:(C, :(:(:(C, x''), y''), z'')), y0), z), u) -> :'(:(:(x'', z''), :(:(:(x'', y''), z''), z)), :(:(:(:(x'', z''), :(:(:(x'', y''), z''), y0)), z), u))
:'(:(:(:(C, :(:(:(C, x''), y''), z''')), y), z''), u) -> :'(:(:(x'', z'''), :(:(:(x'', y''), z'''), z'')), :(:(:(:(x'', z'''), :(:(:(x'', y''), z'''), y)), z''), u))
:'(:(:(:(C, :(:(C, x''), y'')), y0), z''), u) -> :'(:(:(:(C, x''), y''), z''), :(:(:(x'', y0), :(:(:(x'', y''), y0), z'')), u))
:'(:(:(:(C, :(C, x'')), y''), z''), u'') -> :'(:(:(C, x''), z''), :(:(x'', z''), :(:(:(x'', y''), z''), u'')))
:'(:(:(:(C, x), y), z), u) -> :'(:(x, y), z)
:'(:(:(:(C, x), y), z), u) -> :'(:(:(x, y), z), u)
:'(:(:(:(C, :(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0)), y), z''), u) -> :'(:(:(:(C, :(:(:(C, x''''), y''''), z'''')), y0''), z'0), z'')


Rule:


:(:(:(:(C, x), y), z), u) -> :(:(x, z), :(:(:(x, y), z), u))


Strategy:

innermost



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