10.6092/issn.1972-5787/4213
This article presents the first formalization of Kurskal's tree theorem in aproof assistant. The Isabelle/HOL development is along the lines of Nash-Williams' original minimal bad sequence argument for proving the treetheorem. Along the way, proofs of Dickson's lemma and Higman's lemma, as well as some technical details of the formalization are discussed.
application/pdf
1972-5787
4213
1
en
Christian Sternagel
Journal of Formalized Reasoning
minimal bad sequences
Certified Kruskal's Tree Theorem
Text.Serial.Journal
https://jfr.unibo.it/
7
Articles
2014-07-17
2014-02-28
2014-07-17
2016-01-29
45-62
JFR
Christian Sternagel
2014/07/17
10.6092/issn.1972-5787/4213
45
University of Innsbruck
1972-5787
1
minimal bad sequences
en
62
Certified Kruskal's Tree Theorem
https://jfr.unibo.it/article/download/4213/3898
7
Certified Kruskal’s Tree Theorem
CHRISTIAN STERNAGEL
University of Innsbruck, Austria


This article presents the first formalization of Kurskal’s tree theorem in a proof assistant. The
Isabelle/HOL development is along the lines of Nash-Williams’ original minimal bad sequence
argument for proving the tree theorem. Along the way, proofs of Dickson’s lemma and Higman’s
lemma, as well as some technical details of the formalization are discussed.




1.   INTRODUCTION
Termination is a key ingredient for total correctness of programs and thus key
to program verification. Instead of focusing on a specific programming language,
termination is typically considered in a more abstract setting. In this respect,
one of the most studied models of computation is term rewriting, as confirmed by
the many automatic tools that are available nowadays (e.g., AProVE [GSKT06],
Ci ME [CCF+ 11], Matchbox [Wal04], MU-TERM [AGLNM11], TTT2 [KSZM09], and
VMTL [SG09]; to name a few). A central task in this area is to synthesize well-
founded relations. Often this is done incrementally, e.g., a given well-founded re-
lation is extended to a bigger structure, like sets, multisets, lists, etc. Since this
is not always easy, there is interest in stronger conditions than well-foundedness
that preserve well-foundedness when extending a given order to bigger structures
in more cases. To illustrate the issue, consider the following example.
  Example 1.1. Given a quasi-order ≤ and two sets A and B, write A ≤+ B
whenever for every a ∈ A there is some b ∈ B such that a ≤ b. In other words,
B majorizes A element-wise. One might ask whether the strict part of ≤+ , i.e.,
<+ = ≤+ \ ≥+ , is well-founded whenever the strict part of ≤ is. The following
counterexample shows that this is not the case. Take ≥d to denote the divisibility
order on natural numbers, i.e, m ≥d n whenever there is a natural number k such
that k · n = m. Note that the strict part of ≥d is well-founded but allows for infinite
antichains, e.g., the sequence p1 , p2 , p3 , . . . of all prime numbers in increasing order.
Now let Pi denote the set of all prime numbers starting from the first i-th, i.e.,
Pi = {pk }k≥i . Then we obtain the strictly decreasing sequence
     P1 > +      +      +
          d P 2 >d P 3 >d · · ·

showing that >d is not well-founded.
It turns out that by preventing infinite antichains, one can obtain well-foundedness
of (the strict part of) ≤+ , i.e., when the given quasi-order ≤ does not allow for
infinite antichains and its strict part is well-founded, then so is the strict part of
≤+ . An order satisfying these two conditions (or several equivalent ones) is called
a well-quasi-order (wqo for short).

This research was supported by the Austrian Science Fund (FWF) project J3202.

                                       Journal of Formalized Reasoning Vol. 7, No. 1, 2014, Pages 45–62.
46     ·        Christian Sternagel

  A famous result of wqo theory is Kruskal’s tree theorem [Kru60] (sometimes
called the tree theorem or Kruskal’s theorem in the following).
   Kruskal’s Tree Theorem. Whenever a set A is well-quasi-ordered by a rela-
tion , then the set of finite trees over A is well-quasi-ordered by homeomorphic
embedding w.r.t. .
Its usefulness for termination proving was first shown by Dershowitz [Der79, Der82],
who employed simplification orders – a class of reduction orders for which well-
foundedness follows from Kruskal’s theorem.
   Nash-Williams gave a short and elegant proof of the tree theorem [NW63], where
he first established what is now known as the minimal bad sequence argument:
first assume the existence of a minimal “bad” infinite sequence of elements, then
construct an even smaller “bad” infinite sequence, thus contradicting minimality
and proving well-quasi-orderedness (since the definition of wqo requires all infinite
sequences of elements to be “good”).
   Besides the minimal bad sequence argument, Nash-Williams’ work [NW63] con-
tains proofs of Dickson’s lemma [Dic13] (if A and B are well-quasi-ordered, then so
is the Cartesian product A × B) and a variant of Higman’s lemma [Hig52] (if A is
well-quasi-ordered, then so is the set of finite subsets of A), where the latter also
incorporates an instance of the minimal bad sequence argument.
   The work at hand constitutes a formalization along the lines of Nash-Williams’
original proofs in the proof assistant Isabelle [NPW02].1 His argumentation is
short (in fact, Nash-Williams’ paper consists of only two and a half pages in total)
and elegant (which was also the main reason for basing the formalization on his
work). However, formalizations using proof assistants typically require us to be
more rigorous than with pen and paper. Thus, the formalization is more detailed
in places, which results in somewhat longer (about two thousand lines of Isabelle/
HOL theories) proofs. In this article, a high-level overview of the formalization is
given. The full development is part of the Archive of Formal Proofs [Ste12b].
   Contributions. This article is a reworked version of an earlier account by the au-
thor [Ste13]. To the best of the author’s knowledge, the presented work constitutes
the first unrestricted formalization of Higman’s lemma in Isabelle/HOL as well as
the first formalization of Kruskal’s tree theorem ever. Both are important combi-
natorial results with applications in rewriting theory. For example, the theory of
simplification orders [Der82, MZ97] was formalized – on top of the presented work –
as part of IsaFoR,2 where it is applied to show well-foundedness of the Knuth-Bendix
order [ST13].
   Moreover, the author believes that besides their high trustworthiness, formaliza-
tions of existing mathematical results are also of archival and educational value.
Especially since a formalization contains all non-trivial steps of a proof. No doubt,
more often than not, those steps were already conducted in the minds of the original
proof authors. However, when the original author writes down a proof in condensed
form for publishing, some of the steps may get lost. If, much later, another person

1 Available   from http://isabelle.in.tum.de (try Isabelle/jEdit for browsing).
2 http://cl-informatik.uibk.ac.at/software/ceta/



Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                            Certified Kruskal’s Tree Theorem         ·     47

