OAI/Combinatorics/IndependentSets/Machines/PoweringMachineRotor.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.Alphabet line 16
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverseRole line 18
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.endpointRole line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 24
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 25
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 26
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 27
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 29
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 30
  10. inductive OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.Label line 32
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.instruction line 37
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverseId line 46
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 49
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 52
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 55
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 65
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.afterReverse line 71
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.finalTapes line 76
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.steps line 82
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 86
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 136
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 147
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.steps_le line 156
  24. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRotor.machine line 173