Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: The Z Property

view this post on Zulip Email Gateway (Aug 22 2022 at 13:30):

From: Tobias Nipkow <nipkow@in.tum.de>
The Z Property
Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom and Christian Sternagel

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.

https://www.isa-afp.org/entries/Rewriting_Z.shtml

Enjoy!
smime.p7s

Last updated: Apr 24 2024 at 20:16 UTC