An Inductive Version of Nash-Williams' Minimal-Bad-Sequence Argument for Higman's Lemma

Higman's lemma has a very elegant, non-constructive proof due to Nash-Williams [NW63] using the so-called minimal-bad-sequence argument. The objective of the present paper is to give a proof that uses the same combinatorial idea, but is constructive. For a two letter alphabet this was done by Coquand and Fridlender [CF94]. Here we present a proof in a theory of inductive definitions that works for arbitrary decidable well quasiorders.

• Type: Conference
• Year: 2000
• Where: TYPES
• Authors: Monika Seisenberger
• Keywords: Formal Methods, Higman's Lemma, Non-constructive Proof, Present Paper, TYPES 2000