OAI/Computability/BinPacking/PCP/PreprocessingRegularBounds.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.actualRow line 13
  2. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.vertexRows line 18
  3. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 23
  4. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 24
  5. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.vertexBits line 27
  6. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 30
  7. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 31
  8. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 34
  9. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 38
  10. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 48
  11. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 52
  12. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 64
  13. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.relation_ext line 77
  14. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 85
  15. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 92
  16. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 102
  17. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 109
  18. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap line 118
  19. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 124
  20. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 132
  21. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 149
  22. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 160
  23. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 187
  24. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 194
  25. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 213
  26. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix line 229
  27. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix line 232
  28. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_zero line 235
  29. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_all line 239
  30. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_succ line 245
  31. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_zero line 253
  32. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_all line 257
  33. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_succ line 263
  34. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_append_suffix line 270
  35. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 283
  36. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 291
  37. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.header line 297
  38. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 300
  39. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 305
  40. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 310
  41. def OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 316
  42. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 324
  43. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 332
  44. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 343
  45. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 357
  46. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 364
  47. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 371
  48. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 378
  49. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 388