OAI/Computability/MinUncut/Machines/PoweringMachineGlobal.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.Tape line 12
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.State line 15
  3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.placement line 18
  4. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.inputTape line 22
  5. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.outputTape line 25
  6. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 28
  7. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 29
  8. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.enumeration line 31
  9. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 35
  10. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.Label line 37
  11. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 40
  12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.initLabels line 44
  13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 45
  14. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 46
  15. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 48
  16. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 51
  17. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 54
  18. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.main line 56
  19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.program line 58
  20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.atInit line 74
  21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.atGuard line 79
  22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.atBridge line 84
  23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.atVertex line 88
  24. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.atFinish line 92
  25. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.machine line 98
  26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.machine_code line 109
  27. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.machine_main line 112
  28. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 114
  29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 117