OAI/Combinatorics/IndependentSets/Expansion/PreprocessingPaddingWords.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap line 13
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 19
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 29
4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowBits line 44
5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 48
6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 51
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 54
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 60
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 74
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 86
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 96
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 110
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 124
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 128
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 140
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 147