Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( x , y ) → g1#( x , x , y )
f#( x , y ) → g1#( y , x , x )
f#( x , y ) → g2#( x , y , y )
f#( x , y ) → g2#( y , y , x )
g1#( x , x , y ) → h#( x , y )
g1#( y , x , x ) → h#( x , y )
g2#( x , y , y ) → h#( x , y )
g2#( y , y , x ) → h#( x , y )

1.1: dependency graph processor

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