OAI/Computability/DirectedFeedback/Games/TestEmit.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.Label line 16
2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.State line 17
3. def OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.localEquation line 19
4. def OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.bodyLabel line 22
5. def OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.program line 27
6. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.testTrace line 35
7. def OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.testInTime line 56
8. def OAI.DFVSGames.Foundations.Hastad.SourceTestEmit.sourceTestInTime line 73
9. inductive OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.Label line 112
10. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.State line 117
11. structure OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.Layout line 119
12. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.equationBits line 131
13. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.steps line 134
14. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.bodyLabel line 140
15. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.statement line 144
16. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.program line 153
17. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.resultTapes line 157
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.resultTapes_other line 160
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.resultTapes_source line 164
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.resultTapes_temporary line 168
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.resultTapes_scratch line 172
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.emitTrace line 176
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.appendTrace line 204
24. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.appendInTime line 247
25. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.programInTime line 263
26. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.sourceAppendInTime line 275
27. abbrev OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.Tape line 311
28. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.standardLayout line 313
29. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.machine line 325
30. def OAI.DFVSGames.Foundations.Hastad.SourceTestAppend.machineInTime line 336
31. abbrev OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.Query line 355
32. abbrev OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.State line 356
33. inductive OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.Label line 358
34. def OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.finish line 365
35. def OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.statement line 371
36. def OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.prefixBits line 383
37. def OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.prefixSteps line 389
38. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.resultTapes_append line 395
39. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.prefixTrace line 406
40. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.prefixSteps_le line 458
41. theorem OAI.DFVSGames.Foundations.Hastad.SourceQueryLoop.loopInTime line 470
42. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.Alphabet line 511
43. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitTapes line 513
44. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.increment line 517
45. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.reset line 525
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.incrementPushBound line 530
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.resetPushBound line 535
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.update_current_inline_MachineTupleOdometer line 539
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.update_remaining_inline_MachineTupleOdometer line 550
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_succ line 556
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.stepAux_increment_zero line 566
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_succ line 576
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.incrementStep_zero line 589
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.resetTrace line 602
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.carryTrace line 616
56. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitSteps line 637
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitTrace line 639
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitSteps_le line 664
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitBudget line 670
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitFrame line 674
61. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.digitInTime line 683
62. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.bodyConfiguration line 705
63. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.checkConfiguration line 713
64. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.cycleExit line 721
65. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.VisitTraces line 728
66. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps line 739
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_zero_inline_MachineTupleOdometer line 742
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.cycleSteps_succ_inline_MachineTupleOdometer line 746
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.cycleTrace line 752
70. def OAI.DFVSGames.Foundations.Complexity.MachineTupleOdometer.ascendingCycleInTime line 787