OAI/Combinatorics/IndependentSets/Machines/PoweringGlobalEnumeration.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 10
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 21
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 27
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 30
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 33
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 36
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 39
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 43
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 47
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 50
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 53
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 56
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 59
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 62
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 65
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 68
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 72
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 76
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 78
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 81
  21. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.Alphabet line 96
  22. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.address line 98
  23. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.value line 101
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.selected line 105
  25. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.instruction line 117
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.relationTrace line 123
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.steps_le line 143
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 153
  29. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRelation.machine line 158