OAI/Combinatorics/IndependentSets/Machines/MachineRegularOriginalBody.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.Tape line 16
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 17
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 18
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 19
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 20
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.State line 21
  7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.Data line 22
  8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 23
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 25
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.readyState line 28
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 32
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 36
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 41
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyView line 45
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 50
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 54
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 57
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 65
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 68
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 76
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 78
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 84
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 90
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 91
  25. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.Label line 94
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.entry line 101
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 103
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 107
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 110
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 113
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.program line 117
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.frame line 128
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 133
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.cfg line 136
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.initialData line 139
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 152
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyData line 155
  38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 160
  39. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 163
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.joinTrace line 167
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 171
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 179
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 195
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 203
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 216
  46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 221
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 225
  48. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 242
  49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 247
  50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement line 252
  51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 255
  52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 271
  53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 286
  54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 292
  55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 310
  56. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 330
  57. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 334
  58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 345
  59. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 349
  60. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 368
  61. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 373
  62. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 389