## Cs.au.dk

**An Inductive Version of Nash-Williams’**
**Minimal-Bad-Sequence Argument**
**for Higman’s Lemma**
1 Mathematisches Institut der Universit¨at M¨unchen
2 Department of Computer Science, University of Wales Swansea

*†*
**Abstract. **Higman’s lemma has a very elegant, non-constructive proof

due to Nash-Williams 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 alpha-

bet this was done by Coquand and Fridlender . Here we present

a proof in a theory of inductive deﬁnitions that works for arbitrary de-

cidable well quasiorders.

**Introduction**
This paper is concerned with Higman’s lemma usually formulated interms of well quasi orders.

If (

*A, ≤A*) is a well quasiorder, then so is the set

*A∗ *of ﬁnite sequencesin

*A*, together with the embeddability relation

*≤A∗*,
where a sequence [

*a*1

*, . . . , an*] is embeddable in [

*b*1

*, . . . , bm*] if there is a strictlyincreasing map

*f *:

*{*1

*, . . . , n} → {*1

*, . . . , m} *such that

*ai ≤A bf*(

*i*) for all

*i ∈*
Among the ﬁrst proofs of Higman’s lemma which all were non-constructive
the proof of Nash-Williams using the so-called minimal-bad-sequence argumentis considered most elegant. A variant of this proof was translated by Murthy viaFriedman’s

*A*-translation into a constructive proof however resulting ina huge proof whose computational content couldn’t yet be discovered. More di-rect constructive proofs were given by Sch¨
dinal notations up to 0 and is related to an earlier proof by Schmidt theother proofs are carried out in a (proof theoretically stronger) theory of induc-tive deﬁnitions. However, their computational content is essentially the same,but does not correspond to that one of Nash-Williams’ proof. (The proof the-oretic strength of the general minimal-bad-sequence argument is Π1

*−*CA
Research supported by the DFG Graduiertenkolleg “Logik in der Informatik”.

*† *Research supported by the British EPSRC.

P. Callaghan et al. (Eds.): TYPES 2000, LNCS 2277, pp. 2002.

was shown by Marcone, however it is open whether the special form used forHigman’s lemma has the same strength .)
The objective of this paper is to present a constructive proof that captures
the combinatorial idea behind Nash-Williams’ proof. For an alphabet

*A *con-sisting of two letters this was done by Coquand and Fridlender Theirproof can quite easily be extended to a ﬁnite alphabet. To obtain a proof forarbitrary decidable well quasiorders, more eﬀort is necessary, as we will describein section
A proof of Higman’s lemma which in contrast to all proofs mentioned above
does not require decidability of the given relation

*≤A *was given by Fridlender. His proof is based on a proof by Veldman that can be found in .

In our formulation of Higman’s lemma we will also use an accessibility notion,as it was done in Fridlender’s proof.

**Basic Definitions and an Inductive Characterization of**

Well Quasiorders
In the whole paper we assume (

*A, ≤A*) to be a set with a reﬂexive and transitive,decidable relatio

**Definition 1. **We use

*a, b, . . . *for letters, i.e., elements of a

*A,*
*as, bs, . . . *for ﬁnite sequences of letters, i.e. elements of

*A∗,*
*v, w, . . . *for words, i.e., elements of

*A∗, *2

*vs, ws, . . . *for ﬁnite sequences of words, i.e., elements of

*A∗∗ .*
By

*as∗a *we denote the sequence obtained from the sequence

*as *by appending theelement

*a*.

*ws∗w *is deﬁned similarly. At some places we add brackets to keep theexpressions legible. However, unary function application will be written withoutbrackets, in general.

For a ﬁnite sequence

*ws *of non-empty words let lasts

*ws *denote the ﬁnite
sequence consisting of the end-letters of the words of

*ws*, that is
lasts [

*w*1

*∗a*1

*, . . . , wn∗an*] = [

*a*1

*, . . . , an*]

*, n ≥ *0

*.*
1 Whereas transitivity is only required for historical reasons, but is not used in our
proof, decidability plays an essential role.

*w*1

*w*2

*w*3

*w*4

