Term Rewriting System R:
[x, y, z]
if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

Termination of R to be shown.

`   R`
`     ↳Dependency Pair Analysis`

R contains the following Dependency Pairs:

IF(if(x, y, z), u, v) -> IF(x, if(y, u, v), if(z, u, v))
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, y, z), u, v) -> IF(z, u, v)

Furthermore, R contains one SCC.

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Narrowing Transformation`

Dependency Pairs:

IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, y, z), u, v) -> IF(x, if(y, u, v), if(z, u, v))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

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

IF(if(x, y, z), u, v) -> IF(x, if(y, u, v), if(z, u, v))
six new Dependency Pairs are created:

IF(if(x, true, z), u, v) -> IF(x, u, if(z, u, v))
IF(if(x, false, z), u, v) -> IF(x, v, if(z, u, v))
IF(if(x, if(x'', y'', z''), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(z, u, v))
IF(if(x, y, true), u, v) -> IF(x, if(y, u, v), u)
IF(if(x, y, false), u, v) -> IF(x, if(y, u, v), v)
IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))

The transformation is resulting in one new DP problem:

`   R`
`     ↳DPs`
`       →DP Problem 1`
`         ↳Nar`
`           →DP Problem 2`
`             ↳Narrowing Transformation`

Dependency Pairs:

IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, y, false), u, v) -> IF(x, if(y, u, v), v)
IF(if(x, if(x'', y'', z''), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(z, u, v))
IF(if(x, true, z), u, v) -> IF(x, u, if(z, u, v))
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, y, z), u, v) -> IF(z, u, v)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

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

IF(if(x, true, z), u, v) -> IF(x, u, if(z, u, v))
three new Dependency Pairs are created:

IF(if(x, true, true), u, v) -> IF(x, u, u)
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))

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:

IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, y, false), u, v) -> IF(x, if(y, u, v), v)
IF(if(x, if(x'', y'', z''), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(z, u, v))
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

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

IF(if(x, if(x'', y'', z''), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(z, u, v))
12 new Dependency Pairs are created:

IF(if(x, if(true, y''', z'''), z), u, v) -> IF(x, if(y''', u, v), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(x'', true, z''), z), u, v) -> IF(x, if(x'', u, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', y'', true), z), u, v) -> IF(x, if(x'', if(y'', u, v), u), if(z, u, v))
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', y'', z''), true), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), u)
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))

The transformation is resulting in one new DP problem:

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

Dependency Pairs:

IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', y'', true), z), u, v) -> IF(x, if(x'', if(y'', u, v), u), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', true, z''), z), u, v) -> IF(x, if(x'', u, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(true, y''', z'''), z), u, v) -> IF(x, if(y''', u, v), if(z, u, v))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, y, false), u, v) -> IF(x, if(y, u, v), v)
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

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

IF(if(x, y, false), u, v) -> IF(x, if(y, u, v), v)
three new Dependency Pairs are created:

IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, false, false), u, v) -> IF(x, v, v)
IF(if(x, if(x'', y'', z'), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z', u, v)), v)

The transformation is resulting in one new DP problem:

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

Dependency Pairs:

IF(if(x, if(x'', y'', z'), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z', u, v)), v)
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', y'', true), z), u, v) -> IF(x, if(x'', if(y'', u, v), u), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', true, z''), z), u, v) -> IF(x, if(x'', u, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(true, y''', z'''), z), u, v) -> IF(x, if(y''', u, v), if(z, u, v))
IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

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

IF(if(x, y, if(x'', y'', z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(z'', u, v)))
12 new Dependency Pairs are created:

IF(if(x, true, if(x'', y'', z'')), u, v) -> IF(x, u, if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, false, if(x'', y'', z'')), u, v) -> IF(x, v, if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, if(x''', y''', z'), if(x'', y'', z'')), u, v) -> IF(x, if(x''', if(y''', u, v), if(z', u, v)), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, y, if(true, y''', z''')), u, v) -> IF(x, if(y, u, v), if(y''', u, v))
IF(if(x, y, if(false, y''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, y, if(x''', z''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, y, if(x'', true, z'')), u, v) -> IF(x, if(y, u, v), if(x'', u, if(z'', u, v)))
IF(if(x, y, if(x'', false, z'')), u, v) -> IF(x, if(y, u, v), if(x'', v, if(z'', u, v)))
IF(if(x, y, if(x'', if(x''', y''', z'), z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(x''', if(y''', u, v), if(z', u, v)), if(z'', u, v)))
IF(if(x, y, if(x'', y'', true)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), u))
IF(if(x, y, if(x'', y'', false)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), v))
IF(if(x, y, if(x'', y'', if(x''', y''', z'))), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(x''', if(y''', u, v), if(z', u, v))))

The transformation is resulting in one new DP problem:

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

Dependency Pairs:

IF(if(x, y, if(x'', y'', if(x''', y''', z'))), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(x''', if(y''', u, v), if(z', u, v))))
IF(if(x, y, if(x'', y'', false)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), v))
IF(if(x, y, if(x'', y'', true)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), u))
IF(if(x, y, if(x'', if(x''', y''', z'), z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(x''', if(y''', u, v), if(z', u, v)), if(z'', u, v)))
IF(if(x, y, if(x'', false, z'')), u, v) -> IF(x, if(y, u, v), if(x'', v, if(z'', u, v)))
IF(if(x, y, if(x'', true, z'')), u, v) -> IF(x, if(y, u, v), if(x'', u, if(z'', u, v)))
IF(if(x, y, if(x''', z''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, y, if(false, y''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, y, if(true, y''', z''')), u, v) -> IF(x, if(y, u, v), if(y''', u, v))
IF(if(x, if(x''', y''', z'), if(x'', y'', z'')), u, v) -> IF(x, if(x''', if(y''', u, v), if(z', u, v)), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, true, if(x'', y'', z'')), u, v) -> IF(x, u, if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', y'', true), z), u, v) -> IF(x, if(x'', if(y'', u, v), u), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', true, z''), z), u, v) -> IF(x, if(x'', u, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(true, y''', z'''), z), u, v) -> IF(x, if(y''', u, v), if(z, u, v))
IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, if(x'', y'', z'), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z', u, v)), v)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

The following dependency pairs can be strictly oriented:

IF(if(x, y, if(x'', y'', true)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), u))
IF(if(x, y, if(x'', true, z'')), u, v) -> IF(x, if(y, u, v), if(x'', u, if(z'', u, v)))
IF(if(x, y, if(true, y''', z''')), u, v) -> IF(x, if(y, u, v), if(y''', u, v))
IF(if(x, true, if(x'', y'', z'')), u, v) -> IF(x, u, if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, true, false), u, v) -> IF(x, u, v)
IF(if(x, if(x'', y'', true), z), u, v) -> IF(x, if(x'', if(y'', u, v), u), if(z, u, v))
IF(if(x, if(x'', true, z''), z), u, v) -> IF(x, if(x'', u, if(z'', u, v)), if(z, u, v))
IF(if(x, if(true, y''', z'''), z), u, v) -> IF(x, if(y''', u, v), if(z, u, v))
IF(if(x, true, if(x'', y', z'')), u, v) -> IF(x, u, if(x'', if(y', u, v), if(z'', u, v)))

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(v) =  0 POL(false) =  0 POL(true) =  1 POL(u) =  0 POL(IF(x1, x2, x3)) =  1 + x1

resulting in one new DP problem.

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

Dependency Pairs:

IF(if(x, y, if(x'', y'', if(x''', y''', z'))), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(x''', if(y''', u, v), if(z', u, v))))
IF(if(x, y, if(x'', y'', false)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), v))
IF(if(x, y, if(x'', if(x''', y''', z'), z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(x''', if(y''', u, v), if(z', u, v)), if(z'', u, v)))
IF(if(x, y, if(x'', false, z'')), u, v) -> IF(x, if(y, u, v), if(x'', v, if(z'', u, v)))
IF(if(x, y, if(x''', z''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, y, if(false, y''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, if(x''', y''', z'), if(x'', y'', z'')), u, v) -> IF(x, if(x''', if(y''', u, v), if(z', u, v)), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)
IF(if(x, if(x'', y'', z'), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z', u, v)), v)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

The following dependency pairs can be strictly oriented:

IF(if(x, y, if(x'', y'', false)), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), v))
IF(if(x, y, if(x'', false, z'')), u, v) -> IF(x, if(y, u, v), if(x'', v, if(z'', u, v)))
IF(if(x, y, if(false, y''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, if(x'', y'', z''), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), v)
IF(if(x, if(x'', y'', false), z), u, v) -> IF(x, if(x'', if(y'', u, v), v), if(z, u, v))
IF(if(x, if(x'', false, z''), z), u, v) -> IF(x, if(x'', v, if(z'', u, v)), if(z, u, v))
IF(if(x, if(false, y''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, if(x'', y'', z'), false), u, v) -> IF(x, if(x'', if(y'', u, v), if(z', u, v)), v)

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2, x3)) =  x1 + x2 + x3 POL(v) =  0 POL(false) =  1 POL(true) =  1 POL(u) =  0 POL(IF(x1, x2, x3)) =  x1

resulting in one new DP problem.

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

Dependency Pairs:

IF(if(x, y, if(x'', y'', if(x''', y''', z'))), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(x''', if(y''', u, v), if(z', u, v))))
IF(if(x, y, if(x'', if(x''', y''', z'), z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(x''', if(y''', u, v), if(z', u, v)), if(z'', u, v)))
IF(if(x, y, if(x''', z''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, if(x''', y''', z'), if(x'', y'', z'')), u, v) -> IF(x, if(x''', if(y''', u, v), if(z', u, v)), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

The following dependency pairs can be strictly oriented:

IF(if(x, y, if(x'', y'', if(x''', y''', z'))), u, v) -> IF(x, if(y, u, v), if(x'', if(y'', u, v), if(x''', if(y''', u, v), if(z', u, v))))
IF(if(x, y, if(x'', if(x''', y''', z'), z'')), u, v) -> IF(x, if(y, u, v), if(x'', if(x''', if(y''', u, v), if(z', u, v)), if(z'', u, v)))
IF(if(x, y, if(x''', z''', z''')), u, v) -> IF(x, if(y, u, v), if(z''', u, v))
IF(if(x, if(x''', y''', z'), if(x'', y'', z'')), u, v) -> IF(x, if(x''', if(y''', u, v), if(z', u, v)), if(x'', if(y'', u, v), if(z'', u, v)))
IF(if(x, if(x'', y'', z''), if(x''', y', z''')), u, v) -> IF(x, if(x'', if(y'', u, v), if(z'', u, v)), if(x''', if(y', u, v), if(z''', u, v)))
IF(if(x, if(x'', y'', if(x''', y', z''')), z), u, v) -> IF(x, if(x'', if(y'', u, v), if(x''', if(y', u, v), if(z''', u, v))), if(z, u, v))
IF(if(x, if(x'', if(x''', y', z'''), z''), z), u, v) -> IF(x, if(x'', if(x''', if(y', u, v), if(z''', u, v)), if(z'', u, v)), if(z, u, v))
IF(if(x, if(x''', z''', z'''), z), u, v) -> IF(x, if(z''', u, v), if(z, u, v))
IF(if(x, y, z), u, v) -> IF(z, u, v)
IF(if(x, y, z), u, v) -> IF(y, u, v)

There are no usable rules w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(if(x1, x2, x3)) =  1 + x1 + x2 + x3 POL(v) =  0 POL(false) =  0 POL(true) =  1 POL(u) =  0 POL(IF(x1, x2, x3)) =  x1

resulting in one new DP problem.

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

Dependency Pair:

Rules:

if(true, x, y) -> x
if(false, x, y) -> y
if(x, y, y) -> y
if(if(x, y, z), u, v) -> if(x, if(y, u, v), if(z, u, v))

Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:24 minutes