\( \newcommand\norm[1]{\lvert\lvert#1\rvert\rvert} \newcommand\epi{\bar{\pi}} \newcommand\esigma{\bar{\sigma}} \newcommand\spi{{\esigma}{\epi}^{-1}} \)

Proof structure

The case analysis is performed by extending the configurations that do not allow application of $\frac{11}{8}$-sequences; or presenting it, case a $\frac{11}{8}$-sequence exists.

Note that several configurations are equivalent under circular shifts and mirroring. When performing computations, the proof generator only takes one representative of a set of equivalent configurations, called canonical configuration. This configuration is selected as the one with the least computed hash code, among its equivalent ones.

Each generated configuration has its own HTML file, which can be either a file presenting a $\frac{11}{8}$-sequence or a list of all possible extensions of it.

It is important to note that, although graphs are drawn in the HTML files, the method employed in our work do not rely on them. We have decided to present the graphs only to facilitate the understanding of the proof for the readers used to the formalisms based on the cycle graph. For $1 \leq i \leq n+1$, the black edge $i$ is relabeled to $i-1$.

Extension files

The extension file starts presenting a cycle graph corresponding to the analysed configuration. Then we present its hash code and a list containing the indices of its open gates. The signature of the configuration is presented. The signature is computed first assigning a label (an integer value) to each cycle in the configuration, according to the order of appearance of its symbols in $\epi$. Then, we map each symbol of $\epi$ to the label of the configuration cycle which contains that symbol. In case of oriented cycles, we add to the mapped value, a decimal corresponding to the ordinal position of the symbol in $\epi$. Then, the 3-norm is presented.

Next, the extensions grouped by Type are presented. If an extension type is not applicable to a configuration, then the associated Type column is empty. Each extension starts with the indices (a, b and c) where the new symbols were inserted into the extended configuration. Then, the file tells if the extension is either BAD or GOOD, highlighted in red and green, respectively. Bad extensions do not allow the application of $\frac{11}{8}$-sequences, while the good ones do. This information is followed by the hash code, the $3$-norm and the signature of the extension. Then, a link with the new configuration generated by the direct insertion of new the symbols into the extended configuration (and not its canonical representative) is presented. Clicking this link opens a popup window with its associated graph.

Finally, a link to the canonical configuration of the extension allows the reader to visualise either a $\frac{11}{8}$-sequence file, case the extension is good; or another extension file, otherwise.

$\frac{11}{8}$-sequence files

The $\frac{11}{8}$-sequence file first presents a graph of the configuration. Then, for each transposition $\tau_i$, in the sequence, represented as a $3$-cycle, it shows $\tau_i$, the permutation $\Gamma{\tau_1}^{-1}\dots{\tau_i}^{-1}$ and the graph corresponding to $\Gamma{\tau_1}^{-1}\dots{\tau_i}^{-1}$, where $\Gamma$ is the configuration being presented.