OAI/Computability/MinUncut/PCP/PreprocessingRegularTables.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 11
  2. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 15
  3. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 19
  4. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 24
  5. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 29
  6. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 34
  7. abbrev OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 38
  8. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 41
  9. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 44
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 48
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 52
  12. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 57
  13. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 63
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 66
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 69
  16. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 72
  17. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 80
  18. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 87
  19. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 95
  20. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 102
  21. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 110
  22. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 123
  23. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 130
  24. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 142
  25. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 153
  26. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 163
  27. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 174
  28. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 184
  29. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 201
  30. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 217
  31. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 223
  32. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 236
  33. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 239
  34. abbrev OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 242
  35. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 246
  36. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.padding line 248
  37. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 252
  38. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 257
  39. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 264
  40. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 270
  41. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 276
  42. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.regularize line 289
  43. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 293
  44. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.reverseFunction line 305
  45. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 310
  46. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad line 318
  47. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad_tail line 336
  48. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 339
  49. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 344
  50. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 348
  51. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 359
  52. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.extendLabeling line 363
  53. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 366
  54. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 369
  55. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad_satisfiable line 372
  56. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 380
  57. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum line 387
  58. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 392
  59. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.extraVertices line 404
  60. abbrev OAI.MinUncutGames.Foundations.PCP.VertexPadding.Vertex line 406
  61. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.card_vertex line 408
  62. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.le_card_vertex line 412
  63. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.card_vertex_le line 416
  64. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 421
  65. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.paddedG line 429
  66. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.paddedG_tail line 432
  67. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 435
  68. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 442
  69. def OAI.MinUncutGames.Foundations.PCP.VertexPadding.liftLabel line 449
  70. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.liftLabel_inl line 452
  71. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.liftLabel_inr line 455
  72. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 459
  73. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 466
  74. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.card_padded_darts line 470
  75. theorem OAI.MinUncutGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 474
  76. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 487
  77. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 490
  78. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 493
  79. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 496
  80. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 500
  81. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 504
  82. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 508
  83. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 513
  84. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 530
  85. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 538
  86. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.pad line 545
  87. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 551
  88. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 555
  89. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 560
  90. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext line 566
  91. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 580
  92. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 588
  93. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 596
  94. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 603
  95. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 610
  96. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 616
  97. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 622
  98. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 628
  99. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext line 634
  100. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 643
  101. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 651
  102. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 661
  103. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 674
  104. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 681
  105. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 689
  106. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 695
  107. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 713
  108. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 728
  109. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 731
  110. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 735