# The ZProperty

 Title: The Z Property Authors: Bertram Felgenhauer (int-e /at/ gmx /dot/ de), 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{https://isa-afp.org/entries/Rewriting_Z.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Abstract-Rewriting, Nominal2 Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.