OAI/Computability/DirectedFeedback/Encoding/PreprocessingRegularTables.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 12
  2. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 16
  3. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 20
  4. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 25
  5. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 30
  6. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 35
  7. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 39
  8. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 42
  9. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 45
  10. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 49
  11. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 53
  12. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 58
  13. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 64
  14. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 67
  15. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 70
  16. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 73
  17. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 81
  18. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 88
  19. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 96
  20. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 103
  21. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 111
  22. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 124
  23. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 131
  24. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 143
  25. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 154
  26. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 164
  27. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 175
  28. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 185
  29. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 202
  30. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 218
  31. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 224
  32. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 236
  33. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 239
  34. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 242
  35. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 246
  36. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.padding line 248
  37. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 252
  38. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 257
  39. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 264
  40. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 270
  41. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 276
  42. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.regularize line 289
  43. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 293
  44. def OAI.DFVSGames.Foundations.PCP.VertexPadding.reverseFunction line 306
  45. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.reverseFunction_involutive line 311
  46. def OAI.DFVSGames.Foundations.PCP.VertexPadding.pad line 319
  47. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.pad_tail line 337
  48. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.pad_reverse_inl line 340
  49. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.pad_reverse_inr line 345
  50. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.edgeSatisfied_inl line 349
  51. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.edgeSatisfied_inr line 360
  52. def OAI.DFVSGames.Foundations.PCP.VertexPadding.extendLabeling line 364
  53. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.extendLabeling_inl line 367
  54. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.extendLabeling_inr line 370
  55. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.pad_satisfiable line 373
  56. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.satisfiable_of_pad line 381
  57. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.rejectionCount_eq_sum_inline_VertexPadding line 388
  58. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.pad_rejectionCount line 393
  59. def OAI.DFVSGames.Foundations.PCP.VertexPadding.extraVertices line 406
  60. abbrev OAI.DFVSGames.Foundations.PCP.VertexPadding.Vertex line 408
  61. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.card_vertex line 410
  62. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.le_card_vertex line 414
  63. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.card_vertex_le line 418
  64. def OAI.DFVSGames.Foundations.PCP.VertexPadding.familyVertexEquiv line 423
  65. def OAI.DFVSGames.Foundations.PCP.VertexPadding.paddedG line 431
  66. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.paddedG_tail line 434
  67. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.paddedG_rejectionCount line 437
  68. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.rejectionCount_eq line 444
  69. def OAI.DFVSGames.Foundations.PCP.VertexPadding.liftLabel line 451
  70. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.liftLabel_inl line 454
  71. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.liftLabel_inr line 457
  72. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.rejectionCount_liftLabel line 461
  73. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.paddedG_satisfiable line 468
  74. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.card_padded_darts line 472
  75. theorem OAI.DFVSGames.Foundations.PCP.VertexPadding.card_padded_darts_le line 476
  76. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv line 491
  77. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inl line 494
  78. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_inr_val line 497
  79. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.vertexEquiv_symm_old line 500
  80. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv line 504
  81. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.dartEquiv_apply line 508
  82. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.sumGraph line 512
  83. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph line 517
  84. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_reverse_equiv line 534
  85. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_accepts_equiv line 542
  86. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.pad line 549
  87. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad line 555
  88. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad line 559
  89. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.pad_valid line 564
  90. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.constraintGraph_ext_inline_PreprocessingPaddingTables line 570
  91. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.baseGraph_pad line 584
  92. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_equiv line 592
  93. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_old line 600
  94. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.rotation_pad_new line 607
  95. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_old line 614
  96. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.accepts_pad_new line 620
  97. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_old line 626
  98. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.reverseIndex_pad_new line 632
  99. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.relation_ext_inline_PreprocessingPaddingTables line 638
  100. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_old line 647
  101. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.relations_pad_new line 655
  102. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.paddedGraph_edgeSatisfied_equiv line 665
  103. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_equiv line 677
  104. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_old line 684
  105. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.edgeSatisfied_pad_new line 692
  106. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.pad_rejectionCount line 698
  107. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.pad_labeling_satisfies_iff line 716
  108. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling line 731
  109. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.extendLabeling_old line 734
  110. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingTables.pad_satisfiable_iff line 738