OAI/Combinatorics/IndependentSets/Machines/MachineOverlayRows.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.State line 15
  2. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.Label line 17
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.bodyIndex line 23
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.bodyIndex_injective line 25
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.trueBits line 29
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.instruction line 31
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowBits line 46
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowSteps line 49
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.resultTapes line 53
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.joinTrace line 58
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowTrace line 62
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowBits_eq_expanderRow line 204
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.machine line 218
  14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.VertexLabel line 229
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexInstruction line 231
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.streamFrame line 241
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.streamOutput line 246
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexSteps line 249
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.valueBound line 254
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowSizeBound line 255
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowCostBound line 256
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.value_le line 259
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowBits_length line 267
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowBits_length_le line 273
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.rowSteps_le line 280
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le_capacity line 290
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le line 315
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.streamFrame_afterRow line 322
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexSuffixTrace line 338
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexTrace line 412
  31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexInTime line 428
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.encodeWords_flatMap line 450
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.streamOutput_expanderRows line 456
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.expanderValues_bounded line 468
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayRows.vertexMachine line 474