tries to understand the proof, there may be some mental gaps (or in the worst case
even errors).
   Finally, formalizations are often hard to read for non-experts (but note that the
Isar language for Isabelle [Wen02] is a huge improvement in that respect). Thus,
the author hopes that this high-level overview makes the presented formalization
more accessible.
   Comparison to Previous Work. In my previous work [Ste13] the focus was on
following Nash-Williams’ original argumentation as close as possible. With hind-
sight this turned out to pose unnecessary complications in some proofs. However,
it is always easier to say which of two variants of a proof is better suited for mech-
anization after formalizing both. By slightly deviating from the original proofs and
starting from a crucial fact about homogeneous subsequences (e.g., presented by
Marc Bezem [Ter03, Appendix 5]) I was able to significantly simplify three parts of
the development compared to my previous work: the construction of minimal bad
sequences, the proof of Higman’s lemma, and the proof of the tree theorem.
   A more detailed comparison to my previous work can be found at the end of
every section whose corresponding formalization changed significantly.
   Overview. The remainder is structured as follows. In Section 2, necessary prelim-
inaries are covered. Then, in Section 3, a crucial fact about almost-full relations is
discussed, which will be useful for many of the later proofs. The next four sections
present a formalization of Dickson’s lemma, in Section 4; a general construction of
minimal bad sequences, in Section 5; a formalization of Higman’s lemma, in Sec-
tion 6; and ultimately, a formalization of Kruskal’s tree theorem, in Section 7. Some
example instances of finite tree data types are discussed in Section 8. Finally, the
paper concludes in Section 9, where also applications are sketched, and future as
well as related work is discussed.

2.   PRELIMINARIES
Throughout this article, standard mathematical notation is used as far as possible.
However, additionally some Isabelle specific notation is employed, since Isabelle’s
document preparation facilities were used for typesetting all lemmas and theorems
(in the words of Haftmann et al. [HKNS13]: no typos, no omissions, no sweat; alas,
this does not extend to the regular text). Thus, some explanation might be in
order.
   Isabelle/HOL is a higher-order logic based on the simply-typed lambda calculus.
Thus, every term has a type, where Greek letters α, β, γ, . . . are used for type
variables; and type constructors like nat for natural numbers, α ⇒ β for the function
space, α × β for ordered pairs, α set for sets, and α list for finite lists. Type
constraints are written t::τ and denote that term t is of type τ . As usual for
lambda calculi, function application is denoted by juxtaposition, i.e., f x denotes
the application of function f to the argument x. The type α ⇒ α ⇒ bool is used
to encode binary relations.
   The following constants from Isabelle/HOL’s library are freely used in the re-
mainder: ◦::(α ⇒ β) ⇒ (γ ⇒ α) ⇒ γ ⇒ β, where f ◦ g denotes the functional
                                                      def
composition of the two functions f and g, i.e., f ◦ g = λx . f (g x ), and sometimes f ϕ
is used instead of f ◦ ϕ for brevity (especially when f denotes an infinite sequence
                                          Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
48     ·     Christian Sternagel

and ϕ is an index-mapping, i.e., a function from the natural numbers to the natural
numbers); fst::α × β ⇒ α and snd ::α × β ⇒ β extract the first and second com-
ponent of a pair, respectively; set::α list ⇒ α set, where set xs is the set of elements
occurring in the list xs; []::α list, the empty list; ·::α ⇒ α list ⇒ α list, where x · xs
denotes adding the element x in front of the list xs; and @::α list ⇒ α list ⇒ α list,
where xs @ ys denotes the concatenation of the two lists xs and ys. Note that since
· and @ are both right-associative and have the same priority, xs @ y · ys is the
same as xs @ (y·ys) and denotes a list that is constructed by inserting the element
y between those of xs and ys.                                                           V
   When stating formulas, sometimes Isabelle specific notation is used. Then,
denotes universal quantification and =⇒ (right-associative) implication. Moreover,
nested implication, like A =⇒ B =⇒ C, is abbreviated to [[A; B ]] =⇒ C .
   Let  be a binary relation and A a set. The relation  is reflexive on A, written
refl A (), if and only if ∀ x ∈A. x  x ; and transitive on A, written trans A (), if
and only if ∀ x ∈A. ∀ y∈A. ∀ z ∈A. x  y ∧ y  z −→ x  z .
   An infinite sequence over elements of type α is represented by a function f of
type nat ⇒ α. The set of all infinite sequences over elements from a set A is denoted
by Aω . A binary relation  is transitive on a sequence f, written trans f (), if and
only if ∀ i j . i < j −→ f i  f j . Note that <::nat ⇒ nat ⇒ bool is transitive on
an index-mapping ϕ if and only if ϕ is a strictly monotone mapping from natural
numbers to natural numbers. Thus, for every f and strictly monotone ϕ, f ϕ is a
subsequence of f whose elements are in the same relative order.
   A sequence f is good w.r.t. a relation , written good  (f ), if and only if there
are indices i < j such that f i  f j. A sequence that is not good, is called bad.
   The author follows Veldman [Vel04] and Vytiniotis et al. in basing wqos on
almost-full relations (which are basically wqos without transitivity). The main
reason for doing so, is that all the properties of interest also hold for almost-full
relations and are easily extended to wqos.
   The relation  is almost-full on A, written af A (), if and only if all infinite
sequences over elements of A are good, i.e., ∀ f ∈Aω . good  (f ). Note that every
almost-full relation is necessarily reflexive: just take an infinite sequence f that
repeats an arbitrary element a ∈ A ad infinitum, then reflexivity trivially follows
from the definitions of almost-full and good, i.e., there are i < j such that f i  f j
and thus a  a.
   Let  be almost-full on A. If in addition  is transitive on A, then  is a
wqo on A (or A is well-quasi-ordered by ), written wqoA (). In the literature,
several equivalent definitions for wqos are used. One of them, also mentioned in
the introduction, is that a wqo is a quasi-order that does not allow for infinite
antichains and whose strict part is well-founded (see theory Well-Quasi-Orders for
other definitions and equivalence proofs). Here, an infinite antichain f is an infinite
sequence such that every two elements at disjoint positions are incomparable, i.e.,
∀ i j . i < j −→ f i 6 f j ∧ f j 6 f i.

3.   HOMOGENEOUS SEQUENCES
While the definition of almost-full relations just requires that in every infinite se-
quence there are two elements such that the former is smaller than or equal to the
latter, it can be shown that every infinite sequence contains a subsequence on which
Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                            Certified Kruskal’s Tree Theorem         ·     49

 is transitive. (In the literature, such sequences are called homogeneous [Ter03].)
