# The ZProperty

 Title: The Z Property Authors: Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel 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