Termination Proof using AProVE

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.

     ↳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.

     ↳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:

     ↳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:

     ↳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:

     ↳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:

     ↳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:

     ↳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(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(v) = 0

POL(false) = 0

POL(true) = 1

POL(u) = 0

POL(IF(x₁, x₂, x₃)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Polynomial Ordering

Dependency Pairs:

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(x₁, x₂, x₃)) = x₁ + x₂ + x₃

POL(v) = 0

POL(false) = 1

POL(true) = 1

POL(u) = 0

POL(IF(x₁, x₂, x₃)) = x₁

resulting in one new DP problem.

     ↳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(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃

POL(v) = 0

POL(false) = 0

POL(true) = 1

POL(u) = 0

POL(IF(x₁, x₂, x₃)) = x₁

resulting in one new DP problem.

     ↳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

POL(if(x₁, x₂, x₃))	= x₁ + x₂ + x₃
POL(v)	= 0
POL(false)	= 0
POL(true)	= 1
POL(u)	= 0
POL(IF(x₁, x₂, x₃))	= 1 + x₁

POL(if(x₁, x₂, x₃))	= 1 + x₁ + x₂ + x₃
POL(v)	= 0
POL(false)	= 0
POL(true)	= 1
POL(u)	= 0
POL(IF(x₁, x₂, x₃))	= x₁