OAI/Computability/MinUncut/Machines/MachineOverlayRows.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.State line 17
  2. inductive OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.Label line 19
  3. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.bodyIndex line 25
  4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.bodyIndex_injective line 27
  5. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.trueBits line 31
  6. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.instruction line 33
  7. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowBits line 48
  8. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowSteps line 51
  9. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.resultTapes line 55
  10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.joinTrace line 60
  11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowTrace line 64
  12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowBits_eq_expanderRow line 206
  13. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.machine line 219
  14. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.VertexLabel line 230
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexInstruction line 232
  16. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.streamFrame line 242
  17. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.streamOutput line 247
  18. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexSteps line 250
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.valueBound line 255
  20. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowSizeBound line 256
  21. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowCostBound line 257
  22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.value_le line 260
  23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowBits_length line 268
  24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowBits_length_le line 274
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.rowSteps_le line 281
  26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le_capacity line 291
  27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexSteps_le line 316
  28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.streamFrame_afterRow line 323
  29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexSuffixTrace line 339
  30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexTrace line 413
  31. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexInTime line 429
  32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.encodeWords_flatMap line 451
  33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.streamOutput_expanderRows line 457
  34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.expanderValues_bounded line 469
  35. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayRows.vertexMachine line 474