A Locale for Minimal Bad Sequences

TL;DR

This paper introduces a locale framework that simplifies the construction of minimal bad sequences, crucial for proofs of Higman's lemma and Kruskal's tree theorem.

Contribution

It provides a new abstract locale that captures the essential components for minimal bad sequence construction, streamlining classical proof techniques.

Findings

Defines a novel locale for minimal bad sequences

Simplifies proofs of Higman's lemma and Kruskal's theorem

Facilitates future theoretical developments in well-quasi-orderings

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.