OAI/Combinatorics/IndependentSets/Machines/PoweringMachineOuterLoop.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 12
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.State line 13
  3. structure OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 15
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.counter line 23
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 26
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 33
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 52
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 58
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 61
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 79
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 83
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.steps line 91
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 97
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 109
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 134
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 139
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 156
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 163
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 189
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 201
  21. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 267