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