Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] new AFP entry: Decreasing Diagrams


view this post on Zulip Email Gateway (Aug 19 2022 at 12:33):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
A new AFP entry is available from http://afp.sf.net

Decreasing Diagrams
by Harald Zankl

Abstract:
This theory contains a formalization of decreasing diagrams showing that any locally decreasing abstract rewrite system is confluent. We consider the valley (van Oostrom, TCS 1994) and the conversion version (van Oostrom, RTA 2008) and closely follow the original proofs. As an application we prove Newman's lemma.

Cheers,
Gerwin


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


Last updated: Apr 25 2024 at 20:15 UTC