OAI/Computability/MinUncut/Machines/MachinePortReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.Alphabet line 14
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.State line 15
  3. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.clean line 17
  4. inductive OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.Label line 20
  5. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.exitAt line 26
  6. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.emit line 32
  7. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.instruction line 37
  8. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.steps line 58
  9. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.steps_le line 60
  10. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 65
  11. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.value line 71
  12. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.frame line 73
  13. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.joinTrace line 77
  14. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.reindexTrace line 81
  15. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.reindexInTime line 237
  16. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.machine line 256
  17. def OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.machineInTime line 267
  18. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePortReindex.lazy_value line 281