OAI/Computability/MeanPayoff/Counters.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.Address.W line 8
  2. abbrev OAI.MeanPayoff.TreeDevice.Address.Count line 9
  3. abbrev OAI.MeanPayoff.TreeDevice.Address.State line 10
  4. def OAI.MeanPayoff.TreeDevice.Address.countData line 11
  5. def OAI.MeanPayoff.TreeDevice.Address.stateData line 12
  6. def OAI.MeanPayoff.TreeDevice.Address.inputData line 13
  7. def OAI.MeanPayoff.TreeDevice.Address.dec line 15
  8. def OAI.MeanPayoff.TreeDevice.Address.test line 16
  9. def OAI.MeanPayoff.TreeDevice.Address.step line 17
  10. theorem OAI.MeanPayoff.TreeDevice.Address.dec_val line 20
  11. theorem OAI.MeanPayoff.TreeDevice.Address.test_eq line 23
  12. def OAI.MeanPayoff.TreeDevice.Address.wordDevice line 27
  13. def OAI.MeanPayoff.TreeDevice.Address.listDevice line 29
  14. def OAI.MeanPayoff.TreeDevice.Address.decDevice line 31
  15. def OAI.MeanPayoff.TreeDevice.Address.testDevice line 33
  16. def OAI.MeanPayoff.TreeDevice.Address.newWordDevice line 35
  17. def OAI.MeanPayoff.TreeDevice.Address.newCountDevice line 37
  18. def OAI.MeanPayoff.TreeDevice.Address.nextDevice line 39
  19. def OAI.MeanPayoff.TreeDevice.Address.stepDevice line 42
  20. def OAI.MeanPayoff.TreeDevice.Address.read line 45
  21. def OAI.MeanPayoff.TreeDevice.Address.initDevice line 46
  22. def OAI.MeanPayoff.TreeDevice.Address.finishDevice line 49
  23. def OAI.MeanPayoff.TreeDevice.Address.device line 54
  24. theorem OAI.MeanPayoff.TreeDevice.Address.fold_stopped line 59
  25. theorem OAI.MeanPayoff.TreeDevice.Address.fold_count line 67
  26. theorem OAI.MeanPayoff.TreeDevice.Address.exact line 82
  27. theorem OAI.MeanPayoff.TreeDevice.Address.word_linear line 86
  28. theorem OAI.MeanPayoff.TreeDevice.Address.list_linear line 87
  29. theorem OAI.MeanPayoff.TreeDevice.Address.dec_linear line 88
  30. theorem OAI.MeanPayoff.TreeDevice.Address.test_linear line 90
  31. theorem OAI.MeanPayoff.TreeDevice.Address.newWord_linear line 92
  32. theorem OAI.MeanPayoff.TreeDevice.Address.newCount_linear line 93
  33. theorem OAI.MeanPayoff.TreeDevice.Address.next_linear line 94
  34. theorem OAI.MeanPayoff.TreeDevice.Address.step_linear line 95
  35. theorem OAI.MeanPayoff.TreeDevice.Address.step_word_length line 98
  36. theorem OAI.MeanPayoff.TreeDevice.Address.step_count_length line 107
  37. theorem OAI.MeanPayoff.TreeDevice.Address.fold_length line 112
  38. theorem OAI.MeanPayoff.TreeDevice.Address.count_size line 126
  39. theorem OAI.MeanPayoff.TreeDevice.Address.fold_polynomial line 131
  40. theorem OAI.MeanPayoff.TreeDevice.Address.init_polynomial line 163
  41. theorem OAI.MeanPayoff.TreeDevice.Address.finish_polynomial line 165
  42. theorem OAI.MeanPayoff.TreeDevice.Address.polynomial line 167
  43. abbrev OAI.MeanPayoff.TreeDevice.Header.W line 172
  44. abbrev OAI.MeanPayoff.TreeDevice.Header.Count line 173
  45. abbrev OAI.MeanPayoff.TreeDevice.Header.Numbers line 174
  46. abbrev OAI.MeanPayoff.TreeDevice.Header.Fields line 175
  47. abbrev OAI.MeanPayoff.TreeDevice.Header.Result line 176
  48. def OAI.MeanPayoff.TreeDevice.Header.restData line 177
  49. def OAI.MeanPayoff.TreeDevice.Header.countData line 178
  50. def OAI.MeanPayoff.TreeDevice.Header.numbersData line 179
  51. def OAI.MeanPayoff.TreeDevice.Header.fieldsData line 180
  52. def OAI.MeanPayoff.TreeDevice.Header.resultData line 181
  53. def OAI.MeanPayoff.TreeDevice.Header.numbers line 183
  54. def OAI.MeanPayoff.TreeDevice.Header.nCount line 186
  55. def OAI.MeanPayoff.TreeDevice.Header.mCount line 187
  56. def OAI.MeanPayoff.TreeDevice.Header.partition line 188
  57. def OAI.MeanPayoff.TreeDevice.Header.finish line 189
  58. def OAI.MeanPayoff.TreeDevice.Header.read line 190
  59. def OAI.MeanPayoff.TreeDevice.Header.numbersDevice line 192
  60. def OAI.MeanPayoff.TreeDevice.Header.inputDevice line 194
  61. def OAI.MeanPayoff.TreeDevice.Header.nWordDevice line 195
  62. def OAI.MeanPayoff.TreeDevice.Header.moreDevice line 197
  63. def OAI.MeanPayoff.TreeDevice.Header.mWordDevice line 199
  64. def OAI.MeanPayoff.TreeDevice.Header.remainderDevice line 201
  65. def OAI.MeanPayoff.TreeDevice.Header.nCountDevice line 203
  66. def OAI.MeanPayoff.TreeDevice.Header.mCountDevice line 205
  67. def OAI.MeanPayoff.TreeDevice.Header.partitionDevice line 207
  68. def OAI.MeanPayoff.TreeDevice.Header.finishDevice line 209
  69. def OAI.MeanPayoff.TreeDevice.Header.device line 211
  70. theorem OAI.MeanPayoff.TreeDevice.Header.numbers_exact line 214
  71. theorem OAI.MeanPayoff.TreeDevice.Header.word_val line 219
  72. theorem OAI.MeanPayoff.TreeDevice.Header.exact line 223
  73. theorem OAI.MeanPayoff.TreeDevice.Header.input_linear line 241
  74. theorem OAI.MeanPayoff.TreeDevice.Header.nWord_linear line 242
  75. theorem OAI.MeanPayoff.TreeDevice.Header.more_linear line 243
  76. theorem OAI.MeanPayoff.TreeDevice.Header.mWord_linear line 244
  77. theorem OAI.MeanPayoff.TreeDevice.Header.remainder_linear line 245
  78. theorem OAI.MeanPayoff.TreeDevice.Header.nCount_polynomial line 246
  79. theorem OAI.MeanPayoff.TreeDevice.Header.mCount_polynomial line 248
  80. theorem OAI.MeanPayoff.TreeDevice.Header.partition_polynomial line 250
  81. theorem OAI.MeanPayoff.TreeDevice.Header.finish_polynomial line 252
  82. theorem OAI.MeanPayoff.TreeDevice.Header.numbers_polynomial line 254
  83. theorem OAI.MeanPayoff.TreeDevice.Header.polynomial line 257
  84. abbrev OAI.MeanPayoff.TreeDevice.EdgeRead.W line 263
  85. abbrev OAI.MeanPayoff.TreeDevice.EdgeRead.Count line 264
  86. abbrev OAI.MeanPayoff.TreeDevice.EdgeRead.Edge line 265
  87. abbrev OAI.MeanPayoff.TreeDevice.EdgeRead.Words line 266
  88. abbrev OAI.MeanPayoff.TreeDevice.EdgeRead.Fields line 267
  89. def OAI.MeanPayoff.TreeDevice.EdgeRead.restData line 268
  90. def OAI.MeanPayoff.TreeDevice.EdgeRead.countData line 269
  91. def OAI.MeanPayoff.TreeDevice.EdgeRead.edgeData line 270
  92. def OAI.MeanPayoff.TreeDevice.EdgeRead.wordsData line 271
  93. def OAI.MeanPayoff.TreeDevice.EdgeRead.fieldsData line 272
  94. def OAI.MeanPayoff.TreeDevice.EdgeRead.words line 274
  95. def OAI.MeanPayoff.TreeDevice.EdgeRead.source line 278
  96. def OAI.MeanPayoff.TreeDevice.EdgeRead.target line 279
  97. def OAI.MeanPayoff.TreeDevice.EdgeRead.edge line 280
  98. def OAI.MeanPayoff.TreeDevice.EdgeRead.finish line 281
  99. def OAI.MeanPayoff.TreeDevice.EdgeRead.read line 282
  100. def OAI.MeanPayoff.TreeDevice.EdgeRead.wordsDevice line 284
  101. def OAI.MeanPayoff.TreeDevice.EdgeRead.inputDevice line 287
  102. def OAI.MeanPayoff.TreeDevice.EdgeRead.sourceWordDevice line 288
  103. def OAI.MeanPayoff.TreeDevice.EdgeRead.moreDevice line 290
  104. def OAI.MeanPayoff.TreeDevice.EdgeRead.targetWordDevice line 292
  105. def OAI.MeanPayoff.TreeDevice.EdgeRead.lastDevice line 294
  106. def OAI.MeanPayoff.TreeDevice.EdgeRead.weightDevice line 296
  107. def OAI.MeanPayoff.TreeDevice.EdgeRead.remainderDevice line 298
  108. def OAI.MeanPayoff.TreeDevice.EdgeRead.sourceDecDevice line 300
  109. def OAI.MeanPayoff.TreeDevice.EdgeRead.targetDecDevice line 302
  110. def OAI.MeanPayoff.TreeDevice.EdgeRead.sourceDevice line 304
  111. def OAI.MeanPayoff.TreeDevice.EdgeRead.targetDevice line 306
  112. def OAI.MeanPayoff.TreeDevice.EdgeRead.edgeDevice line 308
  113. def OAI.MeanPayoff.TreeDevice.EdgeRead.finishDevice line 310
  114. def OAI.MeanPayoff.TreeDevice.EdgeRead.device line 312
  115. def OAI.MeanPayoff.TreeDevice.EdgeRead.encodedWord line 315
  116. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.encodedWord_val line 319
  117. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.words_exact line 329
  118. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.exact line 335
  119. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.words_polynomial line 345
  120. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.input_linear line 349
  121. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.sourceWord_linear line 350
  122. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.more_linear line 351
  123. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.targetWord_linear line 352
  124. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.last_linear line 353
  125. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.weight_linear line 354
  126. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.remainder_linear line 355
  127. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.sourceDec_linear line 356
  128. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.targetDec_linear line 357
  129. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.source_polynomial line 358
  130. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.target_polynomial line 360
  131. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.edge_polynomial line 362
  132. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.finish_polynomial line 364
  133. theorem OAI.MeanPayoff.TreeDevice.EdgeRead.polynomial line 366