OAI/Computability/BinPacking/PCP/PreprocessingMachineBounds.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.idxOf_map_injective line 10
2. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_idxOf line 20
3. def OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.offset line 47
4. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_length line 50
5. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.paddingOrder_val line 56
6. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.vertexOrder_dummy_val line 64
7. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_zero line 71
8. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_all line 74
9. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.localStep line 90
10. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.destination line 94
11. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.rowIndex line 98
12. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row line 103
13. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation line 107
14. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.equalityRelation_apply line 110
15. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.cloud_rotation line 114
16. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.source_rotation line 123
17. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.rotation_internal line 135
18. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.reverseIndex_internal line 142
19. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.relation_ext line 152
20. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.relations_internal line 161
21. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_tail line 168
22. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_reverse line 173
23. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_relation line 180
24. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.localStep_original line 185
25. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.localStep_dummy line 190
26. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_tail_original line 194
27. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_tail_dummy line 200
28. def OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex line 206
29. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_eq line 211
30. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_old line 235
31. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.selectedIndex_dummy line 240
32. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.row_reverse_selectedIndex line 246
33. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingInternalRows.rowWords_eq line 254
34. def OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.inputLength line 270
35. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.cloudSize_le_input line 272
36. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.cloudTotal_le_input line 276
37. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.level_le_input line 282
38. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.regularVertices_le_input line 286
39. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.offset_le_sum line 291
40. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.prefix_le_input line 302
41. def OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.tablePolynomial line 310
42. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.tableBits_le_of_counts line 315
43. def OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.regularPolynomial line 325
44. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.regularBits_le line 328
45. def OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.rotorPolynomial line 342
46. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingMachineBounds.cloudRotorBits_le line 346