OAI/Combinatorics/IndependentSets/Machines/MachineExpanderTable.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.completeBudget line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.timePolynomial line 19
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 22
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 31
  6. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.TableRun line 66
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.initializeInTime line 78
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderTable.tableInTime line 95
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.cycleWords line 128
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 138
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 142
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 147
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.copyFrame line 157
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.returnFrame line 162
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.installedFrame line 167
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 171
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 176
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 188
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 202
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 213