Termination proof
1: switching to dependency pairs
The following set of initial dependency pairs has been identified.
none
1.1: P is empty
All dependency pairs have been removed.