*w*5
Although of the same kind we distinguish be-tween ﬁnite sequences (of letters) and words,because they will play diﬀerent rolls, as is il-lustrated in the picture on the right.

3 In our picture we have lasts [

*w*1

*, . . . , w*5] =

*as*.

An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument

**Definition 2 (Higman Embedding). **The embedding relation on

*A∗ *can be

inductively described by the following rules:

**Definition 3 (Good/Bad). **A ﬁnite sequence [

*a*1

*, . . . , an*] (respectively an in-

ﬁnite sequence

*a*1

*, a*2

*, . . .*) of elements in

*A *is good if there exist

*i < j ≤ n*

(

*i < j < ω*) such that

*ai ≤A aj*; otherwise it is called bad.

Furthermore, we use the notion good(

*as, a*) if there is an element in

*as*, say
the i-th one, such that (

*as*)

*i ≤A a*. bad(

*as, a*) stands for

*¬*good(

*as, a*).

Finally, badsubseq(

*as*) determines the ﬁrst occurring bad subsequence in

*as*:
badsubseq(

*as*)

*∗a *if bad(badsubseq(

*as*)

*, a*)

*,*
**Definition 4 (Well Quasiorder). **(

*A, ≤A*) is a well quasiorder (wqo) if every

inﬁnite sequence of elements in

*A *is good.

**Definition 5 (The Relation**
*A ***and Its Accessible Part). **The relation

*bs A as *:

*↔ bs *=

*as∗a *for some

*a ∈ A *s.t. bad(

*as, a*)

*.*
The accessible part (also called the well-founded part) of the relation
and provides the following induction prfor any formula

*φ*:

*∀as. ∀bs A as φ*(

*bs*)

*→ φ*(

*as*)

*.*
**Definition 6 (Well Quasiorder, Inductive Characterizati****). **(*A, ≤A*)

is a well quasiorder if acc

4 At some places we use a seemingly stronger induction principle where the premise
*A as φ*(*bs*) *→ φ*(*as*)*. *This principle can be easily
Deﬁnitions to should be understood for arbitrary (reﬂexive and transitive)
relations, not only for our ﬁxed (*A, ≤A*). We will use them also for (*A∗, ≤A∗*).

Moreover, the operation acc will also be applied to the relations
**Towards a Constructive Proof**

In order to motivate further deﬁnitions we ﬁrst want to give the idea behindthe constructive proof. This is best done by showing the connection between theclassical and the constructive proof. To this end we shortly recall Nash-Williams’minimal-bad-sequence proof and show how the main steps are captured by theinductive proof. We also include an informal idea of the latter.

*The steps of the Nash-Williams’ proof:*
1. In order to show “wqo(*A*) implies wqo(*A∗*)”, assume for contraction that
2. Among all inﬁnite bad sequences we choose (using classical dependent choice)
a minimal bad sequence, i.e., a sequence, say (*wi*)*i<ω, *which is minimal withrespect to a lexicographical order on inﬁnite sequences of words (where *w*1is less or equal *w*2, if *w*1 is an initial segment of *w*2).

