inductive ShortTree : Type

A concrete encoding of the data of a short augmented form: a finite list of Left options, a finite list of Right options, and two tombstone bits. As an inductive type in Type 0, it is Small.{u} for every u.

• mk (L R : List ShortTree) (tL tR : Bool) : ShortTree

@[irreducible]

noncomputable def ShortTree.toForm : ShortTree → AugmentedForm

Interpret a ShortTree as an augmented form.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ShortTree.moves_toForm (p : Player) (L R : List ShortTree) (tL tR : Bool) : Moves.moves p (mk L R tL tR).toForm = toForm '' {y : ShortTree | y ∈ Player.cases L R p}

@[simp]

theorem ShortTree.hasTombstone_toForm (p : Player) (L R : List ShortTree) (tL tR : Bool) : AugmentedForm.hasTombstone p (mk L R tL tR).toForm = (Player.cases tL tR p = true)

theorem ShortTree.exists_list_image (S : Set AugmentedForm) (hfin : S.Finite) (h_ext : ∀ y ∈ S, ∃ (t : ShortTree), t.toForm = y) : ∃ (L : List ShortTree), toForm '' {y : ShortTree | y ∈ L} = S

Any finite set of augmented forms, each of which is in the range of toForm, is the image under toForm of (the set of members of) some list.

theorem ShortTree.isShort_mem_range_toForm {x : AugmentedForm} (h_isShort : Form.IsShort x) : ∃ (t : ShortTree), t.toForm = x

Every short augmented form is in the range of toForm.

instance smallSetOfIsShort : Small.{u, u + 1} ↑{x : AugmentedForm | Form.IsShort x}

The set of all short augmented forms definable in u is u-small.