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:09 minutes