OAI/Computability/MeanPayoff/ArenaParsing.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.ArenaRead.Count line 8
  2. abbrev OAI.MeanPayoff.TreeDevice.ArenaRead.Fields line 9
  3. abbrev OAI.MeanPayoff.TreeDevice.ArenaRead.Arena line 10
  4. def OAI.MeanPayoff.TreeDevice.ArenaRead.restData line 11
  5. def OAI.MeanPayoff.TreeDevice.ArenaRead.countData line 12
  6. def OAI.MeanPayoff.TreeDevice.ArenaRead.edgesData line 13
  7. def OAI.MeanPayoff.TreeDevice.ArenaRead.fieldsData line 14
  8. def OAI.MeanPayoff.TreeDevice.ArenaRead.arenaData line 15
  9. def OAI.MeanPayoff.TreeDevice.ArenaRead.edgeArgs line 17
  10. def OAI.MeanPayoff.TreeDevice.ArenaRead.finish line 18
  11. def OAI.MeanPayoff.TreeDevice.ArenaRead.read line 19
  12. def OAI.MeanPayoff.TreeDevice.ArenaRead.headerDevice line 21
  13. def OAI.MeanPayoff.TreeDevice.ArenaRead.nDevice line 22
  14. def OAI.MeanPayoff.TreeDevice.ArenaRead.moreDevice line 24
  15. def OAI.MeanPayoff.TreeDevice.ArenaRead.mDevice line 26
  16. def OAI.MeanPayoff.TreeDevice.ArenaRead.lastDevice line 28
  17. def OAI.MeanPayoff.TreeDevice.ArenaRead.ownersDevice line 30
  18. def OAI.MeanPayoff.TreeDevice.ArenaRead.remainderDevice line 32
  19. def OAI.MeanPayoff.TreeDevice.ArenaRead.argsDevice line 34
  20. def OAI.MeanPayoff.TreeDevice.ArenaRead.parseDevice line 36
  21. def OAI.MeanPayoff.TreeDevice.ArenaRead.edgesDevice line 38
  22. def OAI.MeanPayoff.TreeDevice.ArenaRead.finishDevice line 40
  23. def OAI.MeanPayoff.TreeDevice.ArenaRead.device line 42
  24. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.code_length line 45
  25. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.raw_exact line 55
  26. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.game_exact line 73
  27. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.header_linear line 86
  28. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.n_linear line 87
  29. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.more_linear line 88
  30. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.m_linear line 89
  31. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.last_linear line 90
  32. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.owners_linear line 91
  33. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.remainder_linear line 92
  34. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.args_linear line 93
  35. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.parse_polynomial line 94
  36. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.edges_polynomial line 95
  37. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.finish_polynomial line 96
  38. theorem OAI.MeanPayoff.TreeDevice.ArenaRead.polynomial line 99
  39. abbrev OAI.MeanPayoff.TreeDevice.Scale.W line 104
  40. abbrev OAI.MeanPayoff.TreeDevice.Scale.Count line 105
  41. abbrev OAI.MeanPayoff.TreeDevice.Scale.State line 106
  42. def OAI.MeanPayoff.TreeDevice.Scale.stateData line 108
  43. def OAI.MeanPayoff.TreeDevice.Scale.countData line 109
  44. def OAI.MeanPayoff.TreeDevice.Scale.step line 111
  45. def OAI.MeanPayoff.TreeDevice.Scale.baseDevice line 112
  46. def OAI.MeanPayoff.TreeDevice.Scale.accDevice line 114
  47. def OAI.MeanPayoff.TreeDevice.Scale.stepDevice line 116
  48. def OAI.MeanPayoff.TreeDevice.Scale.scale line 119
  49. def OAI.MeanPayoff.TreeDevice.Scale.initDevice line 120
  50. def OAI.MeanPayoff.TreeDevice.Scale.device line 123
  51. theorem OAI.MeanPayoff.TreeDevice.Scale.step_first line 128
  52. theorem OAI.MeanPayoff.TreeDevice.Scale.step_val line 129
  53. theorem OAI.MeanPayoff.TreeDevice.Scale.fold_first line 130
  54. theorem OAI.MeanPayoff.TreeDevice.Scale.fold_val line 135
  55. theorem OAI.MeanPayoff.TreeDevice.Scale.exact line 143
  56. theorem OAI.MeanPayoff.TreeDevice.Scale.step_length line 147
  57. theorem OAI.MeanPayoff.TreeDevice.Scale.fold_length line 151
  58. theorem OAI.MeanPayoff.TreeDevice.Scale.base_linear line 162
  59. theorem OAI.MeanPayoff.TreeDevice.Scale.acc_linear line 163
  60. theorem OAI.MeanPayoff.TreeDevice.Scale.step_linear line 164
  61. theorem OAI.MeanPayoff.TreeDevice.Scale.fold_polynomial line 167
  62. theorem OAI.MeanPayoff.TreeDevice.Scale.init_linear line 186
  63. theorem OAI.MeanPayoff.TreeDevice.Scale.polynomial line 188
  64. def OAI.MeanPayoff.TreeDevice.Scale.oneWord line 191
  65. def OAI.MeanPayoff.TreeDevice.Scale.transform line 193
  66. def OAI.MeanPayoff.TreeDevice.Scale.transformDevice line 194
  67. theorem OAI.MeanPayoff.TreeDevice.Scale.transform_val line 197
  68. theorem OAI.MeanPayoff.TreeDevice.Scale.transform_polynomial line 202
  69. abbrev OAI.MeanPayoff.TreeDevice.CountTest.Count line 207
  70. def OAI.MeanPayoff.TreeDevice.CountTest.countData line 208
  71. def OAI.MeanPayoff.TreeDevice.CountTest.emptyStep line 210
  72. def OAI.MeanPayoff.TreeDevice.CountTest.emptyStepDevice line 211
  73. theorem OAI.MeanPayoff.TreeDevice.CountTest.fold_false line 214
  74. theorem OAI.MeanPayoff.TreeDevice.CountTest.fold_empty line 219
  75. def OAI.MeanPayoff.TreeDevice.CountTest.emptyDevice line 224
  76. theorem OAI.MeanPayoff.TreeDevice.CountTest.emptyStep_polynomial line 228
  77. theorem OAI.MeanPayoff.TreeDevice.CountTest.empty_polynomial line 230
  78. def OAI.MeanPayoff.TreeDevice.CountTest.equal line 237
  79. def OAI.MeanPayoff.TreeDevice.CountTest.forwardDevice line 239
  80. def OAI.MeanPayoff.TreeDevice.CountTest.backwardDevice line 242
  81. def OAI.MeanPayoff.TreeDevice.CountTest.device line 245
  82. theorem OAI.MeanPayoff.TreeDevice.CountTest.equal_eq line 248
  83. theorem OAI.MeanPayoff.TreeDevice.CountTest.forward_polynomial line 261
  84. theorem OAI.MeanPayoff.TreeDevice.CountTest.backward_polynomial line 263
  85. theorem OAI.MeanPayoff.TreeDevice.CountTest.polynomial line 265
  86. def OAI.MeanPayoff.TreeDevice.EnvFilter.stateData line 273
  87. def OAI.MeanPayoff.TreeDevice.EnvFilter.step line 274
  88. def OAI.MeanPayoff.TreeDevice.EnvFilter.envDevice line 277
  89. def OAI.MeanPayoff.TreeDevice.EnvFilter.accDevice line 279
  90. def OAI.MeanPayoff.TreeDevice.EnvFilter.testDevice line 281
  91. def OAI.MeanPayoff.TreeDevice.EnvFilter.consDevice line 284
  92. def OAI.MeanPayoff.TreeDevice.EnvFilter.stepDevice line 287
  93. def OAI.MeanPayoff.TreeDevice.EnvFilter.initDevice line 291
  94. def OAI.MeanPayoff.TreeDevice.EnvFilter.rawDevice line 294
  95. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.fold_exact line 301
  96. def OAI.MeanPayoff.TreeDevice.EnvFilter.device line 314
  97. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.env_linear line 318
  98. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.acc_linear line 319
  99. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.cons_linear line 320
  100. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.test_polynomial line 322
  101. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.step_polynomial line 325
  102. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.fold_polynomial line 327
  103. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.init_linear line 333
  104. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.raw_polynomial line 335
  105. theorem OAI.MeanPayoff.TreeDevice.EnvFilter.polynomial line 337