main page

    The Syntax of the Generated Case Analysis

    The easiest way of understanding the syntax of the generated proof is to read this section and at the same time browse the web interface. The case analysis has been generated by (1) extending configurations that do not have a sorting and (2) by giving the sorting for those that have. A straight forward implementation of the program that does not take into account that several configurations are equivalent under circular shifts and mirroring would take months to run. To avoid this we have defined one of the configurations that are equivalent under circular shifts and mirroring to be canonical. (The canonical configuration is selected to be the one with least hash value using some hash function.) Therefore every configuration is transformed into its canonical form before further processing. Every configuration has a separate file and depending on the configuration either the file contains a sorting or a list of all extensions of it. Every configuration is represented by its cycles. Each cycle is represented by the positions of its black edges when read by following the black edges counter clock-wise.

    Extensions

    Every file for configurations without a sorting starts with an image showing the configuration. Thereafter there are three lines describing the configuration itself; the configuration and its open gates. E.g. the three lines below describe the unoriented intersecting pair where numBE is the number of black edges, numOCy is the number of odd cycles, and every cycle is preceded by its length: 
    Configuration    numBE = 6   numOCy = 2  hVal = 658
[3](0 3 1)[3](2 5 4)
OPEN GATES: #2 {1,5}
    After this comes the listing of all sufficient extensions of the configuration with links to their canonical representations. Below is an excerpt from extensions of the two intersecting cycles. The first extension, which does not have a sorting, is given by adding a cycle before positions 1, 0, and 4. The second extension, which has a sorting, is given by adding a cycle before positions 1, 0, and 5. Note that since the open gate in position 1 is closed by both extensions the new configurations are sufficient. 
    ------------
open = 1 a = 0 b = 4
Configuration    numBE = 9   numOCy = 3  hVal = 948238
[3](0 6 2)[3](1 5 3)[3](4 8 7)
canonical representation
Configuration    numBE = 9   numOCy = 3  hVal = 231531
[3](8 6 2)[3](7 5 3)[3](4 1 0)
BAD EXTENSION
View Canonical Extension [3](0_4_1)[3](2_8_6)[3](3_7_5).html
------------
open = 1 a = 0 b = 5
Configuration    numBE = 9   numOCy = 3  hVal = 948336
[3](0 7 2)[3](1 5 3)[3](4 8 6)
canonical representation
Configuration    numBE = 9   numOCy = 3  hVal = 384384
[3](1 8 3)[3](2 6 4)[3](5 0 7)
GOOD EXTENSION
View sorting [3](0_7_5)[3](1_8_3)[3](2_6_4).html
------------

    Sorting

    Every file for configurations with a sorting simply contains the sorting. Below is the file for the second extension described above. Each move is described by the black edges it touches. In the example below the first move touches edges 4, 5, and 6, and is a 0-move. 
    HAS SORTING
Configuration    numBE = 9   numOCy = 3  hVal = 384384
[3](1 8 3)[3](2 6 4)[3](5 0 7)
0:   a = 4   b = 5   c = 6   move_type = 0
Configuration numBE = 9   numOCy = 3  hVal = 380559
[3](1 8 3)[1](5)[5](6 0 7 4 2)
1:   a = 0 b = 2   c = 6   move_type = 2
Configuration    numBE = 9   numOCy = 5  hVal = 1192915
[3](5 8 1)[1](3)[3](0 7 2)[1](6)[1](4)
2:   a = 1   b = 5   c = 8 move_type = 2
Configuration    numBE = 9   numOCy = 7  hVal = 1876031
[1](1)[1](6)[3](0 3 5)[1](2)[1](7)[1](8)[1](4)
3:   a = 0