Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

g#( h( g( x ) ) ) g#( x )
g#( g( x ) ) g#( h( g( x ) ) )
g#( g( x ) ) h#( g( x ) )
g#( g( x ) ) g#( x )
h#( h( x ) ) h#( f( h( x ) , x ) )
h#( h( x ) ) h#( x )

1.1: dependency graph processor

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