# * A Constructive Proof of Higman's Lemma *

## by Chetan Murthy, James R. Russell

1990

Proceedings of Fifth IEEE Symposium on Logic in Computer Science

**Abstract**

Higman's Lemma is a special case of the more general Kruskal's tree embedding theorem and the graph minor theorem. Prior to this work, only classical (and impredicative) proofs of the Lemma were known. Recently, there has been much interest in developing a constructive proof of the Lemma, primarily via Friedman's A-translation. In this paper we present a direct constructive proof. We achieve this by reducing the problem to a construction of certain sets of sequential regular expressions. We then exhibit a well-founded order on such sets, and the Lemma then follows by induction.

**bibTex ref: MR90**

cite link