OAI/Combinatorics/IndependentSets/Expansion/PoweringTableLayout.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.blockSize line 11
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.dartCount_eq_vertex_blocks line 13
3. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.blockIndex line 18
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.blockIndex_val line 23
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.blockIndex_eq_encodeDart line 29
6. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRows line 40
7. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRowWords line 45
8. def OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRowBits line 49
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRows_length line 53
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vector_toList_ofFn line 58
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vector_blocks line 65
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.rowList_eq_vertexRows line 81
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.outputWords_vertexRows line 87
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.encodeWords_flatMap line 97
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.outputBits_vertexRows line 105
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRowWords_length line 113
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_ge line 120
18. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_le line 128
19. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringTableLayout.outputHeader_length line 137