A Locale for Minimal Bad Sequences

Christian Sternagel

Isabelle Users Workshop (IUW 2012), 2012.


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.


  PDF  |    arXiv


author = "Christian Sternagel",
title = "A Locale for Minimal Bad Sequences",
booktitle = "Isabelle Users Workshop",
year = 2012
Nach oben scrollen