A constructive proof of Higman's lemma

Abstract

G. Higman's lemma (1952) is a special case of the more general Kruskal's tree embedding theorem and the graph minor theorem. A direct constructive proof of the lemma with manifest computational content is presented. This is done by reducing the problem to a construction of certain sets of sequential regular expressions. A well-founded order on such sets is exhibited, and the lemma then follows by induction.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>