OAI/Computability/RandomMean/DispatchBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobLabel line 9
2. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobLabel.code line 11
3. inductive OAI.MeanPayoff.TreeDevice.Certified.RawControl.FrameLabel line 22
4. def OAI.MeanPayoff.TreeDevice.Certified.RawControl.FrameLabel.code line 24
5. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobLabel.small line 47
6. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.FrameLabel.small line 126
7. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.JobLabel.mass line 249
8. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.FrameLabel.mass line 258
9. theorem OAI.MeanPayoff.TreeDevice.Certified.Code.select_spec line 280
10. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.jobs_spec line 292
11. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.frames_spec line 307
12. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.caller_mass line 334
13. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch_small line 337
14. theorem OAI.MeanPayoff.TreeDevice.Certified.RawControl.dispatch_mass line 352