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
                 ↳Argument Filtering and 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'', 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, 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)


The following usable rules using the Ce-refinement can be oriented:

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))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
IF > if

resulting in one new DP problem.
Used Argument Filtering System:
IF(x1, x2, x3) -> IF(x1, x2, x3)
if(x1, x2, x3) -> if(x1, x2, x3)


   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳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:31 minutes