OAI/Computability/MeanPayoff/Stack.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.MeanPayoff.SourceControl.Result line 10
  2. abbrev OAI.MeanPayoff.SourceControl.Result.Value line 17
  3. inductive OAI.MeanPayoff.SourceControl.Job line 24
  4. inductive OAI.MeanPayoff.SourceControl.Frame line 41
  5. inductive OAI.MeanPayoff.SourceControl.Kont line 84
  6. inductive OAI.MeanPayoff.SourceControl.State line 88
  7. def OAI.MeanPayoff.SourceControl.resume line 92
  8. def OAI.MeanPayoff.SourceControl.step line 141
  9. def OAI.MeanPayoff.SourceControl.Job.tag line 172
  10. def OAI.MeanPayoff.SourceControl.Frame.tag line 177
  11. theorem OAI.MeanPayoff.Counted.ext line 187
  12. theorem OAI.MeanPayoff.Counted.pure_bind line 189
  13. theorem OAI.MeanPayoff.Counted.bind_pure line 191
  14. theorem OAI.MeanPayoff.Counted.map_pure line 193
  15. theorem OAI.MeanPayoff.Counted.map_bind line 195
  16. theorem OAI.MeanPayoff.Counted.bind_map line 198
  17. theorem OAI.MeanPayoff.Counted.bind_assoc line 201
  18. theorem OAI.MeanPayoff.Counted.map_map line 204
  19. theorem OAI.MeanPayoff.Counted.bind_pure_eq_map line 207
  20. theorem OAI.MeanPayoff.Counted.charge_bind line 210
  21. abbrev OAI.MeanPayoff.SourceControl.wholeLower line 215
  22. def OAI.MeanPayoff.SourceControl.Job.denote line 218
  23. def OAI.MeanPayoff.SourceControl.Frame.denote line 233
  24. def OAI.MeanPayoff.SourceControl.Kont.denote line 283
  25. def OAI.MeanPayoff.SourceControl.State.denote line 287
  26. theorem OAI.MeanPayoff.SourceControl.resume_denote line 291
  27. theorem OAI.MeanPayoff.SourceControl.solve_notSmall line 316
  28. theorem OAI.MeanPayoff.SourceControl.step_denote line 321