OAI/Computability/MeanPayoff/EncodedArithmetic.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.take_size line 11
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.add_length line 26
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.neg_length line 28
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.half_length line 32
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.double_length line 33
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.addFold_length line 35
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.digitSum_le_size line 46
  8. def OAI.MeanPayoff.TreeDevice.Certified.Word.addFold line 58
  9. def OAI.MeanPayoff.TreeDevice.Certified.Word.sum line 74
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.addFold_val line 76
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.sum_val line 87
  12. def OAI.MeanPayoff.TreeDevice.Certified.Word.shiftStep line 93
  13. def OAI.MeanPayoff.TreeDevice.Certified.Word.shiftRight line 94
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.shiftRight_val line 107
  15. def OAI.MeanPayoff.TreeDevice.Certified.Counter.inc line 120
  16. def OAI.MeanPayoff.TreeDevice.Certified.Counter.step line 121
  17. def OAI.MeanPayoff.TreeDevice.Certified.Counter.word line 122
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.word_val line 123
  19. def OAI.MeanPayoff.TreeDevice.Certified.Counter.add line 125
  20. def OAI.MeanPayoff.TreeDevice.Certified.Counter.mul line 126
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.add_length line 127
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.Counter.mul_length line 128
  23. def OAI.MeanPayoff.TreeDevice.Certified.VectorRep line 137
  24. def OAI.MeanPayoff.TreeDevice.Certified.MaskRep line 140
  25. def OAI.MeanPayoff.TreeDevice.Certified.Word.constant line 144
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.Word.constant_val line 145
  27. def OAI.MeanPayoff.TreeDevice.Certified.Array.zero line 150
  28. def OAI.MeanPayoff.TreeDevice.Certified.Array.add line 151
  29. def OAI.MeanPayoff.TreeDevice.Certified.Array.sub line 152
  30. def OAI.MeanPayoff.TreeDevice.Certified.Array.min line 153
  31. def OAI.MeanPayoff.TreeDevice.Certified.Array.max line 154
  32. def OAI.MeanPayoff.TreeDevice.Certified.Array.average line 155
  33. def OAI.MeanPayoff.TreeDevice.Certified.Array.mul line 156
  34. def OAI.MeanPayoff.TreeDevice.Certified.Array.lt line 157
  35. def OAI.MeanPayoff.TreeDevice.Certified.Array.le line 158
  36. def OAI.MeanPayoff.TreeDevice.Certified.Array.scale line 159
  37. def OAI.MeanPayoff.TreeDevice.Certified.Array.translate line 160
  38. def OAI.MeanPayoff.TreeDevice.Certified.Array.complement line 161
  39. def OAI.MeanPayoff.TreeDevice.Certified.Array.mask line 162
  40. def OAI.MeanPayoff.TreeDevice.Certified.Array.doubleOn line 164
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.zip_ofFn line 167
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.zip_rep line 174
  43. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Data line 188
  44. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.k line 189
  45. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.m line 190
  46. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.alpha line 191
  47. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.beta line 192
  48. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.kn line 193
  49. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.kd line 194
  50. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.mn line 195
  51. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.md line 196
  52. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.times line 197
  53. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.shrink line 198
  54. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reduceK line 200
  55. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reduceM line 201
  56. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reweightK line 202
  57. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reweightM line 205
  58. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.density line 208
  59. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.total line 209
  60. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.parameterNumerator line 210
  61. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.parameterDenominator line 211
  62. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.small line 212
  63. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.measureLarge line 213
  64. def OAI.MeanPayoff.TreeDevice.Certified.RawBudget.smallMask line 215
  65. structure OAI.MeanPayoff.TreeDevice.Certified.RawBudget.Rep line 218
  66. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.times_val line 230
  67. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.shrink_fst line 232
  68. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.shrink_snd line 233
  69. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reduceK_rep line 235
  70. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reduceM_rep line 250
  71. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reweightK_rep line 265
  72. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.reweightM_rep line 298
  73. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.density_cast line 331
  74. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.total_eq line 336
  75. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.masked_eq line 350
  76. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.small_eq line 370
  77. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBudget.measureLarge_eq line 392