OAI/Computability/MeanPayoff/ArithmeticDevices.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Forest.atom line 9
  2. def OAI.MeanPayoff.TreeDevice.Forest.literal line 21
  3. def OAI.MeanPayoff.TreeDevice.constant line 32
  4. def OAI.MeanPayoff.TreeDevice.branch line 36
  5. def OAI.MeanPayoff.TreeDevice.Bits.notDevice line 43
  6. abbrev OAI.MeanPayoff.TreeDevice.Head.flow line 51
  7. abbrev OAI.MeanPayoff.TreeDevice.Head.program line 58
  8. def OAI.MeanPayoff.TreeDevice.Head.limit line 60
  9. theorem OAI.MeanPayoff.TreeDevice.Head.runs line 64
  10. def OAI.MeanPayoff.TreeDevice.Head.device line 97
  11. abbrev OAI.MeanPayoff.TreeDevice.Median.Count line 107
  12. abbrev OAI.MeanPayoff.TreeDevice.Median.State line 108
  13. def OAI.MeanPayoff.TreeDevice.Median.unitData line 110
  14. def OAI.MeanPayoff.TreeDevice.Median.stateData line 111
  15. def OAI.MeanPayoff.TreeDevice.Median.halfStep line 113
  16. def OAI.MeanPayoff.TreeDevice.Median.incrementDevice line 115
  17. def OAI.MeanPayoff.TreeDevice.Median.halfStepDevice line 120
  18. def OAI.MeanPayoff.TreeDevice.Median.count line 126
  19. def OAI.MeanPayoff.TreeDevice.Median.countDevice line 129
  20. theorem OAI.MeanPayoff.TreeDevice.Median.halfStep_measure line 135
  21. theorem OAI.MeanPayoff.TreeDevice.Median.count_measure line 140
  22. theorem OAI.MeanPayoff.TreeDevice.Median.count_length line 150
  23. theorem OAI.MeanPayoff.TreeDevice.Median.repeatTail line 159
  24. def OAI.MeanPayoff.TreeDevice.Median.dropDevice line 168
  25. def OAI.MeanPayoff.TreeDevice.Median.zeroWord line 175
  26. def OAI.MeanPayoff.TreeDevice.Median.median line 177
  27. def OAI.MeanPayoff.TreeDevice.Median.device line 180
  28. theorem OAI.MeanPayoff.TreeDevice.Median.val_headD line 188
  29. theorem OAI.MeanPayoff.TreeDevice.Median.zeroWord_val line 192
  30. theorem OAI.MeanPayoff.TreeDevice.Median.value_exact line 194
  31. def OAI.MeanPayoff.TreeDevice.Median.vectorDevice line 209
  32. theorem OAI.MeanPayoff.TreeDevice.Median.coordinate_exact line 212
  33. def OAI.MeanPayoff.TreeDevice.LinearCost line 224
  34. theorem OAI.MeanPayoff.TreeDevice.LinearCost.identity line 229
  35. theorem OAI.MeanPayoff.TreeDevice.LinearCost.compose line 235
  36. theorem OAI.MeanPayoff.TreeDevice.LinearCost.dup line 250
  37. theorem OAI.MeanPayoff.TreeDevice.LinearCost.pairMap line 256
  38. theorem OAI.MeanPayoff.TreeDevice.LinearCost.fanout line 274
  39. theorem OAI.MeanPayoff.TreeDevice.LinearCost.first line 279
  40. theorem OAI.MeanPayoff.TreeDevice.LinearCost.second line 286
  41. theorem OAI.MeanPayoff.TreeDevice.LinearCost.select line 293
  42. theorem OAI.MeanPayoff.TreeDevice.LinearCost.compare line 302
  43. theorem OAI.MeanPayoff.TreeDevice.LinearCost.add line 312
  44. theorem OAI.MeanPayoff.TreeDevice.LinearCost.min line 325
  45. theorem OAI.MeanPayoff.TreeDevice.LinearCost.max line 328