Email Gateway (Apr 13 2025 at 07:46): Email Gateway (Apr 13 2025 at 07:46):From: Tobias Nipkow <nipkow@in.tum.de>
Completeness of Decreasing Diagrams for the Least Uncountable Cardinality
Ievgen Ivanov
In Decreasing-Diagrams it was formally proved that the decreasing diagrams
method is sound for proving confluence: if a binary relation r has LD property
defined in Decreasing-Diagrams, then it has CR property defined in
Abstract-Rewriting.
In this formal theory it is proved that if the cardinality of r
does not exceed the first uncountable cardinal, then r has CR property if and
only if has LD property. As a consequence, the decreasing diagrams method is
complete for proving confluence of relations of the least uncountable cardinality.
https://www.isa-afp.org/entries/Completeness_Decreasing_Diagrams_for_N1.html
Enjoy!
Last updated: May 06 2025 at 08:28 UTC