cl-banner

A Locale for Minimal Bad Sequences

Christian Sternagel

Isabelle Users Workshop (IUW 2012), 2012.

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.

 

  PDF  |    arXiv

BibTeX 

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