### A Proof Order for Decreasing Diagrams

Bertram FelgenhauerProceedings of the 1st International Workshop on Confluence (IWC 2012), pp. 7 – 13, 2012.

### Abstract

In this note we describe a well-founded proof order that entails the

decreasing diagrams technique, i.e., it orders peaks of locally

decreasing diagrams above their joining sequences. We also investigate

an extension that promises to be useful for proving confluence modulo.

Unrelated to this proof order we also present an example showing that

witnesses for non-confluence can not always be found by starting from

critical pairs alone, even for linear TRSs.

### BibTeX

@inproceedings{BF-IWC12, author = "Bertram Felgenhauer", title = "A Proof Order for Decreasing Diagrams", booktitle = "Proceedings of the 1st International Workshop on Confluence", pages = "7--13", year = 2012 }