Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( X ) → if#( X , c , n__f( true ) )
if#( false , X , Y ) → activate#( Y )
activate#( n__f( X ) ) → f#( X )

1.1: reduction pair processor

Using the following reduction pair

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

one remains with the following pair(s).

if#( false , X , Y ) → activate#( Y )

1.1.1: dependency graph processor

The dependency pairs are split into 0 component(s).