3. Since *wi *= [ ], let *wi *= *vi∗ai *for all *i*. Using Ramsey’s theorem and the
fact that our alphabet *A *is a well quasiorder, we know that there exists aninﬁnite subsequence *aκ ≤*
*A · · · *of the sequence (*ai*)*i<ω. *This also
determines a corresponding sequence *w*1*, . . . , wκ*
4. The sequence *w*1*, . . . , wκ*
*, v , . . .*. must be bad (otherwise (*w*
would be good), but this contradicts the minimality in 2.

*In the constructive proof this steps correspond to*
2. The minimality argument will be replaced by structural induction on words.

3. Given a bad sequence *ws *= [*w*1*, . . . , wn*] s.t. *wi *= *vi∗ai*, we are interested
sponding sequences *w*1*, . . . , wκ*
*, . . . , v *. In the proof these sequences
will be computed by the procedure forest which takes *ws *as input and yieldsa forest labeled by pairs in *A∗∗ × A*. In the produced forest the right-handcomponents of each path form a weakly ascending subsequence of [*a*1*, . . . , an*]
5 In our paper we only deal with this second deﬁnition of a well quasiorder since it is
very suitable for a constructive proof. For sake of completeness we give an argumentfor the equivalence of deﬁnition and deﬁnition To prove that deﬁnition impliesdeﬁnition one shows more generally that for all *as *such that acc
inﬁnite sequence, starting with *as*, is good. The reverse direction is an instance ofBrouwer’s axiom of bar induction.

6 By maximal length we mean that we only look at those subsequences which are
ascending, but not contained in other ones, for instance our chosen subsequences of[1*, *4*, *3*, *0*, *3] are [1*, *4]*, *[1*, *3*, *3] and [0*, *3].

An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
and the corresponding sequence of form *w*1*, . . . , wκ*
read oﬀ in the left-hand component of the endnode of such a path. If weextend the sequence *ws *badly by a word *v∗a*, then in the existing foresteither new nodes, possibly at several places, are inserted, or a new singletontree with node *ws∗v, a *is added. Now the informal idea of the inductiveproof is: if in forest *ws *not inﬁnitely often new nodes could be inserted andif also not inﬁnitely often new trees could be added, then *ws *could not beextended badly inﬁnitely often. Formally this will be captured by the state-ment: *∀ws. *acc
badsubseq(lasts *ws*) *→ *acc
*≺ *forest *ws → *acc *A∗ ws*
4. The ﬁrst part of item 4 corresponds to lemma
We proceed with the formal deﬁnition of forest and the relation *≺ *on forests.

**Definition 7. **We use

for elements in *T *(*A∗∗ × A*), i.e., trees labeled by pairs in *A∗∗ × A,*
*f, ts *for elements in (*T *(*A∗∗ × A*))*∗*, i.e., forests.

The tree with root *ws, a *and ﬁnite sequence of immediate subtrees *ts *is written
*ws, a ts*. We use the destructors left and right for pairs and the destructors root
and subtrees for trees, hence root *ws, a ts *= *ws, a *and subtrees *ws, a ts *= *ts*.

For better readability we set:
:= [root *t*1*, . . . , *root *tn*]*,*
lefts [ *vs*1*, a*1 *, . . . , vsn, an *] := [*vs*1*, . . . , vsn*]*,*rights [ *vs*1*, a*1 *, . . . , vsn, an *] := [*a*1*, . . . , an*]*.*
**Definition 8. **Let *ws ∈ A∗∗ *be a sequence of non-empty words. Then forest *ws ∈*

*T *((*A∗∗ × A*))*∗ *is deﬁned recursively by:
if good(badsubseq(lasts *ws*)*, a*)
(forest *ws*) *∗ *newtree *ws∗w, a *otherwise,
7 For sake of simplicity we deﬁne insertforest by a map operation, i.e., we insert a new
node at every possible place. However, it would already suﬃce to insert at least onceand it even could be arbitrarily chosen where to insert.

8 In case of a ﬁnite alphabet forest *ws *has only non-branching trees where the right-
hand components of such a tree are constant. So, if in the notion of wehave *T*0(*vs, ws*) or *R*0(*vs, ws*), in our setting the sequence *vs *could be read oﬀ as theleft-hand component in the endnode of the tree whose right-hand components are 0.

insertforest(*f, w, a*) = map *λt *
inserttree(*t, w, a*) *f*
*vs, a *insertforest(*ts, w, a*)
if good(rights (roots *ts*)*, a*)*,*
*vs, a *(*ts ∗ *newtree *vs∗w, a *) otherwise.

**Definition 9. **Let *f *and *f *be forests in *T *((*A∗∗ × A*))*∗. *Then

*f *= insertforest(*f, w, a*) for some *w ∈ A∗, a ∈ A*
*f ≺ f *:*↔ *such that *f *= *f *and the left-hand component of
each label in *f *is a bad sequence in *A∗∗.*
**Lemma 1. **Let *ws *be a bad sequence of non-empty words. Then in every label

of forest *ws *the left-hand component is a bad sequence.

*Proof. *IND(structure of *ws*). 1. *ws *= [ ]. Clear.

2. Assume that every left-hand component of a label in forest *ws *is bad and
look at the nodes in forest *ws∗*(*w∗a*) where *ws∗*(*w∗a*) is assumed to be bad.

Case 1: bad(badsubseq(lasts *ws*)*, a*). Then in forest *ws∗*(*w∗a*) only one node
was added, i.e., the node with label *ws∗w, a *where by assumption *ws∗w *isbad.

Case 2: good(badsubseq(lasts *ws*)*, a*). In this cassome nodes of the form
*vs∗w, a *were inserted in forest *ws *where *vs *is a left-hand component of a node in
forest *ws *which by assumption is bad. Assume good(*vs, w*)*, *that is, *∃i*(*vs*)*i ≤A∗ w*and show *⊥*.

Case 2.1: (*vs*)*i *is a word in *ws*. Then, by the Higman embedding we obtain
(*vs*)*i ≤A∗ w∗a *– contradicting the badness of *ws∗*(*w∗a*).

Case 2.2: (*vs*)*i *is a word in *ws *cut by an end letter *a*0 and by the construction
of the forests it holds *a*0 *≤A a*Then, again by the Higman embedding it follows(*vs*)*i∗a*0 *≤A∗ w∗a. *Contradiction.

**Lemma 2. **i) acc*≺ *[]*. *ii) acc*≺ f ∧ *acc*≺ *[*t*] *→ *acc*≺ f ∗ t.*

