OAI/Computability/WeisfeilerLeman/Tableau.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLTime.CircuitEncoding.Address line 9
  2. def OAI.WLTime.CircuitEncoding.ProductAllowed line 11
  3. structure OAI.WLTime.CircuitEncoding.Schematic line 14
  4. abbrev OAI.WLTime.CircuitEncoding.Schematic.Instance line 37
  5. abbrev OAI.WLTime.CircuitEncoding.Schematic.Connection line 38
  6. def OAI.WLTime.CircuitEncoding.Schematic.transmit line 40
  7. def OAI.WLTime.CircuitEncoding.Schematic.expand line 44
  8. inductive OAI.WLTime.CircuitEncoding.Schematic.Node line 69
  9. inductive OAI.WLTime.CircuitEncoding.Schematic.Edge line 75
  10. def OAI.WLTime.CircuitEncoding.Schematic.nodeDim line 83
  11. def OAI.WLTime.CircuitEncoding.Schematic.edgeSrc line 88
  12. def OAI.WLTime.CircuitEncoding.Schematic.edgeDst line 95
  13. def OAI.WLTime.CircuitEncoding.Schematic.edgeDomain line 102
  14. def OAI.WLTime.CircuitEncoding.Schematic.edgeCoord line 109
  15. theorem OAI.WLTime.CircuitEncoding.Schematic.edgeCoord_inj line 116
  16. def OAI.WLTime.CircuitEncoding.Schematic.sumForm line 119
  17. def OAI.WLTime.CircuitEncoding.Schematic.coordForm line 124
  18. def OAI.WLTime.CircuitEncoding.Schematic.srcForm line 129
  19. def OAI.WLTime.CircuitEncoding.Schematic.dstForm line 136
  20. def OAI.WLTime.CircuitEncoding.Schematic.dstBias line 143
  21. def OAI.WLTime.CircuitEncoding.Schematic.consistency line 147
  22. theorem OAI.WLTime.CircuitEncoding.Schematic.same_transmit_first line 159
  23. theorem OAI.WLTime.CircuitEncoding.Schematic.same_transmit_second line 162
  24. theorem OAI.WLTime.CircuitEncoding.Schematic.same_transmit_third line 165
  25. theorem OAI.WLTime.CircuitEncoding.Schematic.same_transmit_seed line 168
  26. theorem OAI.WLTime.CircuitEncoding.Schematic.same_transmit_test line 171
  27. theorem OAI.WLTime.CircuitEncoding.Schematic.affineSrc_first line 175
  28. theorem OAI.WLTime.CircuitEncoding.Schematic.affineSrc_second line 180
  29. theorem OAI.WLTime.CircuitEncoding.Schematic.affineSrc_seed line 185
  30. theorem OAI.WLTime.CircuitEncoding.Schematic.affineSrc_test line 190
  31. theorem OAI.WLTime.CircuitEncoding.Schematic.affineSrc_third line 195
  32. theorem OAI.WLTime.CircuitEncoding.Schematic.affineDst_first line 202
  33. theorem OAI.WLTime.CircuitEncoding.Schematic.affineDst_second line 207
  34. theorem OAI.WLTime.CircuitEncoding.Schematic.affineDst_third line 212
  35. theorem OAI.WLTime.CircuitEncoding.Schematic.affineDst_seed line 217
  36. theorem OAI.WLTime.CircuitEncoding.Schematic.affineDst_test line 222
  37. def OAI.WLTime.CircuitEncoding.Schematic.setsOfWitness line 231
  38. theorem OAI.WLTime.CircuitEncoding.Schematic.setsOfWitness_nonempty line 237
  39. theorem OAI.WLTime.CircuitEncoding.Schematic.setsOfWitness_buffer line 251
  40. theorem OAI.WLTime.CircuitEncoding.Schematic.consistent_of_witness line 256
  41. def OAI.WLTime.CircuitEncoding.Schematic.witnessOfConsistent line 298
  42. theorem OAI.WLTime.CircuitEncoding.Schematic.consistency_iff_tests_false line 340
  43. theorem OAI.WLTime.CircuitEncoding.Schematic.dim_le_two line 349
  44. def OAI.WLTime.CircuitEncoding.Circuit.EdgeCover line 361
  45. theorem OAI.WLTime.CircuitEncoding.Circuit.incoming_of_cover line 365
  46. theorem OAI.WLTime.CircuitEncoding.Circuit.truth_of_cover line 377
  47. inductive OAI.WLTime.CircuitEncoding.BoxTableau.Label line 396
  48. abbrev OAI.WLTime.CircuitEncoding.BoxTableau.Tag line 404
  49. def OAI.WLTime.CircuitEncoding.BoxTableau.labelEquiv line 406
  50. instance OAI.WLTime.CircuitEncoding.BoxTableau.(instance at line 428) line 428
  51. def OAI.WLTime.CircuitEncoding.BoxTableau.src line 434
  52. def OAI.WLTime.CircuitEncoding.BoxTableau.dst line 441
  53. def OAI.WLTime.CircuitEncoding.BoxTableau.port line 448
  54. def OAI.WLTime.CircuitEncoding.BoxTableau.box line 455
  55. def OAI.WLTime.CircuitEncoding.BoxTableau.Numerical line 462
  56. theorem OAI.WLTime.CircuitEncoding.BoxTableau.box_numerical line 474
  57. def OAI.WLTime.CircuitEncoding.BoxTableau.nodeMap line 492
  58. def OAI.WLTime.CircuitEncoding.BoxTableau.nodeEquiv line 496
  59. theorem OAI.WLTime.CircuitEncoding.BoxTableau.nodeEquiv_apply line 500
  60. theorem OAI.WLTime.CircuitEncoding.BoxTableau.numerical_forward line 503
  61. theorem OAI.WLTime.CircuitEncoding.BoxTableau.box_forward line 510
  62. theorem OAI.WLTime.CircuitEncoding.BoxTableau.left_covered line 516
  63. theorem OAI.WLTime.CircuitEncoding.BoxTableau.center_covered line 524
  64. theorem OAI.WLTime.CircuitEncoding.BoxTableau.right_covered line 532
  65. theorem OAI.WLTime.CircuitEncoding.BoxTableau.realizes line 540
  66. theorem OAI.WLTime.CircuitEncoding.BoxTableau.covers line 577
  67. def OAI.WLTime.CircuitEncoding.BoxTableau.initialDigit line 624
  68. def OAI.WLTime.CircuitEncoding.BoxTableau.initialRing line 627
  69. def OAI.WLTime.CircuitEncoding.BoxTableau.seedGate line 630
  70. def OAI.WLTime.CircuitEncoding.BoxTableau.positionDomain line 634
  71. def OAI.WLTime.CircuitEncoding.BoxTableau.seedDomain line 639
  72. theorem OAI.WLTime.CircuitEncoding.BoxTableau.seed_allowed line 642
  73. theorem OAI.WLTime.CircuitEncoding.BoxTableau.input_allowed line 649
  74. theorem OAI.WLTime.CircuitEncoding.BoxTableau.blank_allowed line 655
  75. theorem OAI.WLTime.CircuitEncoding.BoxTableau.seed_spec line 662
  76. def OAI.WLTime.CircuitEncoding.BoxTableau.testGate line 693
  77. def OAI.WLTime.CircuitEncoding.BoxTableau.testDomain line 695
  78. theorem OAI.WLTime.CircuitEncoding.BoxTableau.test_allowed line 699
  79. theorem OAI.WLTime.CircuitEncoding.BoxTableau.test_spec line 705
  80. theorem OAI.WLTime.CircuitEncoding.BoxTableau.terminal line 713
  81. def OAI.WLTime.CircuitEncoding.BoxTableau.schematic line 725
  82. theorem OAI.WLTime.CircuitEncoding.BoxTableau.edge_cover line 744
  83. theorem OAI.WLTime.CircuitEncoding.BoxTableau.seed_eq line 770
  84. theorem OAI.WLTime.CircuitEncoding.BoxTableau.test_eq line 792
  85. theorem OAI.WLTime.CircuitEncoding.BoxTableau.truth_eq line 810
  86. theorem OAI.WLTime.CircuitEncoding.BoxTableau.local_equivalence line 816