OAI/Computability/MeanPayoff/EncodedPrograms.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Zip.restData line 14
  2. def OAI.MeanPayoff.TreeDevice.Zip.stateData line 15
  3. def OAI.MeanPayoff.TreeDevice.Zip.countData line 16
  4. def OAI.MeanPayoff.TreeDevice.Zip.zip line 19
  5. def OAI.MeanPayoff.TreeDevice.Zip.row line 23
  6. def OAI.MeanPayoff.TreeDevice.Zip.localDevice line 26
  7. def OAI.MeanPayoff.TreeDevice.Zip.leftDevice line 28
  8. def OAI.MeanPayoff.TreeDevice.Zip.rightDevice line 30
  9. def OAI.MeanPayoff.TreeDevice.Zip.headArgsDevice line 32
  10. def OAI.MeanPayoff.TreeDevice.Zip.tailsDevice line 35
  11. def OAI.MeanPayoff.TreeDevice.Zip.headDevice line 40
  12. def OAI.MeanPayoff.TreeDevice.Zip.rowDevice line 43
  13. def OAI.MeanPayoff.TreeDevice.Zip.stateDevice line 46
  14. def OAI.MeanPayoff.TreeDevice.Zip.countDevice line 49
  15. def OAI.MeanPayoff.TreeDevice.Zip.initDevice line 52
  16. def OAI.MeanPayoff.TreeDevice.Zip.resultDevice line 55
  17. def OAI.MeanPayoff.TreeDevice.Zip.foldedDevice line 59
  18. def OAI.MeanPayoff.TreeDevice.Zip.rawDevice line 67
  19. theorem OAI.MeanPayoff.TreeDevice.Zip.fold_exact line 72
  20. def OAI.MeanPayoff.TreeDevice.Zip.device line 85
  21. theorem OAI.MeanPayoff.TreeDevice.Zip.length line 93
  22. theorem OAI.MeanPayoff.TreeDevice.Zip.ofFn line 98
  23. theorem OAI.MeanPayoff.TreeDevice.Zip.local_linear line 104
  24. theorem OAI.MeanPayoff.TreeDevice.Zip.left_linear line 105
  25. theorem OAI.MeanPayoff.TreeDevice.Zip.right_linear line 106
  26. theorem OAI.MeanPayoff.TreeDevice.Zip.headArgs_linear line 107
  27. theorem OAI.MeanPayoff.TreeDevice.Zip.tails_linear line 109
  28. theorem OAI.MeanPayoff.TreeDevice.Zip.head_polynomial line 111
  29. theorem OAI.MeanPayoff.TreeDevice.Zip.row_polynomial line 112
  30. theorem OAI.MeanPayoff.TreeDevice.Zip.fold_polynomial line 114
  31. theorem OAI.MeanPayoff.TreeDevice.Zip.state_linear line 124
  32. theorem OAI.MeanPayoff.TreeDevice.Zip.count_polynomial line 125
  33. theorem OAI.MeanPayoff.TreeDevice.Zip.init_polynomial line 127
  34. theorem OAI.MeanPayoff.TreeDevice.Zip.result_polynomial line 128
  35. theorem OAI.MeanPayoff.TreeDevice.Zip.folded_polynomial line 130
  36. theorem OAI.MeanPayoff.TreeDevice.Zip.raw_polynomial line 131
  37. theorem OAI.MeanPayoff.TreeDevice.Zip.polynomial line 132
  38. class OAI.MeanPayoff.TreeDevice.Certified.Encoding line 137
  39. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 141) line 141
  40. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 142) line 142
  41. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 143) line 143
  42. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 144) line 144
  43. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 146) line 146
  44. structure OAI.MeanPayoff.TreeDevice.Certified.Code line 148
  45. instance OAI.MeanPayoff.TreeDevice.Certified.Code.(instance at line 155) line 155
  46. def OAI.MeanPayoff.TreeDevice.Certified.Code.id line 157
  47. def OAI.MeanPayoff.TreeDevice.Certified.Code.const line 158
  48. def OAI.MeanPayoff.TreeDevice.Certified.Code.comp line 160
  49. def OAI.MeanPayoff.TreeDevice.Certified.Code.pair line 162
  50. def OAI.MeanPayoff.TreeDevice.Certified.Code.fst line 164
  51. def OAI.MeanPayoff.TreeDevice.Certified.Code.snd line 166
  52. def OAI.MeanPayoff.TreeDevice.Certified.Code.branch line 168
  53. def OAI.MeanPayoff.TreeDevice.Certified.Code.map line 171
  54. def OAI.MeanPayoff.TreeDevice.Certified.Code.envMap line 173
  55. def OAI.MeanPayoff.TreeDevice.Certified.Code.head line 175
  56. def OAI.MeanPayoff.TreeDevice.Certified.Code.tail line 177
  57. def OAI.MeanPayoff.TreeDevice.Certified.Code.cons line 179
  58. def OAI.MeanPayoff.TreeDevice.Certified.Code.reverse line 181
  59. def OAI.MeanPayoff.TreeDevice.Certified.Code.zip line 183
  60. def OAI.MeanPayoff.TreeDevice.Certified.Code.fold line 185
  61. def OAI.MeanPayoff.TreeDevice.Certified.Code.recode line 190
  62. def OAI.MeanPayoff.TreeDevice.Certified.Code.foldPrefix line 197
  63. def OAI.MeanPayoff.TreeDevice.Certified.Code.ext line 202
  64. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.id_eval line 205
  65. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.const_eval line 206
  66. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.comp_eval line 207
  67. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.pair_eval line 208
  68. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.fst_eval line 209
  69. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.snd_eval line 210
  70. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.branch_eval line 211
  71. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.map_eval line 212
  72. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.envMap_eval line 213
  73. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.head_eval line 214
  74. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.tail_eval line 215
  75. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.cons_eval line 216
  76. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.reverse_eval line 217
  77. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.zip_eval line 218
  78. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.ext_eval line 219
  79. abbrev OAI.MeanPayoff.TreeDevice.Certified.W line 227
  80. abbrev OAI.MeanPayoff.TreeDevice.Certified.Count line 228
  81. def OAI.MeanPayoff.TreeDevice.Certified.Code.swap line 232
  82. def OAI.MeanPayoff.TreeDevice.Certified.Code.count line 233
  83. def OAI.MeanPayoff.TreeDevice.Certified.Code.not line 234
  84. def OAI.MeanPayoff.TreeDevice.Certified.Code.and line 235
  85. def OAI.MeanPayoff.TreeDevice.Certified.Code.or line 236
  86. def OAI.MeanPayoff.TreeDevice.Certified.Code.empty line 237
  87. def OAI.MeanPayoff.TreeDevice.Certified.Code.drop line 239
  88. def OAI.MeanPayoff.TreeDevice.Certified.Code.nth line 241
  89. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.list_size_append line 243
  90. def OAI.MeanPayoff.TreeDevice.Certified.Code.consAcc line 249
  91. def OAI.MeanPayoff.TreeDevice.Certified.Code.revAppend line 250
  92. def OAI.MeanPayoff.TreeDevice.Certified.Code.append line 256
  93. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.revAppend_eval line 259
  94. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.append_eval line 262
  95. def OAI.MeanPayoff.TreeDevice.Certified.Code.flatten line 265
  96. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.flatten_eval line 272
  97. def OAI.MeanPayoff.TreeDevice.Certified.Code.filter line 277
  98. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.filter_eval line 282
  99. def OAI.MeanPayoff.TreeDevice.Certified.Code.any line 284
  100. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.empty_eval line 286
  101. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.count_eval line 288
  102. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.not_eval line 289
  103. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.nth_eval line 290
  104. structure OAI.MeanPayoff.TreeDevice.Certified.Digits line 295
  105. instance OAI.MeanPayoff.TreeDevice.Certified.(instance at line 297) line 297
  106. def OAI.MeanPayoff.TreeDevice.Certified.Word.add line 300
  107. def OAI.MeanPayoff.TreeDevice.Certified.Word.neg line 302
  108. def OAI.MeanPayoff.TreeDevice.Certified.Word.sub line 303
  109. def OAI.MeanPayoff.TreeDevice.Certified.Word.lt line 304
  110. def OAI.MeanPayoff.TreeDevice.Certified.Word.le line 306
  111. def OAI.MeanPayoff.TreeDevice.Certified.Word.min line 307
  112. def OAI.MeanPayoff.TreeDevice.Certified.Word.max line 308
  113. def OAI.MeanPayoff.TreeDevice.Certified.Word.half line 309
  114. def OAI.MeanPayoff.TreeDevice.Certified.Word.double line 320
  115. def OAI.MeanPayoff.TreeDevice.Certified.Word.average line 321
  116. def OAI.MeanPayoff.TreeDevice.Certified.Word.signDevice line 322
  117. def OAI.MeanPayoff.TreeDevice.Certified.Word.sign line 326
  118. def OAI.MeanPayoff.TreeDevice.Certified.Word.digitsDevice line 329
  119. def OAI.MeanPayoff.TreeDevice.Certified.Word.digits line 332
  120. def OAI.MeanPayoff.TreeDevice.Certified.Word.mulDigitsDevice line 334
  121. def OAI.MeanPayoff.TreeDevice.Certified.Word.mulDigits line 337
  122. def OAI.MeanPayoff.TreeDevice.Certified.Word.unsignedMul line 341
  123. def OAI.MeanPayoff.TreeDevice.Certified.Word.mul line 342
  124. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.add_val line 345
  125. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.neg_val line 346
  126. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.sub_val line 347
  127. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.lt_eval line 348
  128. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.le_eval line 349
  129. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.min_val line 353
  130. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.max_val line 354
  131. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.half_val line 355
  132. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.double_val line 356
  133. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.average_val line 357
  134. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.sign_eval line 358
  135. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.unsignedMul_val line 359
  136. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.mul_val line 363