OAI/Combinatorics/IndependentSets/Machines/Label.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.Label line 15
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.State line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.addressIndex line 18
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.addressIndex_injective line 20
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.fields line 24
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexInstruction line 26
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.instruction line 35
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexRowBits line 40
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexMappedTapes line 44
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexResultTapes line 48
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexSteps line 53
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.rowBits line 57
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.mappedTapes line 60
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.resultTapes line 63
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.steps line 68
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.reindexRowTrace line 71
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.rowTrace line 134
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.rowBits_eq_moveRow line 155
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.machine line 163
  20. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.Buffer line 174
  21. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.StreamState line 175
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamClean line 177
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.relationStateEquiv line 180
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy line 187
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy_step line 192
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.bodyIndex line 217
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.bodyIndex_injective line 219
  28. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.StreamLabel line 224
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamInstruction line 230
  30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.inputRowBits line 248
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamRowSteps line 251
  32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamResultTapes line 256
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.joinTrace line 261
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyRows.streamRowTrace line 265