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
                 ↳Remaining Obligation(s)




The following remains to be proven:
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



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