*Proof. *i) acc*≺ *[] holds by deﬁnition, since there is no tree in which new nodescould be inserted. ii) Clear, since insertforest is deﬁned by a map-operation.

9 Here, we only sketch the combinatorial part of the proof; a formal proof involves an
10 Note that transitivity is not required.

An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
**Lemma 3. **Assume acc

*A∗ ws → ∀a. *acc*≺ *[newtree *ws, a *]*.*
*Proof. *IND1(acc *A∗ *): IH1 : *∀vs*
*A∗ ws, ∀a. *acc*≺ *[newtree *vs, a *]*. *Let *a ∈ A*. In-
stead of proving acc*≺ *[newtree *ws, a *] we show more generally that this assertionholds for all *t *with root *t *= *ws, a *such that
(a) the subtrees of *t *form a forest in acc*≺ *and(b) rights (roots (subtrees *t*)) is sequence in acc
We do this by main induction on (b) and side induction on (a), i.e., formally
*∀t. *root *t *= (*ws, a*) *∧ *subtrees *t *= *ts ∧ as *= rights (roots (subtrees *t*)) *→*
). Assume that we have an *as *such that acc
IND3(acc*≺ *). Let *ts *be such that acc*≺ ts *and ﬁx *t *such that root *t *= *ws, a *,
subtrees *t *= *ts*, and *as *= rights (roots (subtrees *t*)).

We have to prove acc*≺ *[*t*]. By the deﬁnition of acc*≺ *and *≺ *if suﬃces to show
*∀t . *[*t *] *≺ *[*t*] *→ *acc*≺ *[*t *] where *t *= inserttree(*t, w, a *) = *t *for some *w ∈ A∗, a ∈ A*and all left-hand components of nodes in *t *are required to be bad. We prove theassertion by case distinction on the deﬁnition of inserttree.

Case 1: *t *= *ws, a *(*ts ∗ *newtree *ws∗w, a *) for some *w *and *a *such that
subtrees *t *= *ts ∗ *newtree *ws∗w, a ,as∗a*
= rights (roots (*ts ∗ *newtree *ws∗w, a *))*.*
Since all left-hand components in *t *are supposed to be bad, in particular, we havethat *ws∗w *is bad, i.e., *ws∗w*
*A∗ ws*. By IH1 we obtain acc*≺ *[newtree *ws∗w, a *],
acc*≺ ts ∗ *newtree *ws∗w, a .*
*A as*, we may apply IH2 to *as∗a , ts ∗ *newtree *ws∗w, a*
and conclude acc*≺ *[*t *]*.*
Case 2: *t *= *ws, a *insertforest(*ts, w, a *) where *a *such that good(*as, a *). In
subtrees *t *= insertforest(*ts, w, a *)*,as*
= rights (roots (subtrees *t *))*.*
11 It’s intended that [*t*] lies in the image of the partial function forest, however we
don’t need this restriction in the formulation of the lemma.

