Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

not#( x ) → if#( x , false , true )
and#( x , y ) → if#( x , y , false )
or#( x , y ) → if#( x , true , y )
implies#( x , y ) → if#( x , y , true )
=#( x , y ) → if#( x , y , not( y ) )
=#( x , y ) → not#( y )
=#( x , y ) → if#( x , y , if( y , false , true ) )
=#( x , y ) → if#( y , false , true )

1.1: dependency graph processor

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