[isabelle] new AFP entry: Decreasing Diagrams
- To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] new AFP entry: Decreasing Diagrams
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Mon, 18 Nov 2013 12:51:02 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHO5FzWQFx+JwA+p02aWx6IwIKI2w==
- Thread-topic: new AFP entry: Decreasing Diagrams
A new AFP entry is available from http://afp.sf.net
by Harald Zankl
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.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and