OAI/Computability/MeanPayoff/WordDecoding.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Multiply.step_length line 10
  2. theorem OAI.MeanPayoff.TreeDevice.Multiply.fold_length line 19
  3. theorem OAI.MeanPayoff.TreeDevice.Multiply.fold_polynomial line 31
  4. theorem OAI.MeanPayoff.TreeDevice.Multiply.init_polynomial line 66
  5. theorem OAI.MeanPayoff.TreeDevice.Multiply.polynomial line 71
  6. abbrev OAI.MeanPayoff.TreeDevice.Prefix.Count line 79
  7. abbrev OAI.MeanPayoff.TreeDevice.Prefix.State line 80
  8. def OAI.MeanPayoff.TreeDevice.Prefix.countData line 81
  9. def OAI.MeanPayoff.TreeDevice.Prefix.listsData line 82
  10. def OAI.MeanPayoff.TreeDevice.Prefix.stateData line 83
  11. def OAI.MeanPayoff.TreeDevice.Prefix.inputData line 84
  12. def OAI.MeanPayoff.TreeDevice.Prefix.step line 86
  13. def OAI.MeanPayoff.TreeDevice.Prefix.countDevice line 90
  14. def OAI.MeanPayoff.TreeDevice.Prefix.restDevice line 92
  15. def OAI.MeanPayoff.TreeDevice.Prefix.bitDevice line 94
  16. def OAI.MeanPayoff.TreeDevice.Prefix.doneDevice line 95
  17. def OAI.MeanPayoff.TreeDevice.Prefix.testDevice line 97
  18. def OAI.MeanPayoff.TreeDevice.Prefix.putDevice line 99
  19. def OAI.MeanPayoff.TreeDevice.Prefix.incDevice line 102
  20. def OAI.MeanPayoff.TreeDevice.Prefix.stopDevice line 105
  21. def OAI.MeanPayoff.TreeDevice.Prefix.stepDevice line 108
  22. def OAI.MeanPayoff.TreeDevice.Prefix.read line 111
  23. def OAI.MeanPayoff.TreeDevice.Prefix.initDevice line 115
  24. def OAI.MeanPayoff.TreeDevice.Prefix.finishDevice line 118
  25. def OAI.MeanPayoff.TreeDevice.Prefix.device line 121
  26. theorem OAI.MeanPayoff.TreeDevice.Prefix.read_from_done line 124
  27. theorem OAI.MeanPayoff.TreeDevice.Prefix.length_prefix line 133
  28. theorem OAI.MeanPayoff.TreeDevice.Prefix.exact line 148
  29. theorem OAI.MeanPayoff.TreeDevice.Prefix.count_linear line 152
  30. theorem OAI.MeanPayoff.TreeDevice.Prefix.rest_linear line 154
  31. theorem OAI.MeanPayoff.TreeDevice.Prefix.bit_linear line 156
  32. theorem OAI.MeanPayoff.TreeDevice.Prefix.done_linear line 157
  33. theorem OAI.MeanPayoff.TreeDevice.Prefix.test_linear line 158
  34. theorem OAI.MeanPayoff.TreeDevice.Prefix.increment_linear line 159
  35. theorem OAI.MeanPayoff.TreeDevice.Prefix.put_linear line 161
  36. theorem OAI.MeanPayoff.TreeDevice.Prefix.inc_linear line 164
  37. theorem OAI.MeanPayoff.TreeDevice.Prefix.stop_linear line 167
  38. theorem OAI.MeanPayoff.TreeDevice.Prefix.step_linear line 169
  39. theorem OAI.MeanPayoff.TreeDevice.Prefix.step_size line 172
  40. theorem OAI.MeanPayoff.TreeDevice.Prefix.polynomial line 179
  41. abbrev OAI.MeanPayoff.TreeDevice.Split.State line 188
  42. def OAI.MeanPayoff.TreeDevice.Split.stateData line 189
  43. def OAI.MeanPayoff.TreeDevice.Split.inputData line 190
  44. def OAI.MeanPayoff.TreeDevice.Split.step line 192
  45. def OAI.MeanPayoff.TreeDevice.Split.fstDevice line 193
  46. def OAI.MeanPayoff.TreeDevice.Split.sndDevice line 195
  47. def OAI.MeanPayoff.TreeDevice.Split.headDevice line 197
  48. def OAI.MeanPayoff.TreeDevice.Split.pushDevice line 199
  49. def OAI.MeanPayoff.TreeDevice.Split.stepDevice line 201
  50. def OAI.MeanPayoff.TreeDevice.Split.split line 203
  51. def OAI.MeanPayoff.TreeDevice.Split.initDevice line 206
  52. def OAI.MeanPayoff.TreeDevice.Split.finishDevice line 210
  53. def OAI.MeanPayoff.TreeDevice.Split.device line 212
  54. theorem OAI.MeanPayoff.TreeDevice.Split.fold_exact line 215
  55. theorem OAI.MeanPayoff.TreeDevice.Split.exact line 227
  56. theorem OAI.MeanPayoff.TreeDevice.Split.fst_linear line 231
  57. theorem OAI.MeanPayoff.TreeDevice.Split.snd_linear line 232
  58. theorem OAI.MeanPayoff.TreeDevice.Split.head_linear line 233
  59. theorem OAI.MeanPayoff.TreeDevice.Split.push_linear line 234
  60. theorem OAI.MeanPayoff.TreeDevice.Split.step_linear line 236
  61. theorem OAI.MeanPayoff.TreeDevice.Split.step_size line 239
  62. theorem OAI.MeanPayoff.TreeDevice.Split.polynomial line 246
  63. abbrev OAI.MeanPayoff.TreeDevice.IntegerRead.W line 255
  64. def OAI.MeanPayoff.TreeDevice.IntegerRead.positive line 256
  65. def OAI.MeanPayoff.TreeDevice.IntegerRead.minusOne line 257
  66. def OAI.MeanPayoff.TreeDevice.IntegerRead.decrement line 258
  67. def OAI.MeanPayoff.TreeDevice.IntegerRead.positiveDevice line 260
  68. def OAI.MeanPayoff.TreeDevice.IntegerRead.decrementDevice line 264
  69. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.decrement_val line 267
  70. def OAI.MeanPayoff.TreeDevice.IntegerRead.readNat line 271
  71. def OAI.MeanPayoff.TreeDevice.IntegerRead.natFieldsDevice line 276
  72. def OAI.MeanPayoff.TreeDevice.IntegerRead.natDevice line 279
  73. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.nat_encode line 282
  74. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.nat_value line 291
  75. abbrev OAI.MeanPayoff.TreeDevice.IntegerRead.Parsed line 296
  76. def OAI.MeanPayoff.TreeDevice.IntegerRead.parsedData line 297
  77. def OAI.MeanPayoff.TreeDevice.IntegerRead.signed line 299
  78. def OAI.MeanPayoff.TreeDevice.IntegerRead.readInt line 300
  79. def OAI.MeanPayoff.TreeDevice.IntegerRead.signTest line 302
  80. def OAI.MeanPayoff.TreeDevice.IntegerRead.magnitude line 304
  81. def OAI.MeanPayoff.TreeDevice.IntegerRead.remainder line 306
  82. def OAI.MeanPayoff.TreeDevice.IntegerRead.negativeMagnitude line 308
  83. def OAI.MeanPayoff.TreeDevice.IntegerRead.chosenMagnitude line 310
  84. def OAI.MeanPayoff.TreeDevice.IntegerRead.signedDevice line 313
  85. def OAI.MeanPayoff.TreeDevice.IntegerRead.intFieldsDevice line 315
  86. def OAI.MeanPayoff.TreeDevice.IntegerRead.intDevice line 318
  87. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.int_remainder line 321
  88. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.int_value line 324
  89. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.positive_linear line 331
  90. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.decrement_linear line 335
  91. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.natFields_polynomial line 338
  92. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.nat_polynomial line 342
  93. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.signTest_linear line 346
  94. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.magnitude_linear line 347
  95. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.remainder_linear line 348
  96. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.negative_polynomial line 349
  97. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.chosen_polynomial line 351
  98. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.signed_polynomial line 353
  99. theorem OAI.MeanPayoff.TreeDevice.IntegerRead.int_polynomial line 356