Termination proof

1: switching to dependency pairs

The following set of initial dependency pairs has been identified.

d#( u( x ) ) c#( x )
c#( u( x ) ) b#( x )

1.1: dependency graph processor

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