OAI/Combinatorics/IndependentSets/Machines/Tape3.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.Tape line 12
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.(instance at line 17) line 17
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.State line 22
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.clean line 24
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.clean_pair line 27
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.splitRoles line 30
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.splitView line 31
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyRoles line 35
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyView line 36
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.oldRoles line 40
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.splitRoles_left line 44
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.splitRoles_right line 47
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyRoles_left line 50
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyRoles_right line 53
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.oldRoles_injective line 56
  16. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.Label line 58
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.program line 68
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.frame line 105
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.initialTapes line 110
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.loopTapes line 112
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finalTapes line 117
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.joinTrace line 119
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.dummyTrace line 123
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.oldTrace line 152
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.prefixSteps line 184
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.prefixTrace line 187
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.vertexBlock line 269
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.bodySteps line 273
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.frame_old_empty line 279
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.bodyTrace line 284
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.drainPhase line 396
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finishSteps line 407
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTable.finishTrace line 409