OAI/Combinatorics/IndependentSets/Machines/PoweringMachineGlobal.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.Tape line 11
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.State line 14
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.placement line 17
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.inputTape line 21
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.outputTape line 24
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 27
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 28
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.enumeration line 30
  9. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 34
  10. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.Label line 36
  11. instance OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 39
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.initLabels line 43
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 44
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 45
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 47
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 50
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 53
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.main line 55
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.program line 57
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.atInit line 73
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.atGuard line 78
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.atBridge line 83
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.atVertex line 87
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.atFinish line 91
  25. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.machine line 97
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.machine_code line 108
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.machine_main line 111
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 113
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 116