Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

g#( x , a , b ) g#( b , b , a )

1.1: dependency graph processor

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