OAI/Combinatorics/IndependentSets/Machines/MachineExpanderTableLoop.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.oldTableWord line 14
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 25
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 31
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 36
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 39
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 42
  9. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 46
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundarySingleStep line 57
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 63
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.clearRegister_position line 119
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.clearRegister_register line 122
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.clearRegister_idempotent line 125
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_reverse_update line 128
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutputTrace line 144
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltTrace line 176
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutputInTime line 191
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.reverseOutputHaltInTime line 204