In some cases, this result allows us to obtain transitivity for free (and hence prove
several results already for almost-full relations rather than wqos).
  Before formally stating the above result, let us have a look at the following
variant of Ramsey’s theorem (see Isabelle/HOL’s library, file ~~/src/HOL/Library/
Ramsey.thy) which is used in its proof.
[[infinite Z ; ∀ i ∈Z . ∀ j ∈Z . i 6= j −→ h {i , j } < n]]
=⇒ ∃ I c. I ⊆ Z ∧ infinite I ∧ c < n ∧ (∀ i ∈I . ∀ j ∈I . i 6= j −→ h {i , j } = c)
In words: Let Z be an infinite set and let h be a function that, given a two-element
subset of Z, returns a natural number smaller than n. Then there is an infinite
subset I of Z and a natural number c smaller than n such that h encodes all two-
element subsets of I by c. More abstractly, assume there is an infinite graph with
nodes from Z such that every edge has exactly one of n colors. Then there is an
infinite subgraph with nodes from I and all edges of color c.
   Lemma 3.1. Every infinite sequence f over elements of a set A that is almost-
full w.r.t.  contains a homogeneous subsequence. That is, there is a strictly mono-
tone index-mapping ϕ::nat ⇒ nat such that f ϕ is transitive w.r.t. . In Isabelle:
[[af A (); f ∈ Aω ]] =⇒ ∃ ϕ. ∀ i j . i < j −→ ϕ i < ϕ j ∧ f ϕ i  f ϕ j.
   Proof. Let  be almost-full on A and f ∈ Aω . Then partition the set of two-
