This web-page contains links to files needed to verify the correctness of some parts of the proof of the main result of the paper "Cyclic Coloring of Plane Graphs with Maximum Face Size 16 and 17" authored by Zdeněk Dvořák, Michael Hebdige, Filip Hlásek, Daniel Kráľ and Jonathan Noel. The paper is available as arXiv:1603:06722.
The following three programs were used to verify the correctness of the proof.
The first two programs were used to verify the reducibility of the configurations. Each of them expects the description the configuration to reduce and its replacement on standard input. The format of the input is described in the paper, and the input files for all the configurations can be downloaded using links below or directly from the directory inputs.
The third program was used to verify the correctness of the discharging procedure. The rules are described in the file RuleValues.lhs (this file is needed to compile the program). The initial setting is to check the correctness of the discharging procedure for Delta*=16, and the correctness of discharging procedure for Delta*=17 can be checked after modifying the constant deltaStar in the file. The program can also be compiled using LaTeX (with listings package) to produce a detailed description of the discharging rules, which can be downloaded as a pdf file here.
largeface has size Delta*-1 and the other Delta*
largefaces have size Delta*-1
largeface has size Delta*-2 and the other Delta*-1
largefaces have size Delta*-2