OAI/Computability/MeanPayoff/RawLabels.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.any_ofFn line 11
  2. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Input line 19
  3. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.width line 20
  4. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.lower line 21
  5. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.masses line 22
  6. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.a line 23
  7. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.b line 24
  8. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.box line 25
  9. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.small line 27
  10. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.base line 28
  11. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.baseLabels line 29
  12. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.piece line 30
  13. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.amount line 32
  14. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.center line 33
  15. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.child line 35
  16. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.provisional line 39
  17. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.continuation line 42
  18. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.lowerCap line 47
  19. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.upperCap line 48
  20. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.minus line 49
  21. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.plus line 51
  22. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Update line 53
  23. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.down line 54
  24. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.up line 56
  25. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.equalWord line 58
  26. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.different line 59
  27. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.changed line 61
  28. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.lowMark line 63
  29. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.highMark line 65
  30. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.selectBool line 67
  31. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.chooseBool line 68
  32. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Finish line 70
  33. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.highFinish line 71
  34. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.finish line 74
  35. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.widthLabels line 78
  36. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.basicCount line 81
  37. def OAI.MeanPayoff.TreeDevice.Certified.DetRaw.basic line 83
  38. structure OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Rep line 86
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.equalWord_eq line 94
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.different_eq line 105
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.base_eq line 114
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.baseLabels_eq line 117
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.small_eq line 120
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.piece_val line 130
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.amount_val line 138
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.box_rep line 143
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.center_rep line 155
  48. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.child_rep line 163
  49. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.provisional_rep line 183
  50. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.continuation_rep line 197
  51. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.minus_rep line 207
  52. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.plus_rep line 217
  53. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.choose_rep_bool line 227
  54. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.down_rep line 234
  55. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.up_rep line 241
  56. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.lt_eq line 248
  57. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.lowMark_eq line 253
  58. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.highMark_eq line 261
  59. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.chooseBool_eq line 269
  60. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.finish_eq line 276
  61. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.widthLabels_eq line 287
  62. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.basic_eq line 296