OAI/Combinatorics/IndependentSets/Machines/MachineDrainMany.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.Alphabet line 13
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.Tapes line 14
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.LocalLabel line 15
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.Label line 16
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.Data line 17
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.entry line 19
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.localInstruction line 22
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.instruction line 26
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.result line 31
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.cost line 34
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalTapes line 36
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalRegister line 40
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalRegister_none line 45
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.steps line 48
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.sequence_result line 53
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.sequence_steps line 63
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalTapes_apply line 70
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalTapes_mem line 81
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalTapes_not_mem line 84
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.lengthSum line 87
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.lengthSum_mono line 91
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.steps_le line 100
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.steps_le_uniform line 116
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.trace line 131
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.execution line 152
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.workTapes line 164
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.mem_workTapes line 167
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.workTapes_length_le line 174
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.haltTapes line 179
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.finalTapes_workTapes line 182
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineDrainMany.cleanupTrace line 192