I was able to verify Skelet’s proofs for these machines… enough.
For posterity, here is a garbage Python script for converting the Closed Transition Graph section of these TMs in particular.
parse_bl_proof.py (8.9 KB)
There shouldn’t be any obstacle to adapting it for other machines, after teaching it to parse “the Special rules” sections or otherwise figure that part out instead of hard-coding it.
Fortunately, it verified every transition in the graphs emitted by Skelet’s program, outputting files in the SymbolicTM format for verification of closure properties.
Unfortunately, the output doesn’t actually pass SymbolicTM’s validation.
Fortunately, my frans_faase_to_dfa utility can translate these output files to MitM-DFA pairs.
Unfortunately, these DFA pairs were definitely wrong.
Fortunately, they were only half-broken: in each case, one side was fine, and the “FAR direct” algorithm was able to complete the proof. I then determinized and reduced to get proper MitM-DFA proofs.
Edited to add: By mistake, the below aren’t good DFA pairs, but rather, best working left- and right-DFA. (The sides each complete to a good FAR solution, and actual MitM-DFA solutions will be given in a later reply.)
Beaver: https://bbchallenge.org/3844064
Left-side DFA transition table: [0, 1, 2, 3, 4, 3, 3, 3, 5, 6, 3, 7, 8, 3, 3, 3, 9, 10, 11, 12, 13, 3, 14, 15, 15, 3, 3, 16, 3, 3, 17, 18, 19, 12, 20, 21, 22, 3, 16, 23, 23, 3, 24, 3, 25, 3, 26, 27, 28, 3, 3, 29, 30, 31, 32, 3, 33, 3, 34, 3, 22, 3, 35, 3, 36, 3, 3, 37, 38, 23, 39, 28, 3, 6, 3, 3, 19, 12, 40, 3, 38, 41, 42, 3, 3, 31]
Right-side DFA transition table: [0, 1, 2, 3, 2, 2, 4, 5, 6, 7, 2, 8, 2, 9, 2, 10, 11, 12, 2, 13, 2, 14, 15, 16, 2, 17, 18, 19, 20, 21, 2, 22, 2, 23, 24, 25, 6, 26, 2, 8, 2, 27, 2, 2 , 2, 3, 2, 28, 15, 29, 2, 17, 2, 10, 2, 2, 30, 31, 2, 32, 33, 34, 27, 35, 2, 14, 2, 1, 2, 10, 36, 5, 6, 29]
Beaver: https://bbchallenge.org/4049716
Left-side DFA transition table: [0, 1, 2, 3, 4, 4, 5, 6, 4, 4, 7, 8, 9, 10, 4, 11, 4, 12, 4, 13, 14, 15, 4, 16, 4, 17, 4, 4, 18, 19, 4, 20, 21, 22, 23, 24, 4, 25, 4, 26, 27, 28, 7, 29, 4, 30, 4, 31, 4, 4, 4, 32, 4, 33, 18, 34, 4, 20, 4, 12, 14, 15, 4, 31, 35, 36, 37, 38, 4, 39, 7, 40, 4, 30, 41, 42, 4, 43, 4, 44, 4, 12, 4, 2, 2, 12, 45, 6, 9, 24, 7, 34]
Right-side DFA transition table: [0, 1, 2, 3, 4, 5, 3, 3, 6, 7, 8, 9, 10, 11, 12, 3, 13, 14, 15, 3, 3, 3, 8, 9, 16, 17, 18, 3, 19, 3, 20, 3, 21, 22, 23, 3, 24, 3, 25, 26, 3, 27, 10, 28, 29, 3, 3, 30, 3, 31, 32, 3, 33, 3, 34, 3, 35, 36, 37, 36, 38, 39, 40, 3, 41, 42, 3, 43, 44, 18, 45, 46, 18, 3, 47, 46, 30, 5, 28, 3, 41, 5, 38, 39, 48, 3 , 3, 3, 3, 3, 5, 3, 49, 3, 5, 43, 3, 14, 26, 3]
This is indeed hundreds of times simpler than the BL_Proof data, so I’m not too fussed about what caused the recoverable errors above. Today I’m happy moving on to filing my taxes – a comparatively peaceful and relaxing activity.
I may come back later with graphics showing the DFA pairs and colorized spacetime diagrams (like on this Discord thread).