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: Nov 21 2024 at 12:39 UTC