OAI/Computability/MeanPayoff/Driver.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.Code.select line 12
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.select_eval line 16
  3. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Frame line 29
  4. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetDriver.State line 30
  5. abbrev OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Env line 31
  6. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.zeroInput line 33
  7. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.zeroFrame line 34
  8. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.call line 35
  9. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.ret line 36
  10. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.frame line 37
  11. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.state line 39
  12. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.arena line 40
  13. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.returning line 41
  14. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.input line 42
  15. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.labels line 43
  16. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.stack line 44
  17. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.top line 45
  18. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.rest line 46
  19. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.tag line 47
  20. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.parent line 48
  21. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.kd line 49
  22. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.pivot line 50
  23. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.frameCode line 51
  24. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.callCode line 53
  25. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.retCode line 55
  26. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.pushCode line 57
  27. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.initialPivot line 60
  28. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.enter line 61
  29. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.updated line 66
  30. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.moving line 68
  31. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.again line 69
  32. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.downDone line 72
  33. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.upDone line 75
  34. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.provisionalDone line 78
  35. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.continuationDone line 81
  36. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.resume line 83
  37. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.stop line 86
  38. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step line 87
  39. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.callCode_eval line 90
  40. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.retCode_eval line 92
  41. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.pushCode_eval line 94
  42. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.frameCode_eval line 96
  43. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_call line 99
  44. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_ret_nil line 105
  45. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_down line 108
  46. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_up line 114
  47. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_provisional line 120
  48. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_continuation line 124
  49. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.stop_call line 127
  50. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.stop_ret line 128
  51. structure OAI.MeanPayoff.TreeDevice.Certified.DetDriver.FrameSmall line 138
  52. structure OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Small line 144
  53. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.FrameSmall.mono line 150
  54. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Small.mono line 153
  55. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.zero_small line 156
  56. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.frame_small line 159
  57. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.call_small line 163
  58. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.ret_small line 167
  59. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.call_push_small line 171
  60. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_forward line 182
  61. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_return_push line 185
  62. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_return_large line 188
  63. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.enter_small line 193
  64. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.resume_small line 207
  65. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.step_small line 247
  66. theorem OAI.MeanPayoff.Label.gridPivot_injective line 275
  67. theorem OAI.MeanPayoff.Label.downRun_fixed line 287
  68. theorem OAI.MeanPayoff.Label.downRun_next line 292
  69. theorem OAI.MeanPayoff.Label.upRun_fixed line 297
  70. theorem OAI.MeanPayoff.Label.upRun_next line 302