Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

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 )

1.1: reduction pair processor

Using the following reduction pair

Linear polynomial interpretation over the naturals
[v] = 0
[true] = 0
[if (x1, x2, x3) ] = 2 x1 + x2 + x3 + 2
[u] = 0
[false] = 0
[if# (x1, x2, x3) ] = x1
[f(x1, ..., xn)] = x1 + ... + xn + 1 for all other symbols f of arity n

one remains with the following pair(s).

none

1.1.1: P is empty

All dependency pairs have been removed.