A Locale for Minimal Bad Sequences
Logic in Computer Science
2012-08-08 v1
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.
Cite
@article{arxiv.1208.1366,
title = {A Locale for Minimal Bad Sequences},
author = {Christian Sternagel},
journal= {arXiv preprint arXiv:1208.1366},
year = {2012}
}
Comments
7 pages, Isabelle Users Workshop 2012