OAI/Combinatorics/IndependentSets/Machines/PoweringMachineLoop.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 11
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 15) line 15
  3. inductive OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 19
  4. instance OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 23) line 23
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 27
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.HeaderState line 28
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.pushTrue line 30
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 35
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 47
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.headerProgram line 55
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.headerMachine line 71
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.initialTapes line 82
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.scanTapes line 86
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.finalTapes line 92
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 98
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 103
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.initializeStep line 107
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 117
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 128
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.scanTrace line 145
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.headerTrace line 162
  22. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.headerInTime line 174
  23. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.remainingRows line 183
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 186
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 189