OAI/Combinatorics/IndependentSets/Machines/Enumeration.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.rowBase line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 30
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 43
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 66
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 72
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 76
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 89
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 102
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 125
  11. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.OtherRegisters line 139
  12. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.Master line 140
  13. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.CompareState line 141
  14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.RowState line 142
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.compareEquiv line 144
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.rowEquiv line 147
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 153
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 157
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 161
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 165
  21. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.withBuffer line 169
  22. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.clean line 172
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 174
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 177
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 180
  26. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.clearBuffer line 183
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 186
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 191