The Z Property

 

Title: The Z Property
Authors: Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com)
Submission date: 2016-06-30
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{Rewriting_Z-AFP,
  author  = {Bertram Felgenhauer and Julian Nagele and Vincent van Oostrom and Christian Sternagel},
  title   = {The Z Property},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/Rewriting_Z.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Abstract-Rewriting, Nominal2