OAI/Computability/BinPacking/PCP/PreprocessingOverlayWords.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.row line 12
  2. abbrev OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.trueRelation line 13
  3. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.oldReverseMap line 15
  4. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.expanderReverseMap line 16
  5. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.oldRow line 18
  6. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow line 24
  7. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.relation_ext line 29
  8. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_old line 36
  9. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.row_overlay_expander line 49
  10. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_reverse_val line 65
  11. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_reverse_val line 73
  12. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.oldRow_words line 81
  13. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.expanderRow_words line 88
  14. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.ofFn_overlayPorts line 98
  15. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows line 104
  16. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_length line 108
  17. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.flatRows_overlay line 112
  18. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.vertexRows_words line 122
  19. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.tableWords_overlay line 145
  20. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.tableBits_overlay line 150
  21. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayWords.rotationWords_vertices line 156