OAI/Computability/MeanPayoff/OperatorDevices.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Select.choose line 9
  2. abbrev OAI.MeanPayoff.TreeDevice.Select.flow line 11
  3. abbrev OAI.MeanPayoff.TreeDevice.Select.program line 26
  4. abbrev OAI.MeanPayoff.TreeDevice.Select.cfg line 27
  5. theorem OAI.MeanPayoff.TreeDevice.Select.popHop line 30
  6. def OAI.MeanPayoff.TreeDevice.Select.limit line 40
  7. theorem OAI.MeanPayoff.TreeDevice.Select.runs line 43
  8. def OAI.MeanPayoff.TreeDevice.Select.device line 75
  9. def OAI.MeanPayoff.TreeDevice.Device.extFun line 83
  10. def OAI.MeanPayoff.TreeDevice.Order.low line 92
  11. def OAI.MeanPayoff.TreeDevice.Order.high line 95
  12. def OAI.MeanPayoff.TreeDevice.Order.minDevice line 98
  13. def OAI.MeanPayoff.TreeDevice.Order.swapDevice line 101
  14. def OAI.MeanPayoff.TreeDevice.Order.maxDevice line 104
  15. theorem OAI.MeanPayoff.TreeDevice.Order.low_val line 107
  16. theorem OAI.MeanPayoff.TreeDevice.Order.high_val line 114
  17. def OAI.MeanPayoff.TreeDevice.Order.clipped line 121
  18. def OAI.MeanPayoff.TreeDevice.Order.clipDevice line 124
  19. theorem OAI.MeanPayoff.TreeDevice.Order.clipped_val line 130
  20. def OAI.MeanPayoff.TreeDevice.Order.clipVectorDevice line 134
  21. theorem OAI.MeanPayoff.TreeDevice.Order.clipping_exact line 138
  22. def OAI.MeanPayoff.TreeDevice.Add.pairWord line 150
  23. def OAI.MeanPayoff.TreeDevice.Add.sumPair line 151
  24. abbrev OAI.MeanPayoff.TreeDevice.Add.flow line 153
  25. abbrev OAI.MeanPayoff.TreeDevice.Add.program line 163
  26. def OAI.MeanPayoff.TreeDevice.Add.limit line 165
  27. theorem OAI.MeanPayoff.TreeDevice.Add.runs line 168
  28. def OAI.MeanPayoff.TreeDevice.Add.device line 196
  29. theorem OAI.MeanPayoff.TreeDevice.Add.sumPair_val line 199
  30. theorem OAI.MeanPayoff.TreeDevice.compose_limit line 209
  31. theorem OAI.MeanPayoff.TreeDevice.dup_limit line 213
  32. theorem OAI.MeanPayoff.TreeDevice.pairMap_limit line 219
  33. theorem OAI.MeanPayoff.TreeDevice.fanout_limit line 228
  34. theorem OAI.MeanPayoff.TreeDevice.first_limit line 235
  35. theorem OAI.MeanPayoff.TreeDevice.second_limit line 241
  36. theorem OAI.MeanPayoff.TreeDevice.Select.limit_le line 246
  37. theorem OAI.MeanPayoff.TreeDevice.wordSize_bound line 253
  38. theorem OAI.MeanPayoff.TreeDevice.digits_le_wordSize line 257
  39. theorem OAI.MeanPayoff.TreeDevice.bitSize_bound line 266
  40. abbrev OAI.MeanPayoff.TreeDevice.EdgeScan.Pair line 273
  41. def OAI.MeanPayoff.TreeDevice.EdgeScan.maxScan line 275
  42. def OAI.MeanPayoff.TreeDevice.EdgeScan.minScan line 278
  43. def OAI.MeanPayoff.TreeDevice.EdgeScan.maxDevice line 281
  44. def OAI.MeanPayoff.TreeDevice.EdgeScan.minDevice line 285
  45. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.high_mem line 289
  46. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.low_mem line 293
  47. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.fold_mem line 297
  48. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.high_bounds line 309
  49. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.low_bounds line 323
  50. def OAI.MeanPayoff.TreeDevice.EdgeScan.Represents line 337
  51. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.maxScan_exact line 343
  52. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.minScan_exact line 361
  53. theorem OAI.MeanPayoff.TreeDevice.EdgeScan.operator_exact line 379