OAI/Computability/MinUncut/Machines/MachineRegularMetadata.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Extra line 13
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList line 17
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_getElem?_ctorIdx_eq line 19
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_nodup line 23
5. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.(instance at line 25) line 25
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Tape line 29
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Alphabet line 30
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.State line 31
9. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Label line 33
10. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 44
11. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankTape line 46
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixTape line 54
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudTape line 69
14. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.program line 83
15. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankView line 109
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixView line 120
17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudView line 138
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankView_left line 152
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankView_right line 154
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 160
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 166
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 172
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 174
24. structure OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.Data line 180
25. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.frame line 193
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.frame_index line 208
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 211
28. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cfg line 214
29. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudData line 218
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 224
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.join_trace line 260
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.drainAt line 264
33. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixData line 274
34. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 278
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 281
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.selected_owner line 333
37. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerData line 341
38. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 344
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 347
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 351
41. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankQuery line 397
42. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.queryFrame line 399
43. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.querySteps line 403
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.queryTrace line 405
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankData line 442
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 446
47. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankSteps line 450
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankTrace line 456
49. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.originalMember line 519
50. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.originalData line 522
51. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.totalTime line 526
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.originalTrace line 530
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le line 551
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 558
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 562
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 573
57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.overhead line 577
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.overhead_le line 581
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 586
60. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.originalInTime line 636
61. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 651