element subsets of the natural numbers into the set X = {{i , j } | i < j ∧ f i  f j }
and its complement Y = − X and colorize two-element sets {i , j } of natural num-
bers by 0 (white) and 1 (black ) according to the following function:
                 (
                  0 if {i , j } ∈ X,
    h {i , j } =
                  1 otherwise.
Now Ramsey’s theorem can be applied (since the set of natural numbers is infinite
and there are exactly two colors). Thus, an infinite set I and a color c, such that
for all i 6= j in I the corresponding color h {i , j } is c, are obtained. Since I
is well-ordered, there is a function ϕ::nat ⇒ nat that enumerates its elements in
increasing order, i.e., ϕ i < ϕ j for all i < j. Moreover, h {ϕ i , ϕ j } = c for all
i < j . Consider the following two cases (for arbitrary but fixed i < j ):
  — case (c is white). Then, h {ϕ i , ϕ j } = 0 and thus {ϕ i , ϕ j } ∈ X which
implies f ϕ i  f ϕ j.
  — case (c is black ). Then, h {ϕ i , ϕ j } = 1, and thus {ϕ i , ϕ j } ∈ Y which
implies f ϕ i 6 f ϕ j and thus yields the bad sequence f ϕ , contradicting the fact
that  is almost-full on A.
  Comparison to Previous Work. Also in my previous work Ramsey’s theorem was
employed. However, only to obtain a proof of Dickson’s lemma without transitivity
and not for the more general result about homogeneous subsequences of this section.

4.   DICKSON’S LEMMA
In essence, the presented formalization is about preservation of well-quasi-orderedness
by certain type constructors (Dickson’s lemma for pairs, Higman’s lemma for lists,
                                          Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
50      ·    Christian Sternagel

and the tree theorem for trees). For each of these constructors, a way to extend
the orders on the base types to an order on the newly constructed type is required.
For Dickson’s lemma the following is used:
  Definition 4.1. Given two orders 1 and 2 , the pointwise order on pairs is
                                            def
defined by (a 1 , a 2 ) 1 ×2 (b 1 , b 2 ) = a 1 1 b 1 ∧ a 2 2 b 2 .
     Using Lemma 3.1, Dickson’s lemma for almost-full relations is shown.
  Lemma 4.2. The pointwise combination 1 ×2 of two almost-full relations 1
and 2 on sets A1 and A2 , is almost-full on the Cartesian product A1 × A2 . In
Isabelle: [[af A1 (1 ); af A2 (2 )]] =⇒ af A1 ×A2 (1 ×2 ).
   Proof. Assume af A1 (1 ) and af A2 (2 ). Moreover, to derive a contradiction,
assume ¬ af A1 ×A2 (1 ×2 ). Then there is a sequence f on A1 × A2 which is
bad. Note that fst ◦ f ∈ A1 ω and snd ◦ f ∈ A2 ω . With Lemma 3.1 we obtain a
strictly monotone index-mapping ϕ such that fst (f ϕ i ) 1 fst (f ϕ j ) for all i < j .
Then snd ◦ f ◦ ϕ ∈ A2 ω and thus snd ◦ f ◦ ϕ is good since A2 is almost-full by
assumption. Thus, we obtain indices i < j such that snd (f ϕ i ) 2 snd (f ϕ j ).
In total, we have f ϕ i 1 ×2 f ϕ j which together with ϕ i < ϕ j contradicts the
badness of f.
Lemma 4.2 trivially extends to wqos.
  Dickson’s Lemma. The pointwise combination of two wqos is again a wqo. In
Isabelle: [[wqoA1 (1 ); wqoA2 (2 )]] =⇒ wqoA1 ×A2 (1 ×2 ).
  Proof. Assuming transitivity of 1 on A1 and 2 on A2 , it is trivial to show
transitivity of 1 ×2 on A1 × A2 . With Lemma 4.2, this concludes the proof.
   Comparison to Previous Work. The new proof of Lemma 4.2 for almost-full re-
lations is based on homogeneous subsequences. As before, the effect is that tran-
sitivity on some infinite sequence is obtained without requiring transitivity of the
whole relation.

5.    MINIMAL BAD SEQUENCES
Since the minimal bad sequence argument is needed for Higman’s lemma as well
as Kruskal’s theorem, a general construction that is applicable to both cases is
provided (see theory Minimal-Bad-Sequences for the formal proof development).
To this end, Isabelle/HOL’s locale mechanism is employed which allows us to define
new constants and prove facts using an “interface” of hypothetical constants and
assumptions. As long as the assumptions can be discharged, the new constants and
proven facts can be instantiated to arbitrary special cases.
  Below, the locale mbs which captures the construction of a minimal bad sequence
over elements from a given set is described (early versions, that could be simplified
drastically since, were presented at the Isabelle Users Workshop in 2012 [Ste12a]
and at the 3rd International Conference on Certified Programs and Proofs [Ste13]).
The locale fixes the following constant:
—A set A whose elements are equipped with a size-function |·|::α ⇒ nat.


Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                                  Certified Kruskal’s Tree Theorem         ·     51

(For Isabelle initiates: here |·| refers to the library type class size, which is auto-
matically instantiated for all data types). Since |·| is a well-founded measure, it
makes sense to talk about minimal elements. It turns out that these ingredients
are enough to construct – under the assumption that there is a bad sequence –
a minimal bad sequence. Informally, a bad infinite sequence is a minimal bad se-
quence, when replacing any element by a smaller one, turns it into a good sequence.
To make this more formal, a partial order on bad infinite sequences is introduced.
   Definition 5.1. Infinite sequences over A are partially ordered by the following
relation. An infinite sequence f is considered less than another infinite sequence g,
written f ω g, whenever there is a position i such that the two sequences are equal
for all earlier elements and |f i | < |g i |, i.e., ∃ i . |f i | < |g i | ∧ (∀ j <i . g j = f j ).
The reflexive closure of ω on A is denoted by ω .
In other words, infinite sequences are compared lexicographically w.r.t. the size of
their elements. First note that this order is not well-founded in general.
   Example 5.2. Take the set of strings over the alphabet {a1 , a2 , a3 , . . .}, ordered
by w  v if and only if the set of letters in w is a subset of the set of letters in v.
Moreover, let size of w be its length. Now, consider the infinite descending sequence
of sequences
     A1   = a1 a1  a2    a3    a4       ···
     A2   = a1 a2 a2     a3    a4       ···
     A3   = a1     a2 a3 a3    a4       ···
     A4   = a1     a2    a3 a4 a4       ···
           ..   ..  ..    ..    ..      ..
            .    .   .     .     .         .
that is, Ai = a1 , a2 , a3 , . . . , ai ai , . . .. Obviously all the Ai are bad infinite sequences.
Furthermore, A1 , A2 , A3 , . . . is an infinite decreasing sequence that shows that ω
is not well-founded.
The example shows that we cannot directly obtain a minimal bad sequence by
means of ω . Thus, in the following we will construct a minimal bad sequence by
choosing smallest possible elements from left to right, which is possible since |·| is
well-founded. To this end, we need some auxiliary constructions, e.g., to filter the
set of bad sequences such that only those remain that are equal to a given sequence
up to a certain point.
   Definition 5.3. Two infinite sequences are equal up to position i, when they are
equal for all previous positions. For a set of infinite sequences S over elements of A,
let S fi denote all those elements of S that are equal to f up to position i. Moreover,
let S [i ] denote the “i -th column” of the sequences in S, i.e., the set {f i | f ∈ S }.
Finally, for a subset B of A, let min B denote a minimal element of B w.r.t. its
size (which exists, whenever B is not empty; note however that in general it is not
uniquely determined, thus the use of Hilbert’s choice operator below).
In the formalization min B is defined by
    min B = (SOME x . x ∈ B ∧ (∀ y∈A. |y| < |x | −→ y ∈
                                                      / B ))

                                                Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
52     ·     Christian Sternagel

where SOME x . Q x is Hilbert’s epsilon operator, i.e., it yields a witness x such
that Q x, whenever ∃ x . Q x, and some arbitrary value of the appropriate type,
otherwise. The above definitions are employed to construct an infinite sequence
from a given set of infinite sequences as follows:
   Definition 5.4. Given the set B of all bad infinite sequences over elements of A,
define a new infinite sequence ` (intended to be a lower bound of B w.r.t. ω ) as
follows:
     ` i = min B` [i]
                   i

   That is, ` 0 is a minimal element among the first elements of sequences in B
(since S f0 = S for all sets S and sequences f ); and to obtain the i+1-th element,
first restrict B to those sequences that are equal to ` up to position i+1, and of
the resulting set of sequences take a minimal element among their i+1-th elements.
The well-definedness of the above definition is guaranteed by the fact that to obtain
the i+1-th element, we only have to consult all the previous elements of `.
   The elements of ` satisfy the following properties:
     h ∈ B =⇒ ` i ∈ B `i [i ]                                                     (1)
     [[h ∈ B; y ∈ A; |y| < |` i |]] =⇒ y ∈
                                         /        B `i [i ]                       (2)
That is, under the assumption that there is a bad sequence h, the i -th element of
` is in the i -th column of the sequences of B that are equal to ` up to position i,
and is minimal amongst its elements.
   Of course it has to be shown that ` is indeed a bad infinite sequence.
  Lemma 5.5. If there is at least one bad infinite sequence, then ` is bad. In
Isabelle: h ∈ B =⇒ ` ∈ B.
  Proof. To derive a contradiction, assume that ` is good. Then there are indices
i < j such that ` i  ` j. Moreover, from (1) we obtain ` j ∈ B `j [j ], which means
that there is some bad infinite sequence g in B `j such that g k = ` k for all k ≤ j,
and thus g i  g j. This, in turn, means that g is good and therefore contradicts
the previously derived g ∈ B `j .
The second crucial property of ` is that it is a lower bound of the set B. That is,
every infinite sequence that is strictly smaller than ` is not bad.
   Lemma 5.6. If there is at least one bad infinite sequence, then every infinite
sequence that is strictly smaller than ` w.r.t. ω is good. In Isabelle: h ∈ B =⇒
∀ g. g ω ` −→ g ∈ / B.
  At this point it can be shown that if a relation is not almost-full, then there is a
minimal bad sequence.
  Theorem 5.7. Let  be a relation that is not almost-full on A. Then there is a
minimal bad sequence, i.e., a bad sequence such that all sequences that are strictly
smaller w.r.t. ω are good. In Isabelle: ¬ af A () =⇒ ∃ m∈B. ∀ g. g ω m −→
good  (g).
  Proof. Assume that  is not almost-full. Then there is some sequence h ∈ B.
