OAI/Computability/MinUncut/PCP/GraphTables.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.PCP.GraphTables.Label line 12
  2. abbrev OAI.MinUncutGames.Foundations.PCP.GraphTables.RelationTable line 13
  3. def OAI.MinUncutGames.Foundations.PCP.GraphTables.relationIndex line 15
  4. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.relationIndex_val line 17
  5. def OAI.MinUncutGames.Foundations.PCP.GraphTables.relationAt line 20
  6. def OAI.MinUncutGames.Foundations.PCP.GraphTables.relationOf line 23
  7. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.relationAt_relationOf line 26
  8. structure OAI.MinUncutGames.Foundations.PCP.GraphTables.DartRow line 30
  9. abbrev OAI.MinUncutGames.Foundations.PCP.GraphTables.Rows line 35
  10. def OAI.MinUncutGames.Foundations.PCP.GraphTables.reverseAt line 37
  11. def OAI.MinUncutGames.Foundations.PCP.GraphTables.acceptsAt line 40
  12. def OAI.MinUncutGames.Foundations.PCP.GraphTables.Valid line 43
  13. instance OAI.MinUncutGames.Foundations.PCP.GraphTables.(instance at line 47) line 47
  14. structure OAI.MinUncutGames.Foundations.PCP.GraphTables.Table line 51
  15. def OAI.MinUncutGames.Foundations.PCP.GraphTables.rowList line 57
  16. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.rowList_length line 59
  17. def OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics line 62
  18. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_reverse line 73
  19. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_tail line 76
  20. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_accepts line 79
  21. def OAI.MinUncutGames.Foundations.PCP.GraphTables.graphRows line 82
  22. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 85
  23. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 90
  24. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.graphRows_valid line 95
  25. def OAI.MinUncutGames.Foundations.PCP.GraphTables.ofGraph line 103
  26. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 106
  27. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 111
  28. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 117
  29. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 122
  30. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.constraintGraph_ext line 127
  31. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph line 141
  32. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 150
  33. def OAI.MinUncutGames.Foundations.PCP.GraphTables.enumeratedGraph line 156
  34. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 172
  35. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 180
  36. def OAI.MinUncutGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 192
  37. def OAI.MinUncutGames.Foundations.PCP.GraphTables.bitWord line 196
  38. def OAI.MinUncutGames.Foundations.PCP.GraphTables.parseBit line 198
  39. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.parseBit_bitWord line 203
  40. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.parseBits_bitWords line 206
  41. def OAI.MinUncutGames.Foundations.PCP.GraphTables.relationWords line 212
  42. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.relationWords_length line 214
  43. def OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRelation line 217
  44. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRelation_encoded line 223
  45. def OAI.MinUncutGames.Foundations.PCP.GraphTables.rowWords line 230
  46. def OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRow line 233
  47. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRow_encoded line 241
  48. def OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRows line 249
  49. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.parseRows_encoded line 257
  50. def OAI.MinUncutGames.Foundations.PCP.GraphTables.tableWords line 263
  51. def OAI.MinUncutGames.Foundations.PCP.GraphTables.tableBits line 266
  52. def OAI.MinUncutGames.Foundations.PCP.GraphTables.decodeTableWords line 268
  53. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 279
  54. def OAI.MinUncutGames.Foundations.PCP.GraphTables.decodeTableBits line 287
  55. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 290
  56. def OAI.MinUncutGames.Foundations.PCP.GraphTables.encoding line 294
  57. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.tableBits_injective line 299
  58. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.rowWords_length line 301
  59. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.rowsWords_length line 304
  60. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.tableWords_length line 310
  61. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 315
  62. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.relationBits_length_le line 320
  63. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.rowBits_length_le line 328
  64. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.rowsBits_length_le line 337
  65. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.tableBits_length_le line 347
  66. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 356
  67. theorem OAI.MinUncutGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 362
  68. structure OAI.MinUncutGames.Foundations.PCP.PoweringWalks.PortGraph line 374
  69. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringWalks.Edge line 378
  70. abbrev OAI.MinUncutGames.Foundations.PCP.PoweringWalks.Walk line 379
  71. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.next line 383
  72. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rot_rot line 385
  73. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.walkEnd line 388
  74. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.walkEnd_nil line 392
  75. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.walkEnd_cons line 394
  76. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.walkEnd_append line 397
  77. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.splitHead line 403
  78. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rotateHead line 414
  79. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rotateHead_vertex line 418
  80. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rotateHead_zero line 421
  81. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rotateHead_succ line 424
  82. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.permutePorts line 428
  83. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.wordEnd line 442
  84. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.endpoint line 446
  85. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.natCard_walk line 449
  86. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.headTailEquiv line 453
  87. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.advanceTail line 464
  88. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.edgeAt line 467
  89. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.pivotEquiv line 473
  90. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.pivotEquiv_fst line 483
  91. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.edgeAt_port line 497
  92. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.pivotEquiv_zero_apply line 513
  93. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.pivotEquiv_succ_apply line 517
  94. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.projectedFiberEquiv line 524
  95. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.projectedEventEquiv line 536
  96. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_fiber line 554
  97. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.natCard_edgeAt_event line 563
  98. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.leftFromPivot line 573
  99. def OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rightFromPivot line 579
  100. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.leftFromPivot_zero line 586
  101. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rightFromPivot_zero line 590
  102. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.leftFromPivot_actual line 595
  103. theorem OAI.MinUncutGames.Foundations.PCP.PoweringWalks.rightFromPivot_actual line 614
  104. abbrev OAI.MinUncutGames.Foundations.PCP.PortTables.Label line 639
  105. def OAI.MinUncutGames.Foundations.PCP.PortTables.rowIndex line 641
  106. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.rowIndex_val line 644
  107. structure OAI.MinUncutGames.Foundations.PCP.PortTables.Table line 647
  108. def OAI.MinUncutGames.Foundations.PCP.PortTables.rotation line 658
  109. def OAI.MinUncutGames.Foundations.PCP.PortTables.accepts line 661
  110. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.rowIndex_rotation line 664
  111. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.rotation_involutive line 668
  112. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.accepts_rotation line 674
  113. def OAI.MinUncutGames.Foundations.PCP.PortTables.portGraph line 678
  114. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.portGraph_rot line 686
  115. def OAI.MinUncutGames.Foundations.PCP.PortTables.baseGraph line 689
  116. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.baseGraph_reverse line 696
  117. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.baseGraph_tail line 699
  118. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.baseGraph_head line 702
  119. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.baseGraph_accepts line 705
  120. def OAI.MinUncutGames.Foundations.PCP.PortTables.ofPortGraph line 708
  121. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 725
  122. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 732
  123. def OAI.MinUncutGames.Foundations.PCP.PortTables.flatRows line 740
  124. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.reverseAt_flatRows line 744
  125. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 748
  126. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.flatRows_valid line 752
  127. def OAI.MinUncutGames.Foundations.PCP.PortTables.graphTable line 759
  128. def OAI.MinUncutGames.Foundations.PCP.PortTables.tableWords line 762
  129. def OAI.MinUncutGames.Foundations.PCP.PortTables.tableBits line 764
  130. abbrev OAI.MinUncutGames.Foundations.PCP.PortTables.Input line 766
  131. def OAI.MinUncutGames.Foundations.PCP.PortTables.inputBits line 768
  132. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.tableWords_eq line 770
  133. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.tableWords_length line 773
  134. theorem OAI.MinUncutGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 777