OAI/Computability/MinUncut/Machines/MachineUnaryCounter.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.Alphabet line 12
2. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guard line 14
3. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes line 21
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_counter line 25
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_other line 30
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardPushBound line 36
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.stepAux_succ line 40
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.stepAux_zero line 48
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardStep_succ line 56
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardStep_zero line 68
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_succ line 80
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_zero line 93
13. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_succ line 105
14. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_zero line 120
15. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLookup.Alphabet line 143
16. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discard line 145
17. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.select line 152
18. inductive OAI.MinUncutGames.Foundations.Complexity.MachineLookup.Label line 159
19. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLookup.Label.enumList line 163
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.Label.enumList_getElem?_ctorIdx_eq line 166
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.Label.enumList_nodup line 170
22. instance OAI.MinUncutGames.Foundations.Complexity.MachineLookup.(instance at line 172) line 172
23. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.program line 176
24. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.tapes line 185
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.tapes_index line 190
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.tapes_source line 196
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.tapes_destination line 202
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.tapes_other line 207
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.update_index line 213
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.update_source line 227
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.update_destination line 238
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.fieldTapes_eq line 244
33. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.machine line 251
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discard_update_twice line 266
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discardStep_delimiter line 275
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discardStep_true line 288
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discard_empty_step line 301
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discardTrace_update line 317
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discardTrace line 340
40. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.discardInTime line 359
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCopy.Alphabet line 382
42. def OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkLoop line 384
43. def OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTapes line 392
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTapes_source line 397
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTapes_left line 403
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTapes_right line 408
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTapes_self line 413
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.update_fork_source line 417
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.update_fork_left line 431
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.update_fork_right line 442
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkStep_empty line 448
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkStep_cons line 464
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkTrace line 482
54. def OAI.MinUncutGames.Foundations.Complexity.MachineCopy.forkInTime line 509
55. def OAI.MinUncutGames.Foundations.Complexity.MachineCopy.drainedTapes line 529
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.restoredTapes line 532
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCopy.copyTrace line 550
58. def OAI.MinUncutGames.Foundations.Complexity.MachineCopy.copyInTime line 591
59. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 622
60. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 628
61. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 633
62. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.BodyTraces line 638
63. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.totalSteps line 647
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 650
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 653
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.loopTrace line 658
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 691
68. def OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.loopInTime line 702
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.baseFrame line 723
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.counterFrame line 734
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 745