Moreover [*t *] *≺ *[*t*] implies subtrees *t ≺ *subtrees *t *= *ts*, and by IH3, applied tosubtrees *t *and *t *, we end up with acc*≺ *[*t *]*.*
Now, the proof of the general assertion is completed, and we may put *as *= [ ],
*f *= [] and *t *= newtree *ws, a *. Since we have acc
by lemma we obtain acc *A∗ ws → *acc*≺ *[newtree *ws, a *].

**The Proof of Higman’s Lemma**

**Proposition 1 (Higman’s Lemma). **acc

*∀ws. as *= badsubseq(lasts *ws*) *∧ f *= forest *ws → *acc *A∗ ws.*
*∀ws. bs *= badsubseq(lasts *ws*) *∧ f *= forest *ws → *acc *A∗ ws.*
IND2(acc*≺ *). Let *f *be s.t acc*≺ f *and IH2 : *∀f ≺ f, ∀ws. *badsubseq(lasts *ws*) =
*as ∧ f *= forest *ws → *acc *A∗ ws *and assume that we have *ws *such that *as *=badsubseq(lasts *ws*) and *f *= forest *ws*. In order to prove acc *A∗ ws *we ﬁx *w *s.t.

*ws∗w *is bad and show acc *A∗ ws∗w *by induction on the structure of *w*:
IND3(*w*). 1. acc *A∗ ws*[] holds by deﬁnition of acc *A∗ *.

2. Now, assume that we have a word of form *w∗a*. We show acc *A∗ ws∗*(*w∗a*)
by case analysis on whether or not bad(*as, a*).

Case 2.1: bad(*as, a*). Then we have
= badsubseq(lasts (*ws∗*(*w∗a*)))*,*
*f ∗ *newtree *ws∗w, a *= forest (*ws∗*(*w∗a*))*.*
First, we show acc*≺ f ∗ *newtree *ws∗w, a *. By assumption we already have acc*≺ f*and by IH3 acc *A∗ ws∗w. *Hence, by lemma we obtain acc*≺ *[newtree *ws∗w, a *]and by lemma we may conclude
acc*≺ f ∗ *newtree *ws∗w, a .*
Now we are able to apply IH1 (to *as∗a, f ∗ *newtree *ws∗w, a *and *ws∗*(*w∗a*)) andend up with acc *A∗ ws∗*(*w∗a*)*.*
Case 2.2: good(*as, a*)*. *In this case it follows
= badsubseq(lasts (*ws∗*(*w∗a*)))*,*
insertforest(*f, w, a*) = forest (*ws∗*(*w∗a*))*.*
By lemma all left-hand components of nodes in insertforest(*f, w, a*) are bad.

Moreover, insertforest(*f, w, a*) = *f *since good(*as, a*) and badsubseq(lasts *ws*) =
*as *= rights (roots (forest *ws*)) imply that indeed at least one node was inserted.

Hence, we obtain
insertforest(*f, w, a*) *≺ f*
An Inductive Version of Nash-Williams’ Minimal-Bad-Sequence Argument
and we may apply IH2 (to insertforest(*f, w, a*) and *ws∗*(*w∗a*)) and concludeacc *A∗ ws∗*(*w∗a*)*.*
This completes the proof of the general assertion. Now, by putting *as *=
[ ]*, f *= [ ] and *ws *= [ ] and the fact that acc*≺ *[] holds by deﬁnition we obtainacc
**Conclusion**

We presented a new constructive proof of Higman’s lemma for arbitrary decid-able well quasiorders in a theory of inductive deﬁnitions. We hope not only thatthis proof gives more insight in the interplay of classical proofs using a minimalbad sequence argument and constructive proofs, but also that this strategy is ex-tendible to other non-constructive theorems, for instance Kruskal’s tree theoremand the so-called extended Kruskal theorem, also known as Kruskal’s theoremwith gap condition. Both have proofs using a minimal-bad-sequence argument(see resp. ), however no constructive proof at all is known forthe latter. Kruskal’s theorem was proved constructively (see for a proofusing ordinal notations or for an inductive reformulation of this proof,and for a proof not requiring decidability). These proofs, however, arequite involved in comparison with the minimal-bad-sequence proof.

