OAI/Computability/MinUncut/Machines/MachineTupleOdometer.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Alphabet line 13
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitTapes line 15
3. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.increment line 19
4. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.reset line 27
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.incrementPushBound line 32
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.resetPushBound line 37
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.update_current line 41
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.update_remaining line 52
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_succ line 58
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_zero line 68
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_succ line 78
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_zero line 91
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.resetTrace line 104
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.carryTrace line 118
15. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitSteps line 139
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitTrace line 141
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitSteps_le line 166
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitBudget line 172
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitFrame line 176
20. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.digitInTime line 185
21. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.bodyConfiguration line 207
22. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.checkConfiguration line 215
23. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.cycleExit line 223
24. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.VisitTraces line 230
25. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps line 241
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_zero line 244
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_succ line 248
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.cycleTrace line 254
29. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime line 289
30. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder line 327
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_length line 330
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_dimension_zero line 333
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_radix_zero line 340
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_cons line 344
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_increment_lowest line 355
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_carry line 362
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleRank_snoc line 371
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.tupleOrder_snoc line 378
39. structure OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.CycleSchedule line 402
40. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Configuration line 409
41. inductive OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle line 412
42. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead line 444
43. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps line 454
44. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.LeafBound line 463
45. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.work line 471
46. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit line 479
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.reverseDigit_current line 481
48. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order line 485
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_eq_tupleOrder line 495
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.order_length line 504
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_eq_work_add_overhead line 509
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.trace line 533
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le line 549
54. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.inTime line 578
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.counterOverhead_le line 590
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.NestedCycle.steps_le_power line 611
57. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.entry line 623
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_dimension_zero line 633
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_zero line 643
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.entryStep_radix_positive line 655
61. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.Label line 673
62. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.start line 675
63. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.body line 676
64. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.exit line 677
65. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.check line 678
66. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.resetLabel line 679
67. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.carry line 681
68. def OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.program line 684
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTupleOdometer.Control.label_card line 694