OAI/Combinatorics/IndependentSets/Expansion/PreprocessingRegularWords.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.actualRow line 15
  2. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.vertexRows line 20
  3. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 25
  4. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 26
  5. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.vertexBits line 29
  6. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 32
  7. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 33
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 36
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 40
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 50
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 54
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 66
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.relation_ext line 79
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 87
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 94
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 104
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 111
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap line 120
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 126
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 134
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 151
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 162
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 188
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 195
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 214