An old proof of the wellfoundednes of the multiset ordering

• To: types@cis.upenn.edu
• Subject: An old proof of the wellfoundednes of the multiset ordering
• From: Tobias.Nipkow@informatik.tu-muenchen.de
• Date: Fri, 16 Oct 1998 09:22:07 +0200
• Sender: Tobias Nipkow <nipkow@informatik.tu-muenchen.de>

The proof that the multisets ordering preserves wellfoundedness that I posted
here on Monday had already been discovered by Thierry Coquand. He told me

> I had a similar argument in An Analysis of Ramsey Theorem, Information
> and Computation 110, 1994, p. 297-304. This is lemma 7 (at the end
> in the remarks, I point out that this can be used for proving that
> a multiset extension of a wf relation is wf).

Tobias

• Prev: a repository for CS research
• Next: International Masters Programme in Computational Logic
• Index(es):
  • Main
  • Thread