Abstract

We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman's lemma and Kruskal's tree theorem.

BibTeX

@inproceedings{CS-IUW12a,
  author      = "Christian Sternagel",
  title       = "A Locale for Minimal Bad Sequences",
  booktitle   = "Isabelle Users Workshop",
  year        = 2012
}