reference for lexicographic path ordering Can you recommend a good reference for reading about lexicographic/recursive path orderings?

I'm currently reading about lpo's in Chapter 2 of the Handbook of Automated Reasoning, 'Resolution Theorem Proving' by Bachmair and Ganzinger, but the presentation is really terse. I would ideally like a more tutorial-like introduction w/ examples.
Some information at the right level of abstraction can be found in:


Nachum Dershowitz's A Taste of Rewrite Systems


If you are near a library or bookshop, this book has even more details:


Baader and Nipkov's Term Rewriting and All That