OAI/Combinatorics/IndependentSets/Machines/MachinePaddingRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.Control line 10
  2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.(instance at line 13) line 13
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.Tape line 17
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.Label line 18
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.Alphabet line 19
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.State line 21
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.bodyEntry line 23
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.extra line 26
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.program line 37
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.tapes line 40
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.cfg line 44
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.bodyTrace line 48
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.guard_succ line 66
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.guard_zero line 77
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.bump_step line 88
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.paddingBits line 100
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.steps line 104
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.loopTrace line 109
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.initialTapes line 131
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.initialize_step line 134
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.paddingTrace line 149
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.machine line 156
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddingRows.execution line 167