OAI/Computability/MeanPayoff/Normalization.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.Normalize.Count line 8
  2. abbrev OAI.MeanPayoff.TreeDevice.Normalize.Edge line 9
  3. abbrev OAI.MeanPayoff.TreeDevice.Normalize.Arena line 10
  4. def OAI.MeanPayoff.TreeDevice.Normalize.countData line 12
  5. def OAI.MeanPayoff.TreeDevice.Normalize.edgeData line 13
  6. def OAI.MeanPayoff.TreeDevice.Normalize.edgesData line 14
  7. def OAI.MeanPayoff.TreeDevice.Normalize.ownersData line 15
  8. def OAI.MeanPayoff.TreeDevice.Normalize.arenaData line 16
  9. def OAI.MeanPayoff.TreeDevice.Normalize.edge line 18
  10. def OAI.MeanPayoff.TreeDevice.Normalize.sourceDevice line 19
  11. def OAI.MeanPayoff.TreeDevice.Normalize.moreDevice line 21
  12. def OAI.MeanPayoff.TreeDevice.Normalize.targetDevice line 23
  13. def OAI.MeanPayoff.TreeDevice.Normalize.weightDevice line 25
  14. def OAI.MeanPayoff.TreeDevice.Normalize.scaleArgsDevice line 27
  15. def OAI.MeanPayoff.TreeDevice.Normalize.scaleDevice line 29
  16. def OAI.MeanPayoff.TreeDevice.Normalize.edgeDevice line 32
  17. def OAI.MeanPayoff.TreeDevice.Normalize.arena line 35
  18. def OAI.MeanPayoff.TreeDevice.Normalize.nDevice line 36
  19. def OAI.MeanPayoff.TreeDevice.Normalize.restDevice line 37
  20. def OAI.MeanPayoff.TreeDevice.Normalize.ownersDevice line 38
  21. def OAI.MeanPayoff.TreeDevice.Normalize.edgesDevice line 39
  22. def OAI.MeanPayoff.TreeDevice.Normalize.mapDevice line 40
  23. def OAI.MeanPayoff.TreeDevice.Normalize.arenaDevice line 42
  24. def OAI.MeanPayoff.TreeDevice.Normalize.read line 45
  25. def OAI.MeanPayoff.TreeDevice.Normalize.device line 46
  26. def OAI.MeanPayoff.TreeDevice.Normalize.word line 48
  27. def OAI.MeanPayoff.TreeDevice.Normalize.encodedEdge line 49
  28. theorem OAI.MeanPayoff.TreeDevice.Normalize.word_val line 52
  29. theorem OAI.MeanPayoff.TreeDevice.Normalize.edge_exact line 55
  30. theorem OAI.MeanPayoff.TreeDevice.Normalize.exact line 58
  31. theorem OAI.MeanPayoff.TreeDevice.Normalize.source_linear line 63
  32. theorem OAI.MeanPayoff.TreeDevice.Normalize.more_linear line 64
  33. theorem OAI.MeanPayoff.TreeDevice.Normalize.target_linear line 65
  34. theorem OAI.MeanPayoff.TreeDevice.Normalize.weight_linear line 66
  35. theorem OAI.MeanPayoff.TreeDevice.Normalize.scaleArgs_linear line 67
  36. theorem OAI.MeanPayoff.TreeDevice.Normalize.scale_polynomial line 68
  37. theorem OAI.MeanPayoff.TreeDevice.Normalize.edge_polynomial line 70
  38. theorem OAI.MeanPayoff.TreeDevice.Normalize.n_linear line 72
  39. theorem OAI.MeanPayoff.TreeDevice.Normalize.rest_linear line 73
  40. theorem OAI.MeanPayoff.TreeDevice.Normalize.owners_linear line 74
  41. theorem OAI.MeanPayoff.TreeDevice.Normalize.edges_linear line 75
  42. theorem OAI.MeanPayoff.TreeDevice.Normalize.map_polynomial line 76
  43. theorem OAI.MeanPayoff.TreeDevice.Normalize.arena_polynomial line 78
  44. theorem OAI.MeanPayoff.TreeDevice.Normalize.polynomial line 81
  45. abbrev OAI.MeanPayoff.TreeDevice.Adjacency.Count line 85
  46. abbrev OAI.MeanPayoff.TreeDevice.Adjacency.Edge line 86
  47. abbrev OAI.MeanPayoff.TreeDevice.Adjacency.Edges line 87
  48. def OAI.MeanPayoff.TreeDevice.Adjacency.countData line 89
  49. def OAI.MeanPayoff.TreeDevice.Adjacency.edgeData line 90
  50. def OAI.MeanPayoff.TreeDevice.Adjacency.edgesData line 91
  51. def OAI.MeanPayoff.TreeDevice.Adjacency.test line 93
  52. def OAI.MeanPayoff.TreeDevice.Adjacency.testArgsDevice line 94
  53. def OAI.MeanPayoff.TreeDevice.Adjacency.testDevice line 97
  54. def OAI.MeanPayoff.TreeDevice.Adjacency.select line 101
  55. def OAI.MeanPayoff.TreeDevice.Adjacency.selectDevice line 103
  56. def OAI.MeanPayoff.TreeDevice.Adjacency.defaultEdge line 106
  57. def OAI.MeanPayoff.TreeDevice.Adjacency.nonempty line 107
  58. def OAI.MeanPayoff.TreeDevice.Adjacency.nonemptyDevice line 108
  59. def OAI.MeanPayoff.TreeDevice.Adjacency.vertex line 111
  60. abbrev OAI.MeanPayoff.TreeDevice.Adjacency.Args line 113
  61. def OAI.MeanPayoff.TreeDevice.Adjacency.argsData line 114
  62. def OAI.MeanPayoff.TreeDevice.Adjacency.localDevice line 115
  63. def OAI.MeanPayoff.TreeDevice.Adjacency.ownerDevice line 116
  64. def OAI.MeanPayoff.TreeDevice.Adjacency.addressDevice line 118
  65. def OAI.MeanPayoff.TreeDevice.Adjacency.selectArgsDevice line 120
  66. def OAI.MeanPayoff.TreeDevice.Adjacency.selectedDevice line 122
  67. def OAI.MeanPayoff.TreeDevice.Adjacency.vertexDevice line 125
  68. theorem OAI.MeanPayoff.TreeDevice.Adjacency.test_exact line 128
  69. theorem OAI.MeanPayoff.TreeDevice.Adjacency.select_exact line 138
  70. theorem OAI.MeanPayoff.TreeDevice.Adjacency.vertex_exact line 144
  71. theorem OAI.MeanPayoff.TreeDevice.Adjacency.testArgs_linear line 152
  72. theorem OAI.MeanPayoff.TreeDevice.Adjacency.test_polynomial line 154
  73. theorem OAI.MeanPayoff.TreeDevice.Adjacency.select_polynomial line 155
  74. theorem OAI.MeanPayoff.TreeDevice.Adjacency.nonempty_linear line 157
  75. theorem OAI.MeanPayoff.TreeDevice.Adjacency.local_linear line 158
  76. theorem OAI.MeanPayoff.TreeDevice.Adjacency.owner_linear line 159
  77. theorem OAI.MeanPayoff.TreeDevice.Adjacency.address_linear line 161
  78. theorem OAI.MeanPayoff.TreeDevice.Adjacency.selectArgs_linear line 162
  79. theorem OAI.MeanPayoff.TreeDevice.Adjacency.selected_polynomial line 163
  80. theorem OAI.MeanPayoff.TreeDevice.Adjacency.vertex_polynomial line 164
  81. abbrev OAI.MeanPayoff.TreeDevice.Rows.Edge line 169
  82. abbrev OAI.MeanPayoff.TreeDevice.Rows.Edges line 170
  83. abbrev OAI.MeanPayoff.TreeDevice.Rows.Count line 171
  84. abbrev OAI.MeanPayoff.TreeDevice.Rows.Arena line 172
  85. abbrev OAI.MeanPayoff.TreeDevice.Rows.State line 173
  86. def OAI.MeanPayoff.TreeDevice.Rows.ownersData line 175
  87. def OAI.MeanPayoff.TreeDevice.Rows.countData line 176
  88. def OAI.MeanPayoff.TreeDevice.Rows.edgesData line 177
  89. def OAI.MeanPayoff.TreeDevice.Rows.outputData line 178
  90. def OAI.MeanPayoff.TreeDevice.Rows.rowArgsData line 179
  91. def OAI.MeanPayoff.TreeDevice.Rows.rowOutputData line 180
  92. def OAI.MeanPayoff.TreeDevice.Rows.stateData line 181
  93. def OAI.MeanPayoff.TreeDevice.Rows.count line 183
  94. def OAI.MeanPayoff.TreeDevice.Rows.countDevice line 184
  95. theorem OAI.MeanPayoff.TreeDevice.Rows.count_eq line 187
  96. def OAI.MeanPayoff.TreeDevice.Rows.row line 189
  97. def OAI.MeanPayoff.TreeDevice.Rows.streamDevice line 191
  98. def OAI.MeanPayoff.TreeDevice.Rows.remainderDevice line 192
  99. def OAI.MeanPayoff.TreeDevice.Rows.addressDevice line 194
  100. def OAI.MeanPayoff.TreeDevice.Rows.ownerDevice line 196
  101. def OAI.MeanPayoff.TreeDevice.Rows.vertexArgsDevice line 198
  102. def OAI.MeanPayoff.TreeDevice.Rows.vertexDevice line 201
  103. def OAI.MeanPayoff.TreeDevice.Rows.rowDevice line 204
  104. def OAI.MeanPayoff.TreeDevice.Rows.descending line 206
  105. theorem OAI.MeanPayoff.TreeDevice.Rows.fold_exact line 210
  106. theorem OAI.MeanPayoff.TreeDevice.Rows.descending_ofFn line 222
  107. def OAI.MeanPayoff.TreeDevice.Rows.build line 233
  108. def OAI.MeanPayoff.TreeDevice.Rows.restDevice line 235
  109. def OAI.MeanPayoff.TreeDevice.Rows.edgesDevice line 236
  110. def OAI.MeanPayoff.TreeDevice.Rows.ownersDevice line 237
  111. def OAI.MeanPayoff.TreeDevice.Rows.reversedDevice line 238
  112. def OAI.MeanPayoff.TreeDevice.Rows.stateDevice line 240
  113. def OAI.MeanPayoff.TreeDevice.Rows.initDevice line 242
  114. def OAI.MeanPayoff.TreeDevice.Rows.resultDevice line 245
  115. def OAI.MeanPayoff.TreeDevice.Rows.foldedDevice line 247
  116. def OAI.MeanPayoff.TreeDevice.Rows.buildDevice line 252
  117. def OAI.MeanPayoff.TreeDevice.Rows.read line 257
  118. def OAI.MeanPayoff.TreeDevice.Rows.device line 258
  119. theorem OAI.MeanPayoff.TreeDevice.Rows.build_exact line 260
  120. theorem OAI.MeanPayoff.TreeDevice.Rows.exact line 272
  121. theorem OAI.MeanPayoff.TreeDevice.Rows.count_polynomial line 275
  122. theorem OAI.MeanPayoff.TreeDevice.Rows.stream_linear line 276
  123. theorem OAI.MeanPayoff.TreeDevice.Rows.remainder_linear line 277
  124. theorem OAI.MeanPayoff.TreeDevice.Rows.address_polynomial line 278
  125. theorem OAI.MeanPayoff.TreeDevice.Rows.owner_linear line 279
  126. theorem OAI.MeanPayoff.TreeDevice.Rows.vertexArgs_polynomial line 280
  127. theorem OAI.MeanPayoff.TreeDevice.Rows.vertex_polynomial line 282
  128. theorem OAI.MeanPayoff.TreeDevice.Rows.row_polynomial line 283
  129. theorem OAI.MeanPayoff.TreeDevice.Rows.fold_polynomial line 285
  130. theorem OAI.MeanPayoff.TreeDevice.Rows.rest_linear line 291
  131. theorem OAI.MeanPayoff.TreeDevice.Rows.edges_linear line 292
  132. theorem OAI.MeanPayoff.TreeDevice.Rows.owners_linear line 293
  133. theorem OAI.MeanPayoff.TreeDevice.Rows.reversed_polynomial line 294
  134. theorem OAI.MeanPayoff.TreeDevice.Rows.state_polynomial line 295
  135. theorem OAI.MeanPayoff.TreeDevice.Rows.init_polynomial line 297
  136. theorem OAI.MeanPayoff.TreeDevice.Rows.result_linear line 298
  137. theorem OAI.MeanPayoff.TreeDevice.Rows.folded_polynomial line 299
  138. theorem OAI.MeanPayoff.TreeDevice.Rows.build_polynomial line 300
  139. theorem OAI.MeanPayoff.TreeDevice.Rows.polynomial line 302