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.

BibTeX

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