OAI/Combinatorics/IndependentSets/Machines/PoweringMachineEqualityField.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.Alphabet line 16
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.Tape line 17
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.State line 18
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.Label line 19
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.entry line 22
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.instruction line 24
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.endpoint line 40
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.resultBit line 44
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes line 48
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes line 54
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.steps line 64
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.steps_le line 71
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_other line 87
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.wordTapes_role line 107
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_other line 128
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_role line 143
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.finalTapes_output line 154
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.joinTrace line 167
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.fieldTrace line 171
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.fieldInTime line 273
  21. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineEqualityField.machine line 296