OAI/Computability/DirectedFeedback/Machines/TupleOrder.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder line 14
2. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_length line 17
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_dimension_zero line 20
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_radix_zero line 27
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_cons line 31
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_increment_lowest line 42
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_carry line 49
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_snoc line 58
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_snoc line 65
10. structure OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.CycleSchedule line 87
11. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Configuration line 94
12. inductive OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle line 97
13. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead line 129
14. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps line 139
15. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound line 148
16. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.work line 156
17. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit line 164
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit_current line 166
19. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order line 170
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_eq_tupleOrder line 180
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_length line 189
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_eq_work_add_overhead line 194
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.trace line 218
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le line 234
25. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime line 263
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead_le line 275
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le_power line 296
28. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.entry line 309
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.entryStep_dimension_zero line 319
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_zero line 329
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_positive line 341
32. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.Label line 359
33. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.start line 361
34. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.body line 362
35. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.exit line 363
36. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.check line 364
37. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.resetLabel line 365
38. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.carry line 367
39. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.program line 370
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Control.label_card line 380
41. def OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.decodeTuple line 396
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_function line 400
43. theorem OAI.DFVSGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate_fin_function line 406
44. def OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.tupleTapeOrder line 418
45. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_eq_tupleTapeOrder line 426
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.testTapeEncoding_flatMap_tupleTapeOrder line 433
47. def OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.rankedQuery line 439
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.rankedQuery_at line 445
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_ofFn line 450
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_enumerate line 465
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.query_prefixBits_eq_tupleTapeOrder line 479
52. def OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.tupleSourceOrder line 488
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.sourceIndexEncoding_eq_tupleSourceOrder line 494
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_eq_tupleOrder line 502
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.sourceList_eq_tupleOrder line 507
56. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.rawSourceList_flatMap_tupleOrder line 511
57. def OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.reverseAppend line 518
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend line 522
59. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_header line 532
60. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.foldl_reverseAppend_prefix line 538
61. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.foldl_resultTapes line 545
62. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.inputBits_eq_header_records line 563
63. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.input_reverse_accumulator line 575
64. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.sourceInput_tuple_reverse_accumulator line 582
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopOrder.finalReverse_steps line 596
66. abbrev OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.Tape line 618
67. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.currentAt line 622
68. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.remainingAt line 625
69. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits line 628
70. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setAcc line 636
71. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.putDigit line 639
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_zero line 643
73. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_extra line 649
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_self line 653
75. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_setAcc line 657
76. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_apply line 661
77. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_setAcc line 664
78. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_extra line 670
79. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_setAcc line 674
80. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_putDigit line 681
81. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc line 701
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc_base line 737
83. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.allBits line 743
84. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix line 746
85. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_eq_ofFn line 750
86. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.blocks line 759
87. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_all line 762
88. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.configuration line 769
89. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.BodyTrace line 772
90. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.val_snoc line 783
91. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.zeros_snoc line 789
92. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration line 794
93. def OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.finalConfiguration line 798
94. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.exists_schedule line 804
95. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.traversalInTime line 935
96. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.initial_current line 957
97. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.initial_remaining line 963
98. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.final_current line 968
99. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.final_remaining line 974
100. theorem OAI.DFVSGames.Foundations.Hastad.SourceOdometerSchedule.final_accumulator line 980