OAI/Combinatorics/IndependentSets/Machines/MachineRegularMetadata.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.Extra line 13
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.(instance at line 16) line 16
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.Tape line 20
4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.Alphabet line 21
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.State line 22
6. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.Label line 24
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 35
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankTape line 37
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixTape line 45
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudTape line 60
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.program line 74
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankView line 100
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixView line 111
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudView line 129
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankView_left line 143
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankView_right line 145
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 151
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 157
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 163
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 165
21. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.Data line 171
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.frame line 184
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.frame_index line 199
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 202
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cfg line 205
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudData line 209
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 215
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.join_trace line 251
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.drainAt line 255
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixData line 265
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 269
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 272
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.selected_owner line 324
34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerData line 332
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 335
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 338
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 342
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankQuery line 388
39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.queryFrame line 390
40. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.querySteps line 394
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.queryTrace line 396
42. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankData line 433
43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 437
44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankSteps line 441
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankTrace line 447
46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.originalMember line 510
47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.originalData line 513
48. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.totalTime line 517
49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.originalTrace line 521
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le line 542
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 549
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 553
53. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 564
54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.overhead line 568
55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.overhead_le line 572
56. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 577
57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.originalInTime line 627
58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 642