Together with Lemma 5.5 and Lemma 5.6, we obtain that ` is a minimal bad
sequence.
Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                             Certified Kruskal’s Tree Theorem         ·     53

   Comparison to Previous Work. Instead of basing the mbs locale on some arbi-
trary well-founded and transitive relation (as in [Ste13]), minimality is now fixed to
refer to the size of elements. While this is only a specific instance of the previous
construction, it suffices for all the later proofs.
   Moreover, the construction of a minimal bad sequence could be significantly
simplified by step-wise narrowing down the set of all bad sequences using the notions
of equal up to, filtering sets of infinite sequences w.r.t. a given infinite sequence,
column of a set of infinite sequences, and minimal element of a set (only the first
of which was present in my previous work).

6.   HIGMAN’S LEMMA
Before Higman’s lemma for almost-full relations is stated formally, a construction
that extends a given order on elements to an order on lists is required: homeomorphic
embedding. The set of lists over elements from a set A, written A∗ , is defined
inductively:
                       x ∈A       xs ∈ A∗
     [] ∈ A∗              x · xs ∈ A∗
The size of a list is measured by its length (i.e., number of elements). Homeomorphic
embedding on lists, for a given base order , is defined inductively by the rules
                         xs ∗ ys              xy       xs ∗ ys
        ∗
     []  ys           xs ∗ y · ys                     ∗
                                                x · xs  y · ys
(In this article the notation ∗ is used consistently to denote list-embedding w.r.t.
the base order  and is not to be confused with the reflexive and transitive closure of
a relation.) Intuitively, it might be easier to think about homeomorphic embedding
on lists as follows: a list xs is embedded in a list ys if and only if xs can be obtained
from ys by dropping elements and replacing elements with arbitrary smaller ones
(w.r.t. the base order). An important special case of embedding is =∗ , which is
called the sublist relation. Then, xs =∗ ys if and only if the list xs can be obtained
from the list ys by dropping elements.
   The mbs locale can be instantiated by taking A∗ for its parameter A and the
length of lists as their size. Thus,
¬ af A∗ (∗ ) =⇒ ∃ m∈B. ∀ g. g ω m −→ good ∗ (g)
which allows us to prove Higman’s lemma for almost-full relations.
  Lemma 6.1. Homeomorphic embedding w.r.t. an almost-full relation  on a set
A, is almost-full on the set of finite lists over A. In Isabelle: af A () =⇒ af A∗ (∗ ).
  Proof. Assume af A () but ¬ af A∗ (∗ ), for the sake of a contradiction. Then
there is a minimal bad sequence m. All lists in m are non-empty (since otherwise
m would be good). Hence, there are sequences h and t of heads and tails of m (i.e.,
m i = h i · t i ).
  Clearly, h ∈ Aω and thus, by Lemma 3.1, there is a strictly monotone index-
mapping such that h ϕ is a -homogeneous sequence. Moreover, t ϕ is bad, since
otherwise m would be good.

                                           Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
54      ·    Christian Sternagel

   Let n abbreviate ϕ 0 and c be the combination of the infinite sequences m and
                  def
t, defined by c i = if i < n then m i else t (ϕ (i − n)) (i.e., c is the same as t ϕ ,
but prepended by the first n elements of m). Then c is bad, since otherwise a
contradiction is obtained as follows: Assume c is good. Then there are i < j such
that c i ∗ c j . Now, analyze the following cases:
—case (j < n). Then m i ∗ m j, contradicting the badness of m.
—case (n ≤ i ). Let i 0 = i − n and j 0 = j − n. Then i 0 < j 0 and t ϕ i 0 ∗ t ϕ j 0,
 contradicting badness of t ϕ .
—case (i < n and n ≤ j ). Let j 0 = j − n. Then m i ∗ t (ϕ j 0) (from c i ∗ c j ).
 Moreover, m i ∗ m (ϕ j 0) (by the second clause of the inductive definition of
 embedding). Together with i < ϕ j 0, this contradicts the badness of m.
Thus, c is bad. Furthermore, ∀ i <n. c i = m i and |c n| < |m n|, and thus c is
good (since m is minimal): A contradiction, concluding the proof.
     This result can be easily extended to wqos.
  Higman’s Lemma. Whenever a set A is well-quasi-ordered by a relation ,
then the set of finite lists over A is well-quasi-ordered by homeomorphic embed-
ding w.r.t. ∗ . In Isabelle: wqoA () =⇒ wqoA∗ (∗ ).
  Proof. For transitivity of ∗ (under the assumption that  is transitive), refer
to lemma list-emb-trans in theory Sublist. Together with Lemma 6.1, this yields
Higman’s lemma.
  Comparison to Previous Work. By employing Lemma 3.1, the slightly tedious
reasoning about the non-existence of an infinite bad sequence “of special shape”
(which is also to be found in Nash-Williams’ original proof) could be completely
avoided. This change made it possible to shorten the previous 166-line proof to
more reasonable 66 lines.

7.    THE TREE THEOREM
The tree theorem is for finite trees, what Higman’s lemma is for finite lists. However,
whereas for finite lists, their representation inside Isabelle/HOL is quite unambigu-
ous and the existing data type is generally applicable; this is not so much the case
for finite trees. Consider the following two data types
      datatype α t = Tree α (α t list)
      datatype α t 0 = E | N α (α t 0 list)

or the type of first-order terms

      datatype (α, β) term = Var β | Fun α ((α, β) term list)
also a kind of finite tree (and more importantly, one of the types to which the tree
theorem is applied, in order to formalize the fact that the Knuth-Bendix order is
a simplification order [ST13]). Restricting the tree theorem to a specific data type
would strongly restrict its applicability. Therefore, again Isabelle/HOL’s locale
mechanism is employed. This time, for a locale kruskal-tree that fixes the following
constants (see theory Kruskal for details):
Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                              Certified Kruskal’s Tree Theorem         ·     55

—A set F::(β × nat) set representing the signature over which trees are built.
—A function mk ::β ⇒ α list ⇒ α that is used to construct a finite tree from a
 given node and a given list of finite trees.
—A function root::α ⇒ β × nat that extracts the root node together with its arity
 from a given tree.
—A function args::α ⇒ α list that extracts the list of arguments (direct subtrees)
 from a given tree.
—As well as the set T (F)::α set of well-formed trees w.r.t. the signature F.
These constants are required to satisfy the following assumptions (thereby turning
mk into kind of a data type constructor with extractors root and args):
    [[t ∈ T (F); s ∈ set (args t)]] =⇒ |s| < |t|                                           (F1)
    (f , |ts|) ∈ F =⇒ root (mk f ts) = (f , |ts|)                                          (F2)
    (f , |ts|) ∈ F =⇒ args (mk f ts) = ts                                                  (F3)
    t ∈ T (F) =⇒ mk (fst (root t)) (args t) = t                                            (F4)
    t ∈ T (F) =⇒ root t ∈ F                                                                (F5)
    t ∈ T (F) =⇒ |args t| = snd (root t)                                                   (F6)
    [[t ∈ T (F); s ∈ set (args t)]] =⇒ s ∈ T (F)                                           (F7)
   That is, the size of a direct subtree of a well-formed tree is strictly smaller than the
size of the tree itself (F1); mk is injective when applied to a number of arguments
corresponding to the arity of a node (i.e., [[(f , |ss|) ∈ F; (g, |ts|) ∈ F]] =⇒ (mk f
ss = mk g ts) = (f = g ∧ ss = ts); (F2) and (F3)); and mk, root, and args interact
“as expected” on well-formed trees ((F4), (F5), (F6), and (F7))
   Homeomorphic embedding on (well-formed) finite trees is defined inductively by
the two rules:
    (f , m) ∈ F        |ts| = m       set ts ⊆ T (F)          t ∈ set ts        s emb t
                                     s emb mk f ts
             (f , m) ∈ F       (g, n) ∈ F     |ss| = m      |ts| = n
     set ss ⊆ T (F)      set ts ⊆ T (F)     (f , m)  (g, n)      ss emb ∗ ts
                               mk f ss emb mk g ts
The first rule subsumes what is often called the subterm property (i.e., a proper
subtree of a well-formed tree is also in the embedding relation). The second rule
states that the nodes of a tree may be replaced by smaller ones w.r.t.  and their
arguments by smaller ones w.r.t. list-embedding where the underlying order is emb .
  To instantiate the mbs locale, take T (F) for its parameter A. Thus,
¬ af T (F ) (emb ) =⇒ ∃ m∈B. ∀ g. g ω m −→ good emb (g)
  Finally, the tree theorem for almost-full relations can be stated and proved (see
theory Kruskal for details).
   Theorem 7.1. Homeomorphic embedding w.r.t. an almost-full relation  on a
set F, is almost-full on the set of finite trees over F. In Isabelle: af F () =⇒
af T (F ) (emb )
                                            Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
56         ·   Christian Sternagel

   Proof. Assume that  is almost-full on F but, for the sake of a contradiction,
emb is not almost-full on T (F). Then, by Theorem 5.7, there is a minimal bad
sequence m such that any smaller sequence w.r.t. ω is good. Moreover, there are
sequences r and a of roots and arguments of m (i.e., m i = mk (fst (r i )) (a i )).
Let A denote the set of all trees occurring in a (i.e., the set of arguments of all
m i ).
   Then it is shown that emb is almost-full on A. To this end, suppose the contrary.
Thus, there is a sequence s ∈ Aω which is bad. Let n be the least index such that
there is some element s k that is an argument of m n (i.e., s k ∈ set (a n) for some
k ). Let c be the combination of m and s, defined by
     def
c i = if i < n then m i else s (k + (i − n))
Clearly, c i = m i for all i < n and c i = s (k + (i − n)), otherwise. Then c
is bad, since otherwise a contradiction is obtained as follows: Assume c is good.
Then, there are i < j such that c i emb c j. Now analyze the following cases:
   — case (j < n). Then m i emb m j, contradicting the badness of m.
   — case (n ≤ i ). Let i 0 = k + (i − n) and j 0 = k + (j − n). Then i 0 < j 0 and
s i 0 emb s j 0, contradicting the badness of s.
   — case (i < n and n ≤ j ). Let j 0 = k + (j − n). Then m i emb s j 0.
Thus, there is some index l ≥ n such that s j 0 ∈ set (a l ), which in turn implies
m i emb m l . Together with i < l, this contradicts the badness of m.
Thus term c is bad. Since also c ω m (since c n is and argument of m n), we
obtain the desired af A (emb ).
   Now by, Lemma 6.1 and Lemma 3.1, we obtain a strictly monotone index-
mapping ϕ such that ϕ i < ϕ j and a ϕ i emb ∗ a ϕ j for all i < j. Moreover,
r ϕ i ∈ F for all i and thus there are indices i < j such that r ϕ i  r ϕ j. Together,
this implies m ϕ i emb m ϕ j , contradicting the badness of m.
   Kruskal’s Tree Theorem. Whenever a set F is well-quasi-ordered by a rela-
tion , then the set of finite trees over F is well-quasi-ordered by homeomorphic
embedding w.r.t. emb . In Isabelle: wqoF () =⇒ wqoT (F ) (emb ).
   Proof. By induction on the definition of embedding, it can be shown that emb
is transitive whenever the base order  is. Together with Theorem 7.1 this yields
the tree theorem.
   Notes. As in my previous work [Ste13], the definition of homeomorphic embed-
ding on trees could have ignored arities of nodes and in turn well-formedness of
trees. This would constitute a slightly simpler definition and still allow us to ob-
tain the tree theorem. Moreover, as in my previous work, closure under context
and transitivity could have been built-in. However, note that every extension of
an almost-full relation is again an almost-full relation (an easy consequence of the
definition of almost-full). Thus it seems desirable to have an embedding relation
that is as small as possible. Since the proof of the tree theorem goes through with
the current version, I went with it. But considering arities does not only make
embedding potentially smaller, it is also necessary for some applications as shown
in the next section.
Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                             Certified Kruskal’s Tree Theorem         ·     57

  Comparison to Previous Work. Again, by employing Lemma 3.1, the very te-
dious reasoning about the non-existence of an infinite bad sequence “of special
shape” (which is also to be found in Nash-Williams’ original proof) could be avoided
completely. Thereby shortening the original 188-line proof to 90 lines and, more
importantly, making the argument much simpler.

8.    EXAMPLES
In this section we consider concrete instances of the kruskal-tree locale for the
following data types:
—Rose trees: datatype α tree = Node α (α tree list)
—First-order terms: datatype (α, β) term = Var β | Fun α ((α, β) term list)
—“Arithmetic” expressions involving addition of variables and constants:
 datatype α exp = V α | C nat | Plus (α exp) (α exp)
  For rose trees consider the selector functions node (Node f ts) = (f , |ts|) and
succs (Node f ts) = ts, as well as the inductive set of trees over a given set of
nodes A:
    f ∈A        ∀ t∈set ts. t ∈ trees A
           Node f ts ∈ trees A
The kruskal-tree locale is easily instantiated by
      interpretation kruskal-tree (A × UNIV) N ode node succs (trees A)
and we obtain the following variant of the tree theorem
      wqoA×UNIV () =⇒ wqotrees A (emb ).
However, arities are actually not interesting (since nodes in a rose tree may have
arbitrarily many successors) thus it might be desirable to start from a base order 
on A (instead of A × UNIV). This is easily possible by noting that the full relation
(x  y for all x and y) is a wqo on any set and invoking Dickson’s lemma.
   For first-order terms consider the selector functions root (Fun f ts) = (f , |ts|) and
args (Fun f ts) = ts, as well as the inductively defined set of ground terms over a
signature F:
       (f , n) ∈ F     |ts| = n     ∀ s∈set ts. s ∈ T (F )
                        Fun f ts ∈ T (F )
Again, the kruskal-tree locale is easily instantiated by
      interpretation kruskal-tree F F un root args T (F)
and we obtain the following variant of the tree theorem
      wqoF () =⇒ wqoT (F ) (emb ).
     For arithmetic expressions consider the constructor function
      mk (v x ) [] = V x
      mk (c n) [] = C n
      mk p [a, b] = Plus a b
                                           Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
58      ·    Christian Sternagel

the root selector function
     rt (V x ) = (v x , 0 )
     rt (C n) = (c n, 0 )
     rt (Plus a b) = (p, 2 )
and the argument selector function
     ags (V x ) = []
     ags (C n) = []
     ags (Plus a b) = [a, b]
where
     datatype α symb = v α | c nat | p.
Moreover, consider the inductively defined set of arithmetic expressions:
                                        a ∈ exps     b ∈ exps
     V x ∈ exps       C n ∈ exps           Plus a b ∈ exps
                         def
For the signature Σ = {(v x, 0) | x ≥ 0} ∪ {(c n, 0) | n ≥ 0} ∪ {(p, 2 )} (which
ensures that constructors are applied to the correct number of arguments), the
kruskal-tree locale can be instantiated by
     interpretation kruskal-tree Σ mk rt ags exps
and we obtain the following variant of the tree theorem
     wqoΣ () =⇒ wqoexps (emb ).

9.   CONCLUSIONS AND RELATED WORK
An Isabelle/HOL formalization of three important results from combinatorics was
presented: Dickson’s lemma, Higman’s lemma, and Kruskal’s tree theorem. The
formalized proofs are reasonably simple and the tree theorem is presented in a
general version that is applicable to several instances.
  Parts of the presented formalization were used by Wu et al. [WZU11] to formalize
a proof of: For every language A, the languages of sub- and superstrings of A are
regular. (Details are given in the corresponding journal article [WU14].)
  Moreover, the presented formalization of the tree theorem is employed for a proof
that the Knuth-Bendix order is a simplification order [ST13].
  There are formalizations of Higman’s lemma in Isabelle/HOL by Berghofer [Ber04]
and using other proof assistants by Murthy [Mur90], Fridlender [Fri98], Herbelin
[Her94], Seisenberger [Sei03], and Martı́n-Mateos et al. [MMRRAH11].
  Since Berghofer’s work was also conducted using Isabelle/HOL, some comments
on the relation to the presented work are in order. First note that Berghofer’s
formalization is constructive (based on an earlier proof by Coquand and Fridlender
in an unpublished manuscript entitled A Proof of Higman’s Lemma by Structural
Induction). Furthermore, it is restricted to a two letter alphabet (and Berghofer
notes that “the extension of the proof to an arbitrary finite alphabet is not at all

Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                           Certified Kruskal’s Tree Theorem         ·     59

trivial”). Also noteworthy is that the focus of Berghofer’s work is on program ex-
traction and the computational behavior of the resulting program. In contrast, the
presented work constitutes a formalization of Higman’s lemma without restricting
the alphabet, i.e., the alphabet may be infinite as long as it is equipped with a wqo
(which is always the case for finite alphabets).
   An intuitionistic proof of Kruskal’s tree theorem is presented in [Vel04]. How-
ever, to the best of the author’s knowledge the presented work constitutes the first
formalization of the tree theorem in a proof assistant ever.
   The tree theorem is a special case of the graph minor theorem, which was proved
by Robertson and Seymour in a series of twenty papers [RS83, RS04]. The size
of this (pen and paper) proof alone makes a formalization interesting. However,
an extension of the current proof would constitute significant extra effort and it is
unclear whether the minimal bad sequence argument could be applied at all. Thus,
we leave it as future work.

References
[AGLNM11]       Beatriz Alarcón, Raúl Gutiérrez, Salvador Lucas, and Rafael
                Navarro-Marset. Proving termination properties with MU-TERM.
                In Michael Johnson and Dusko Pavlovic, editors, Proceedings of
                the 13th International Conference on Algebraic Methodology And
                Software Technology, volume 6486 of Lecture Notes in Computer
                Science, pages 201–208. Springer Berlin Heidelberg, 2011. doi:
                10.1007/978-3-642-17796-5_12.
[Ber04]         Stefan Berghofer. A constructive proof of Higman’s lemma in Is-
                abelle. In Stefano Berardi, Mario Coppo, and Ferruccio Dami-
                ani, editors, Proceedings of the 3rd International Workshop on
                Types for Proofs and Programs, volume 3085 of Lecture Notes in
                Computer Science, pages 66–82. Springer Berlin Heidelberg, 2004.
                doi:10.1007/978-3-540-24849-1_5.
[CCF+ 11]       Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons,
                and Xavier Urbain. Automated certified proofs with Ci ME3. In
                Manfred Schmidt-Schauß, editor, Proceedings of the 22nd Inter-
                national Conference on Rewriting Techniques and Applications,
                volume 10 of Leibniz International Proceedings in Informatics
                (LIPIcs), pages 21–30. Schloss Dagstuhl – Leibniz-Zentrum für In-
                formatik, 2011. doi:10.4230/LIPIcs.RTA.2011.21.
[Der79]         Nachum Dershowitz. A note on simplification orderings. In-
                formation Processing Letters, 9(5):212–215, 1979. doi:10.1016/
                0020-0190(79)90071-1.
[Der82]         Nachum Dershowitz. Orderings for term-rewriting systems. The-
                oretical Computer Science, 17(3):279–301, 1982. doi:10.1016/
                0304-3975(82)90026-3.
[Dic13]         Leonard Eugene Dickson. Finiteness of the odd perfect and prim-
                itive abundant numbers with n distinct prime factors. Ameri-
                can Journal of Mathematics, 35(4):413–422, 1913. doi:10.2307/
                2370405.
                                         Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
60     ·     Christian Sternagel

[Fri98]    Daniel Fridlender. Higman’s lemma in type theory. In Eduardo
           Giménez and Christine Paulin-Mohring, editors, Proceedings of the
           1st International Workshop on Types for Proofs and Programs, vol-
           ume 1512 of Lecture Notes in Computer Science, pages 112–133.
           Springer Berlin Heidelberg, 1998. doi:10.1007/BFb0097789.
[GSKT06]   Jürgen Giesl, Peter Schneider-Kamp, and René Thiemann. AProVE
           1.2: Automatic termination proofs in the dependency pair frame-
           work. In Ulrich Furbach and Natarajan Shankar, editors, Proceed-
           ings of the 3rd International Joint Conference on Automated Rea-
           soning, volume 4130, pages 281–286. Springer Berlin Heidelberg,
           2006. doi:10.1007/11814771_24.
[Her94]    Hugo Herbelin. A program from an A-translated impredicative
           proof of Higman’s lemma, 1994. http://coq.inria.fr/pylons/
           contribs/view/HigmanNW/v8.3.
[Hig52]    Graham Higman. Ordering by divisibility in abstract algebras. Pro-
           ceedings of the London Mathematical Society, s3-2(1):326–336, 1952.
           doi:10.1112/plms/s3-2.1.326.
[HKNS13]   Florian Haftmann, Gerwin Klein, Tobias Nipkow, and Nor-
           bert Schirmer.       LATEX sugar for Isabelle documents, 2013.
           http://isabelle.in.tum.de/website-Isabelle2013-2/dist/
           Isabelle2013-2/doc/sugar.pdf.
[Kru60]    Joseph Bernard Kruskal. Well-quasi-ordering, the tree theorem, and
           Vazsonyi’s conjecture. Transactions of the American Mathematical
           Society, 95(2):210–225, 1960. doi:10.2307/1993287.
[KSZM09]   Martin Korp, Christian Sternagel, Harald Zankl, and Aart Middel-
           dorp. Tyrolean Termination Tool 2. In Ralf Treinen, editor, Pro-
           ceedings of the 20th International Conference on Rewriting Tech-
           niques and Applications, volume 5595 of Lecture Notes in Com-
           puter Science, pages 295–304. Springer Berlin Heidelberg, 2009.
           doi:10.1007/978-3-642-02348-4_21.
[MMRRAH11] Francisco Jesús Martı́n-Mateos, José Luis Ruiz-Reina, José Anto-
           nio Alonso, and Marı́a José Hidalgo. Proof pearl: A formal proof
           of Higman’s lemma in ACL2. Journal of Automated Reasoning,
           47(3):229–250, 2011. doi:10.1007/s10817-010-9178-x.
[Mur90]    Chetan R. Murthy. Extracting Constructive Content from Classical
           Proofs. PhD thesis, Cornell University, 1990. http://hdl.handle.
           net/1813/6991.
[MZ97]     Aart Middeldorp and Hans Zantema. Simple termination of rewrite
           systems. Theoretical Computer Science, 175(1):127–158, 1997. doi:
           10.1016/S0304-3975(96)00172-7.
[NPW02]    Tobias Nipkow, Lawrence Charles Paulson, and Markus Wenzel.
           Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume
           2283 of Lecture Notes in Computer Science. Springer Berlin Hei-
           delberg, 2002. doi:10.1007/3-540-45949-9.


Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
                                     Certified Kruskal’s Tree Theorem         ·     61

[NW63]     Crispin St. John Alvah Nash-Williams. On well-quasi-ordering fi-
           nite trees. Proceedings of the Cambridge Philosophical Society,
           59(4):833–835, 1963. doi:10.1017/S0305004100003844.
[RS83]     Neil Robertson and Paul Seymour. Graph minors. i. excluding a
           forest. Journal of Combinatorial Theory, Series B, 35(1):39–61,
           1983. doi:10.1016/0095-8956(83)90079-5.
[RS04]     Neil Robertson and Paul Seymour. Graph minors. xx. wagner’s
           conjecture. Journal of Combinatorial Theory, Series B, 92(2):325–
           357, 2004. doi:10.1016/j.jctb.2004.08.001.
[Sei03]    Monika Seisenberger. On the Constructive Content of Proofs. PhD
           thesis, LMU Munich, 2003. http://nbn-resolving.de/urn:nbn:
           de:bvb:19-16190.
[SG09]     Felix Schernhammer and Bernhard Gramlich. VMTL – a modu-
           lar termination laboratory. In Ralf Treinen, editor, Proceedings
           of the 20th International Conference on Rewriting Techniques and
           Applications, volume 5595 of Lecture Notes in Computer Science,
           pages 285–294. Springer Berlin Heidelberg, 2009. doi:10.1007/
           978-3-642-02348-4_20.
[ST13]     Christian Sternagel and René Thiemann. Formalizing Knuth-
           Bendix orders and Knuth-Bendix completion. In Femke van Raams-
           donk, editor, Proceedings of the 24th International Conference on
           Rewriting Techniques and Applications, volume 21 of Leibniz In-
           ternational Proceedings in Informatics (LIPIcs), pages 287–302.
           Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. doi:
           10.4230/LIPIcs.RTA.2013287.
[Ste12a]   Christian Sternagel. A locale for minimal bad sequences. In Isabelle
           Users Workshop, 2012. arXiv:1208.1366.
[Ste12b]   Christian Sternagel. Well-Quasi-Orders. In Gerwin Klein, To-
           bias Nipkow, and Lawrence Charles Paulson, editors, Archive of
           Formal Proofs. April 2012. http://afp.sf.net/devel-entries/
           Well_Quasi_Orders.shtml.
[Ste13]    Christian Sternagel. Certified Kruskal’s tree theorem. In Georges
           Gonthier and Michael Norrish, editors, Proceedings of the 3rd In-
           ternational Conference on Certified Programs and Proofs, volume
           8307 of Lecture Notes in Computer Science, pages 178–193. Springer
           Berlin Heidelberg, 2013. doi:10.1007/978-3-319-03545-1_12.
[Ter03]    Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts
           Theoret. Comput. Sci. Cambridge Univ. Press, 2003.
[Vel04]    Wim Veldman. An intuitionistic proof of Kruskal’s theorem.
           Archive for Mathematical Logic, 43(2):215–264, 2004. doi:10.
           1007/s00153-003-0207-x.
[Wal04]    Johannes Waldmann. Matchbox: A tool for match-bounded string
           rewriting. In Vincent van Oostrom, editor, Proceedings of the
           15th International Conference on Rewriting Techniques and Ap-
           plications, volume 3091 of Lecture Notes in Computer Science,
                                   Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
62     ·     Christian Sternagel

                   pages 85–94. Springer Berlin Heidelberg, 2004. doi:10.1007/
                   978-3-540-25979-4_6.
[Wen02]            Markus Wenzel. Isabelle/Isar – A Versatile Environment for
                   Human-readable Formal Proof Documents. PhD thesis, Technische
                   Universität München, 2002. http://tumb1.biblio.tu-muenchen.
                   de/publ/diss/in/2002/wenzel.pdf.
[WU14]             Chunhan Wu and Xingyuan Zhang Christian Urban. A formal-
                   isation of the Myhill-Nerode theorem based on regular expres-
                   sions. Journal of Automated Reasoning, pages 1–30, 2014. doi:
                   10.1007/s10817-013-9297-2.
[WZU11]            Chunhan Wu, Xingyuan Zhang, and Christian Urban. The Myhill-
                   Nerode theorem based on regular expressions. In Gerwin Klein,
                   Tobias Nipkow, and Lawrence Charles Paulson, editors, Archive
                   of Formal Proofs. August 2011. http://afp.sf.net/entries/
                   Myhill-Nerode.shtml.




Journal of Formalized Reasoning Vol. 7, No. 1, 2014.
