Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

f#( x , y ) h#( x , y )
f#( x , y ) h#( y , x )

1.1: dependency graph processor

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