OAI/Computability/VertexCover/PCP/PreprocessingRegularTables.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 14
  2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 18
  3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 22
  4. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 27
  5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 32
  6. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 37
  7. abbrev OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 41
  8. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 44
  9. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 47
  10. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 51
  11. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 55
  12. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 60
  13. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 66
  14. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 69
  15. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 72
  16. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 75
  17. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 83
  18. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 90
  19. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 98
  20. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 105
  21. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 113
  22. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 126
  23. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 133
  24. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 145
  25. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 156
  26. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 166
  27. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 177
  28. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 187
  29. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 204
  30. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 220
  31. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 226
  32. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 238
  33. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 241
  34. abbrev OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 244
  35. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 248
  36. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.padding line 250
  37. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 254
  38. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 259
  39. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 266
  40. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 272
  41. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 278
  42. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.regularize line 291
  43. def OAI.UniqueGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 295