# Termination of a hydra game #

This file deals with the following version of the hydra game: each head of the hydra is
labelled by an element in a type `α`

, and when you cut off one head with label `a`

, it
grows back an arbitrary but finite number of heads, all labelled by elements smaller than
`a`

with respect to a well-founded relation `r`

on `α`

. We show that no matter how (in
what order) you choose cut off the heads, the game always terminates, i.e. all heads will
eventually be cut off (but of course it can last arbitrarily long, i.e. takes an
arbitrary finite number of steps).

This result is stated as the well-foundedness of the `CutExpand`

relation defined in
this file: we model the heads of the hydra as a multiset of elements of `α`

, and the
valid "moves" of the game are modelled by the relation `CutExpand r`

on `Multiset α`

:
`CutExpand r s' s`

is true iff `s'`

is obtained by removing one head `a ∈ s`

and
adding back an arbitrary multiset `t`

of heads such that all `a' ∈ t`

satisfy `r a' a`

.

We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.

TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz) hydras, and prove their well-foundedness.

The relation that specifies valid moves in our hydra game. `CutExpand r s' s`

means that `s'`

is obtained by removing one head `a ∈ s`

and adding back an arbitrary
multiset `t`

of heads such that all `a' ∈ t`

satisfy `r a' a`

.

This is most directly translated into `s' = s.erase a + t`

, but `Multiset.erase`

requires
`DecidableEq α`

, so we use the equivalent condition `s' + {a} = s + t`

instead, which
is also easier to verify for explicit multisets `s'`

, `s`

and `t`

.

We also don't include the condition `a ∈ s`

because `s' + {a} = s + t`

already
guarantees `a ∈ s + t`

, and if `r`

is irreflexive then `a ∉ t`

, which is the
case when `r`

is well-founded, the case we are primarily interested in.

The lemma `Relation.cutExpand_iff`

below converts between this convenient definition
and the direct translation when `r`

is irreflexive.

## Instances For

For any relation `r`

on `α`

, multiset addition `Multiset α × Multiset α → Multiset α`

is a
fibration between the game sum of `CutExpand r`

with itself and `CutExpand r`

itself.

A multiset is accessible under `CutExpand`

if all its singleton subsets are,
assuming `r`

is irreflexive.

A singleton `{a}`

is accessible under `CutExpand r`

if `a`

is accessible under `r`

,
assuming `r`

is irreflexive.

`CutExpand r`

is well-founded when `r`

is.