The Z Property

Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel

30 June 2016

Abstract

We formalize the Z property introduced by Dehornoy and van Oostrom. First we show that for any abstract rewrite system, Z implies confluence. Then we give two examples of proofs using Z: confluence of lambda-calculus with respect to beta-reduction and confluence of combinatory logic.
BSD License

Depends On

Topics

Related Entries

Theories

Cite

×
@article{Rewriting_Z-AFP,
  author  = {Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel},
  title   = {The Z Property},
  journal = {Archive of Formal Proofs},
  month   = June,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Rewriting_Z.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
Download