# Help Mr. Blass Prove His Theorem!

## What is happening? (for nerds)

A non-empty binary tree is either made of a single node (the root) or is determined by the two trees below the root.
This means that, as a type, the type T of binary trees satisfies the "equation" T=1+T2.
It can be checked that, as an equation concerning complex numbers, this equation has sixth roots of unity as its solutions.
This indicates that, in some way, we may expect to have T=T7.
This actually holds for trees, but a proof of the isomorphism can't involve any minus sign, since types can't be substracted.
In other words, we have to work in the semi-ring ℕ[T]/(T=1+T2), and we wish to prove T=T7.

This game is related to this problem in the following way:

• The states of the game correspond to polynomials in T whose coefficients (the number of disks on each rod) are nonnegative integers.
• The initial state of the game corresponds to the polynomial T, i.e. the type of trees.
• The final state, which the player tries to reach, corresponds to the polynomial T7, i.e. the type of septuples of trees.
• Each join is an application of the rule 1+T2 → T (as well as T+T3 → T2, etc.).
• Each split is an application of the "backwards" rule T → 1+T2 (etc.)

This means that every move in this game corresponds to a completely explicit isomorphism of types.
By reaching the state corresponding to the polynomial T7, the player demonstrates a result, made famous by Andreas Blass:
The type T of binary trees is "very explicitly" isomorphic to the type T7 of septuples of trees.

Note that, as a player, you're making your own proof of the result when playing this game.
Different players will construct different bijections...
This is a fun way to solve the computational part of the theorem!

Here is a link to the famous paper "Seven Trees in One" by Andreas Blass, on the arXiv: https://arxiv.org/pdf/math/9405205.

Game by Béranger Seguin, december 2021.
A funnier version of the game ;). The (dirty) Python code used to prove that 18 moves are necessary.