OAI/Combinatorics/IndependentSets/Machines/MachineRegularOriginalClean.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.Tape line 11
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 12
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.State line 13
  4. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.Label line 15
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.instruction line 20
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 30
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 34
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.join_trace line 38
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 42
  10. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.Input line 76
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 81
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 95
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 105
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 149
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.steps line 163
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 167
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 170
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 178
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.machine line 197
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 208