OAI/Combinatorics/IndependentSets/Machines/PoweringMachineRowBody.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.capacity line 15
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 16
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.State line 17
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.commands line 19
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.Label line 22
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.planMain line 26
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 33
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.entry line 40
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 43
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 47
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 51
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 56
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 71
  14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.instruction line 85
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 96
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 100
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.rowWords line 105
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 110
  19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 117
  20. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.planSteps line 125
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 130
  22. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.steps line 143
  23. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.Ready line 148
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.plan_other line 153
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 166
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 173
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 183
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 205
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 218
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 243
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 262
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 278
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 307
  34. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.budget line 359
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.steps_le line 363
  36. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 374