Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

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

1.1: dependency graph processor

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