Decreasing Diagrams II

Bertram Felgenhauer

20 August 2015

Abstract

This theory formalizes the commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.
GNU Lesser General Public License (LGPL)

Depends On

Topics

Related Entries

Theories

Cite

×
@article{Decreasing-Diagrams-II-AFP,
  author  = {Bertram Felgenhauer},
  title   = {Decreasing Diagrams II},
  journal = {Archive of Formal Proofs},
  month   = August,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Decreasing-Diagrams-II.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download