OAI/Computability/MinUncut/PCP/PoweringTableLayout.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.blockSize line 12
2. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.dartCount_eq_vertex_blocks line 14
3. def OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.blockIndex line 20
4. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.blockIndex_val line 25
5. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.blockIndex_eq_encodeDart line 31
6. def OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRows line 38
7. def OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRowWords line 43
8. def OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRowBits line 47
9. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRows_length line 51
10. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vector_toList_ofFn line 57
11. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vector_blocks line 64
12. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.rowList_eq_vertexRows line 80
13. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.outputWords_vertexRows line 86
14. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.encodeWords_flatMap line 97
15. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.outputBits_vertexRows line 105
16. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRowWords_length line 113
17. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_ge line 120
18. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_le line 128
19. theorem OAI.MinUncutGames.Foundations.PCP.PoweringTableLayout.outputHeader_length line 137