OAI/Combinatorics/IndependentSets/Expansion/PreprocessingRegularTables.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.paddingList line 13
  2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.paddingList_nodup line 17
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.mem_paddingList line 21
  4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.paddingListOrder line 26
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.paddingList_length line 31
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.paddingOrder line 36
  7. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.Vertex line 40
  8. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexCount line 43
  9. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder line 46
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_original line 50
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexOrder_dummy line 54
  12. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.unitOrder line 59
  13. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.portOrder line 65
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.portOrder_internal line 68
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.portOrder_inherited line 71
  16. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.cloudGraphs line 74
  17. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.sourcePortGraph line 82
  18. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.sourceGraph line 89
  19. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.numberedPortGraph line 97
  20. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts line 104
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.numberedAccepts_transpose line 112
  22. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.ofCloudTables line 125
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.rotation_ofCloudTables line 132
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.accepts_ofCloudTables line 144
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.accepts_internal line 155
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.accepts_original line 165
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.accepts_dummy line 176
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.edgeSatisfied_ofCloudTables line 186
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_ofCloudTables line 203
  30. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.liftedLabel line 219
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.rejectionCount_liftedLabel line 225
  32. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.emptyTable line 238
  33. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.resizeTable line 241
  34. abbrev OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.BaseTable line 244
  35. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.internalDegree line 248
  36. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.padding line 250
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.cloudSize_add_padding line 254
  38. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_sum_cloudPaddedSize line 259
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_le line 266
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.vertexCount_eq_zero_of_no_darts line 272
  41. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.familyCloudTable line 278
  42. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.regularize line 291
  43. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularTables.regularizeInput line 295