We do not claim that our proof of Higman’s lemma is ‘better’ than the other
constructive proofs mentioned in the introduction, but, as already stated, it usesa diﬀerent combinatorial idea, hence results in another algorithm. An analysisof these diﬀerent algorithms is still missing and could give rise to an interestingcase study in machine supported theorem proving.

**Acknowledgment**

I am grateful to Ulrich Berger, Thierry Coquand, and the referees for theirhelpful comments and suggestions on this article, and particularly I would liketo thank Daniel Fridlender for valuable discussions during his Munich visit inJune 2000. The idea to use a tree structure is due to him.

**References**

Thierry Coquand and Daniel Fridlender. A proof of Higman’s lemma by struc-tural induction, 1994.

Daniel Fridlender. *Higman’s Lemma in Type Theory*. PhD thesis, ChalmersUniversity of Technology and University of G¨
Hig52. Graham Higman. Ordering by divisibility in abstract algebras. *Proc. London*
*Math. Soc.*, 2:326–336, 1952.

Mar96. Alberto Marcone. On the logical strength of Nash-Williams’ theorem on trans-
ﬁnite sequences. In: Logic: from Foundations to Applications; European logiccolloquium, pp. 327–351, 1996.

MR90. Chetan R. Murthy and James R. Russell. A Constructive proof of Higman’s
Lemma. In Proc. Fifth Symp. on Logic in Comp. Science, pp. 257–267, 1990.

Mur91. Chetan R. Murthy. An Evaluation Semantics for Classical Proofs. In Proc.

Sixth Symp. on Logic in Computer Science, pp. 96–109, 1991.

NW63. Crispin St. J. A. Nash-Williams. On well-quasi-ordering ﬁnite trees. *Proc.*
*Cambridge Phil. Soc.*, 59:833–835, 1963.

RW93. Michael Rathjen and Andreas Weiermann. Proof–theoretic investigations on
Kruskal’s theorem. *Annals of Pure and Applied Logic*, 60:49–88, 1993.

Fred Richman and Gabriel Stolzenberg. Well Quasi–Ordered Sets. *Advancesin Math.*, 97:145–153, 1993.

Monika Seisenberger. Kruskal’s tree theorem in a constructive theory of induc-tive deﬁnitions In: Reuniting the Antipodes -Constructive and NonstandardViews of the Continuum. Synthese Library, Kluwer, Dordrecht, forthcoming.

utte and Stephen G. Simpson. Ein in der reinen Zahlentheorie un-
*Mathematische Logik und Grundlagenforschung*, 25:75–89, 1985.

Sim85. Stephen G. Simpson. Nonprovability of certain combinatorial properties of
ﬁnite trees. In L.A. Harrington, et al., eds., *Harvey Friedman’s Research on theFoundations of Mathematics*, pp. 87–117. North–Holland, Amsterdam, 1985.

Sch79. Diana Schmidt. Well-orderings and their maximal order types, 1979. Habili-
tationsschrift, Mathematisches Institut der Universit¨
Wim Veldman. An intuitionistic proof of Kruskal’s Theorem. Report no. 0017,Department of Mathematics, University of Nijmegen, 2000.

Source: http://cs.au.dk/~danher/Papers/SeisenbNWHL.pdf

IATA Dangerous Goods Regulations ADDENDUM II Users of the IATA Dangerous Goods Regulations are asked to note the following amendments and corrections to the 54th Edition, effective from 1 January 2013. Where appropriate, changes or amendments to existing text have been highlighted (in yellow - PDF or grey - hardcopy) to help identify the change or amendment. New or Amended Operator Vari

Leila Dargahi Personal Information Date of Birth: 10/31/1979 Place of Birth: Tehran Nationality: Iranian Marital status: Single Address for correspondence Neuroscience Research Center Shahid Beheshti University of Medical Sciences Tehran, Iran Tel: ( +98-21) 22 42 97 68 Fax: ( +98-21) 22 43 20 47 Mobile: ( +98-912) 506 99 30 e-mai Educ