OAI/Computability/BinPacking/PCP/RawInitialPredicate.lean

GitHub source file

151 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.PCP.GraphTables.Label line 14
  2. abbrev OAI.BinPackingGames.Foundations.PCP.GraphTables.RelationTable line 15
  3. def OAI.BinPackingGames.Foundations.PCP.GraphTables.relationIndex line 17
  4. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.relationIndex_val line 19
  5. def OAI.BinPackingGames.Foundations.PCP.GraphTables.relationAt line 22
  6. def OAI.BinPackingGames.Foundations.PCP.GraphTables.relationOf line 25
  7. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.relationAt_relationOf line 28
  8. structure OAI.BinPackingGames.Foundations.PCP.GraphTables.DartRow line 32
  9. abbrev OAI.BinPackingGames.Foundations.PCP.GraphTables.Rows line 37
  10. def OAI.BinPackingGames.Foundations.PCP.GraphTables.reverseAt line 39
  11. def OAI.BinPackingGames.Foundations.PCP.GraphTables.acceptsAt line 42
  12. def OAI.BinPackingGames.Foundations.PCP.GraphTables.Valid line 45
  13. instance OAI.BinPackingGames.Foundations.PCP.GraphTables.(instance at line 49) line 49
  14. structure OAI.BinPackingGames.Foundations.PCP.GraphTables.Table line 53
  15. def OAI.BinPackingGames.Foundations.PCP.GraphTables.rowList line 59
  16. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.rowList_length line 61
  17. def OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics line 64
  18. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_reverse line 75
  19. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_tail line 78
  20. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_accepts line 81
  21. def OAI.BinPackingGames.Foundations.PCP.GraphTables.graphRows line 84
  22. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.reverseAt_graphRows line 87
  23. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.acceptsAt_graphRows line 92
  24. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.graphRows_valid line 97
  25. def OAI.BinPackingGames.Foundations.PCP.GraphTables.ofGraph line 105
  26. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph_reverse line 108
  27. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph_tail line 113
  28. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph_accepts line 119
  29. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph_edgeSatisfied line 124
  30. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.constraintGraph_ext line 129
  31. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph line 143
  32. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.semantics_ofGraph_rejectionCount line 152
  33. def OAI.BinPackingGames.Foundations.PCP.GraphTables.enumeratedGraph line 158
  34. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.enumeratedGraph_edgeSatisfied line 174
  35. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.enumeratedGraph_rejectionCount line 182
  36. def OAI.BinPackingGames.Foundations.PCP.GraphTables.ofEnumeratedGraph line 194
  37. def OAI.BinPackingGames.Foundations.PCP.GraphTables.bitWord line 198
  38. def OAI.BinPackingGames.Foundations.PCP.GraphTables.parseBit line 200
  39. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.parseBit_bitWord line 205
  40. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.parseBits_bitWords line 208
  41. def OAI.BinPackingGames.Foundations.PCP.GraphTables.relationWords line 214
  42. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.relationWords_length line 216
  43. def OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRelation line 219
  44. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRelation_encoded line 225
  45. def OAI.BinPackingGames.Foundations.PCP.GraphTables.rowWords line 232
  46. def OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRow line 235
  47. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRow_encoded line 243
  48. def OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRows line 251
  49. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.parseRows_encoded line 259
  50. def OAI.BinPackingGames.Foundations.PCP.GraphTables.tableWords line 265
  51. def OAI.BinPackingGames.Foundations.PCP.GraphTables.tableBits line 268
  52. def OAI.BinPackingGames.Foundations.PCP.GraphTables.decodeTableWords line 270
  53. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.decodeTableWords_encoded line 281
  54. def OAI.BinPackingGames.Foundations.PCP.GraphTables.decodeTableBits line 289
  55. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.decodeTableBits_encoded line 292
  56. def OAI.BinPackingGames.Foundations.PCP.GraphTables.encoding line 296
  57. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.tableBits_injective line 301
  58. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.rowWords_length line 303
  59. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.rowsWords_length line 306
  60. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.tableWords_length line 312
  61. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.tableWords_length_le_bits line 317
  62. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.relationBits_length_le line 322
  63. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.rowBits_length_le line 330
  64. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.rowsBits_length_le line 339
  65. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.tableBits_length_le line 349
  66. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.vertices_le_tableBits_length line 358
  67. theorem OAI.BinPackingGames.Foundations.PCP.GraphTables.darts_le_tableBits_length line 364
  68. abbrev OAI.BinPackingGames.Foundations.PCP.PortTables.Label line 376
  69. def OAI.BinPackingGames.Foundations.PCP.PortTables.rowIndex line 378
  70. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.rowIndex_val line 381
  71. structure OAI.BinPackingGames.Foundations.PCP.PortTables.Table line 384
  72. def OAI.BinPackingGames.Foundations.PCP.PortTables.rotation line 395
  73. def OAI.BinPackingGames.Foundations.PCP.PortTables.accepts line 398
  74. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.rowIndex_rotation line 401
  75. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.rotation_involutive line 405
  76. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.accepts_rotation line 411
  77. def OAI.BinPackingGames.Foundations.PCP.PortTables.portGraph line 415
  78. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.portGraph_rot line 423
  79. def OAI.BinPackingGames.Foundations.PCP.PortTables.baseGraph line 426
  80. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.baseGraph_reverse line 433
  81. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.baseGraph_tail line 436
  82. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.baseGraph_head line 439
  83. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.baseGraph_accepts line 442
  84. def OAI.BinPackingGames.Foundations.PCP.PortTables.ofPortGraph line 445
  85. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.rotation_ofPortGraph line 462
  86. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.accepts_ofPortGraph line 469
  87. def OAI.BinPackingGames.Foundations.PCP.PortTables.flatRows line 477
  88. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.reverseAt_flatRows line 481
  89. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.acceptsAt_flatRows line 485
  90. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.flatRows_valid line 489
  91. def OAI.BinPackingGames.Foundations.PCP.PortTables.graphTable line 496
  92. def OAI.BinPackingGames.Foundations.PCP.PortTables.tableWords line 499
  93. def OAI.BinPackingGames.Foundations.PCP.PortTables.tableBits line 501
  94. abbrev OAI.BinPackingGames.Foundations.PCP.PortTables.Input line 503
  95. def OAI.BinPackingGames.Foundations.PCP.PortTables.inputBits line 505
  96. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.tableWords_eq line 507
  97. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.tableWords_length line 510
  98. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.vertices_le_tableBits_length line 514
  99. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.flatMap_word line 521
  100. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.vertices_word line 553
  101. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.darts_word line 556
  102. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.row_word line 559
  103. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.tail_word line 575
  104. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.reverse_word line 583
  105. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.relation_word line 592
  106. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.accepts_word line 604
  107. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.rotation_head_word line 611
  108. theorem OAI.BinPackingGames.Foundations.PCP.PortTableLookup.rotor_lookups line 616
  109. def OAI.BinPackingGames.Foundations.PCP.PortTables.HasPortTails line 629
  110. instance OAI.BinPackingGames.Foundations.PCP.PortTables.(instance at line 632) line 632
  111. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.flatRows_hasPortTails line 636
  112. def OAI.BinPackingGames.Foundations.PCP.PortTables.ofRows line 640
  113. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.table_ext line 652
  114. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.ofRows_flatRows line 661
  115. def OAI.BinPackingGames.Foundations.PCP.PortTables.extractInput line 671
  116. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.extractInput_graphTable line 683
  117. def OAI.BinPackingGames.Foundations.PCP.PortTables.decodeInputBits line 687
  118. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.decodeInputBits_inputBits line 690
  119. def OAI.BinPackingGames.Foundations.PCP.PortTables.encoding line 695
  120. theorem OAI.BinPackingGames.Foundations.PCP.PortTables.inputBits_injective line 700
  121. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.unitOrder line 709
  122. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.slotOrder line 715
  123. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.binaryOrder line 724
  124. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.labelOrder line 733
  125. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.vertexOrder line 735
  126. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.eventOrder line 739
  127. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.dartOrder line 742
  128. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.raw64 line 746
  129. def OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table line 750
  130. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_vertices line 753
  131. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_darts line 756
  132. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_vertices_positive line 758
  133. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_darts_positive line 761
  134. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.raw64_satisfiable_iff line 764
  135. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_semantics line 769
  136. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.table_satisfiable_iff line 777
  137. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.initial_rejection line 783
  138. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialTables.initial_size line 789
  139. abbrev OAI.BinPackingGames.Foundations.PCP.RawInitialRows.Signs line 800
  140. abbrev OAI.BinPackingGames.Foundations.PCP.RawInitialRows.Names line 801
  141. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.clauseSigns line 803
  142. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.clauseNames line 806
  143. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.nameWord line 809
  144. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.decodedLabel line 814
  145. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.incidencePredicate line 817
  146. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.relationPredicate line 825
  147. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.relationWordsFor line 830
  148. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialRows.relationWordsFor_length line 833
  149. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.incidenceWords line 837
  150. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.clauseWords line 843
  151. def OAI.BinPackingGames.Foundations.PCP.RawInitialRows.dummyWords line 851