Decreasing Diagrams

Harald Zankl 🌐

November 1, 2013

Abstract

This theory contains a formalization of decreasing diagrams showing that any locally decreasing abstract rewrite system is confluent. We consider the valley (van Oostrom, TCS 1994) and the conversion version (van Oostrom, RTA 2008) and closely follow the original proofs. As an application we prove Newman's lemma.

License

GNU Lesser General Public License (LGPL)

Topics

Session Decreasing-Diagrams

Depends on

Auto-related entries

Cite

× 
@article{Decreasing-Diagrams-AFP,
  author  = {Harald Zankl},
  title   = {Decreasing Diagrams},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2013},
  note    = {\url{https://isa-afp.org/entries/Decreasing-Diagrams.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: