Lars With: Completeness and Confluence of Order-Sorted Term Rewriting. CTRS 1992: 393-407