OAI/Computability/BinPacking/Computation/MachineCloudRank.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Tape line 11
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Tape.enumList line 15
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_getElem?_ctorIdx_eq line 18
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_nodup line 22
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.(instance at line 24) line 24
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Alphabet line 28
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.State line 29
8. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory line 31
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_original line 39
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_work line 41
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_target line 43
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_scratch line 45
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_count line 47
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.memory_spare line 49
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.update_memory_work line 52
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.update_memory_target line 56
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 60
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.update_memory_count line 64
19. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.finishField line 71
20. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.fieldLoop line 74
21. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.hit line 87
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 89
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 106
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 122
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.fieldTrace line 138
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 172
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 176
28. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 208
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 228
30. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Label line 263
31. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.skipLabel line 268
32. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowEntry line 271
33. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.program line 277
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.program_skip line 290
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 295
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowStep_empty line 305
37. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.Row line 311
38. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowWords line 313
39. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowTime line 315
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowTrace line 318
41. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowsHits line 353
42. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowsTime line 357
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowsTrace line 361
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowTime_le line 385
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowsTime_le line 394
46. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.inputWord line 404
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.inputWord_eq line 407
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.inputWord_length line 411
49. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.totalSteps line 418
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.countTrace line 421
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.totalSteps_le line 456
52. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.tableRows line 465
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.tableRows_width line 469
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.tableRows_words line 475
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.tableRows_input line 482
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 487
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 494
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 501
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.tableRows_hits line 507
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 513
61. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 527
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.update_memory_spare line 550
63. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.RankLabel line 555
64. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankSkip line 561
65. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankProgram line 564
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 583
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 588
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 599
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 607
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankRowTrace line 621
71. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.prefixTime line 657
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.prefixTrace line 661
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.prefixTime_le line 688
74. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.queryWord line 698
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 701
76. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankSteps line 709
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankTrace line 714
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.rankSteps_le line 772
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 785
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.tableRows_length line 804
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 807
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 820
83. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 843