A Locale for Minimal Bad Sequences
arXiv:1208.1366
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.
7 pages, Isabelle Users Workshop 2012