OAI/Computability/MeanPayoff/RawSolutions.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.fst line 14
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.snd line 18
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.mem line 22
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.length line 31
  5. def OAI.MeanPayoff.TreeDevice.Certified.Array.Bounded line 39
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.bounded_size line 41
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.size_bound line 45
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.bounded_zip line 58
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.zip_length line 84
  10. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawBasic.Arena line 92
  11. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawBasic.Env line 93
  12. abbrev OAI.MeanPayoff.TreeDevice.Certified.RawBasic.Acc line 94
  13. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.graph line 96
  14. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.next line 98
  15. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.advance line 100
  16. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.ArenaBounded line 103
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.arenaBounded_size line 106
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.lookup_bound line 116
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.vertex_bound line 127
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.graph_bound line 153
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.clip_bound line 160
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.next_bound line 166
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.next_length line 179
  24. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.fold_layout line 182
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.fold_bound line 195
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.prefix_size line 216
  27. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.loop line 252
  28. def OAI.MeanPayoff.TreeDevice.Certified.RawBasic.solve line 253
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.next_rep line 256
  30. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.loop_rep line 269
  31. theorem OAI.MeanPayoff.TreeDevice.Certified.RawBasic.solve_rep line 282