OAI/Computability/MinUncut/PCP/PreprocessingPaddingWords.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.encodeWords_flatMap line 14
  2. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.ofFn_split line 20
  3. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.flatten_ofFn_rowIndex line 30
  4. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits line 45
  5. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits line 49
  6. def OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits line 52
  7. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_flat line 55
  8. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_eq_vertices line 61
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_old line 75
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowBits_pad_new line 87
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.dummy_rowsBits_eq_ofFn line 97
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.paddingBits_eq_ofFn line 111
  13. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_old line 125
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.vertexBits_pad_new line 129
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.rowsBits_pad line 141
  16. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingPaddingWords.tableBits_pad line 148
  17. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.actualRow line 169
  18. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.vertexRows line 174
  19. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexRows line 179
  20. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexRows line 180
  21. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.vertexBits line 183
  22. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.originalVertexBits line 186
  23. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.dummyVertexBits line 187
  24. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_internal line 190
  25. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_eq line 194
  26. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_tail line 204
  27. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_reverse line 208
  28. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_reverse line 220
  29. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.relation_ext line 233
  30. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_relation line 241
  31. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_relation line 248
  32. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_original_words line 258
  33. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.inherited_dummy_words line 265
  34. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.encodeWords_flatMap line 274
  35. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.actualRow_bits line 280
  36. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.vertexBits_eq line 288
  37. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.paddingOrder_ofFn line 305
  38. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.vertexOrder_ofFn line 317
  39. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.paddingList_flatMap line 347
  40. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.rowsBits_ofCloudTables line 354
  41. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularWords.tableBits_ofCloudTables line 373