Decreasing Diagrams II

Bertram Felgenhauer 📧

August 20, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

GNU Lesser General Public License (LGPL)

Topics

Session Decreasing-Diagrams-II

Depends on

Cite

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

Download

× Download latest

Older releases: