OAI/Computability/MinUncut/Games/PoweringGlobalEnumeration.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 11
  2. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 22
  3. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 28
  4. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 31
  5. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 34
  6. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 37
  7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 40
  8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 44
  9. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 48
  10. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 51
  11. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 54
  12. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 57
  13. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 60
  14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 63
  15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 66
  16. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 69
  17. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 73
  18. def OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 77
  19. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 79
  20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 82