最小坏序列的 Locale
计算机科学中的逻辑
2012-08-08 v1
摘要
我们提出了一个 locale，它抽象了构建最小坏序列所需的必要要素，这是 Higman 引理和 Kruskal 树定理的经典证明中所要求的。
引用
@article{arxiv.1208.1366,
title = {A Locale for Minimal Bad Sequences},
author = {Christian Sternagel},
journal= {arXiv preprint arXiv:1208.1366},
year = {2012}
}
备注
7 pages, Isabelle Users Workshop 2012