OAI/Computability/RandomMean/ControlCorrectness.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawControl.VecsRep line 9
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.VecsRep.map line 12
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.VecsRep.getD line 18
  4. structure OAI.MeanPayoff.TreeDevice.Certified.RawControl.EnvRep line 27
  5. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobPackRep line 34
  6. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.FramePackRep line 44
  7. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.ValueRep line 63
  8. inductive OAI.MeanPayoff.TreeDevice.Certified.RawControl.KontRep line 71
  9. inductive OAI.MeanPayoff.TreeDevice.Certified.RawControl.StateRep line 76
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.smallWidth_eq line 94
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.basic_rep line 102
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.narrow_rep line 110
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.wide_rep line 118
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.delta_eq line 124
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.capWidth_eq line 130
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.centerAt_rep line 136
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastPositive_rep line 143
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.lastNegative_rep line 153
  19. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.jobCode line 172
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch_call line 178
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.sampled_call_rep line 183
  22. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.frameCode line 307
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch_return line 319
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.sampled_resume_rep line 324
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.sampled_dispatch_rep line 437