The Z Property

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

The Archive of Formal Proofs, 2016.


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.


  PDF  |    AFP entry


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{}, Formal proof development",
ISSN = "2150-914x",
Nach oben scrollen