OAI/Computability/MinUncut/Machines/MachineLazyRows.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.Label line 16
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.State line 17
  3. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.addressIndex line 19
  4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.addressIndex_injective line 21
  5. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.fields line 25
  6. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexInstruction line 27
  7. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.instruction line 36
  8. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexRowBits line 41
  9. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexMappedTapes line 45
  10. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexResultTapes line 49
  11. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexSteps line 54
  12. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.rowBits line 58
  13. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.mappedTapes line 61
  14. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.resultTapes line 64
  15. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.steps line 69
  16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexRowTrace line 72
  17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.rowTrace line 135
  18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.rowBits_eq_moveRow line 156
  19. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.machine line 164
  20. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.Buffer line 175
  21. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.StreamState line 176
  22. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamClean line 178
  23. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.relationStateEquiv line 181
  24. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy line 188
  25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamRelationCopy_step line 193
  26. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.bodyIndex line 218
  27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.bodyIndex_injective line 220
  28. inductive OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.StreamLabel line 225
  29. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamInstruction line 231
  30. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.inputRowBits line 249
  31. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamRowSteps line 252
  32. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamResultTapes line 257
  33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.joinTrace line 262
  34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamRowTrace line 266
  35. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.VertexLabel line 454
  36. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexInstruction line 456
  37. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.recordsInput line 466
  38. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.recordsOutput line 469
  39. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamFrame line 472
  40. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexSteps line 477
  41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.recordsInput_eq_codec line 483
  42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamFrame_afterRow line 492
  43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexSuffixTrace line 509
  44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexTrace line 593
  45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.encodeWords_flatMap line 609
  46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.recordsOutput_lazy line 615
  47. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.valueBound line 630
  48. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.rowSizeBound line 631
  49. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.rowCostBound line 632
  50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexValue_le line 635
  51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.reindexRowBits_length_le line 644
  52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.streamRowSteps_le line 654
  53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le_capacity line 666
  54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexSteps_le line 691
  55. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexInTime line 697
  56. def OAI.MinUncutGames.Foundations.Complexity.MachineLazyRows.vertexMachine line 718