OAI/Computability/BinPacking/PCP/PoweringTableLayout.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.blockSize line 11
2. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.dartCount_eq_vertex_blocks line 13
3. def OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.blockIndex line 18
4. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.blockIndex_val line 23
5. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.blockIndex_eq_encodeDart line 29
6. def OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRows line 36
7. def OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRowWords line 41
8. def OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRowBits line 45
9. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRows_length line 49
10. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vector_toList_ofFn line 54
11. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vector_blocks line 61
12. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.rowList_eq_vertexRows line 77
13. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.outputWords_vertexRows line 83
14. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.encodeWords_flatMap line 94
15. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.outputBits_vertexRows line 102
16. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRowWords_length line 110
17. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_ge line 117
18. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_le line 125
19. theorem OAI.BinPackingGames.Foundations.PCP.PoweringTableLayout.outputHeader_length line 134