OAI/Computability/MeanPayoff/Realizer.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.DetPost.boolean line 7
  2. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPost.boolean_poly line 11
  3. def OAI.MeanPayoff.TreeDevice.Certified.DetPost.digits line 14
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.DetPost.digits_eval line 20
  5. def OAI.MeanPayoff.Box5.place line 27
  6. theorem OAI.MeanPayoff.Box5.injective line 28
  7. theorem OAI.MeanPayoff.Box5.installs line 29
  8. def OAI.MeanPayoff.Box5.program line 37
  9. theorem OAI.MeanPayoff.Box5.quiet line 38
  10. theorem OAI.MeanPayoff.Box5.runs line 39
  11. def OAI.MeanPayoff.Emit.program line 57
  12. def OAI.MeanPayoff.Emit.cfg line 67
  13. def OAI.MeanPayoff.Emit.cost line 68
  14. theorem OAI.MeanPayoff.Emit.quiet line 69
  15. theorem OAI.MeanPayoff.Emit.nil_run line 70
  16. theorem OAI.MeanPayoff.Emit.one line 76
  17. theorem OAI.MeanPayoff.Emit.runs line 82
  18. theorem OAI.MeanPayoff.Emit.bound line 91
  19. def OAI.MeanPayoff.RegisterBits.Sequence5.flow line 106
  20. def OAI.MeanPayoff.RegisterBits.Sequence5.program line 112
  21. theorem OAI.MeanPayoff.RegisterBits.Sequence5.quiet line 113
  22. theorem OAI.MeanPayoff.RegisterBits.Sequence5.finish_output line 115
  23. theorem OAI.MeanPayoff.RegisterBits.Sequence5.runs line 124
  24. def OAI.MeanPayoff.DetRealizer.preTail line 140
  25. def OAI.MeanPayoff.DetRealizer.pre line 141
  26. def OAI.MeanPayoff.DetRealizer.preCost line 142
  27. theorem OAI.MeanPayoff.DetRealizer.pre_quiet line 144
  28. theorem OAI.MeanPayoff.DetRealizer.pre_runs line 146
  29. def OAI.MeanPayoff.DetRealizer.post line 158
  30. def OAI.MeanPayoff.DetRealizer.postCost line 159
  31. theorem OAI.MeanPayoff.DetRealizer.post_quiet line 160
  32. theorem OAI.MeanPayoff.DetRealizer.post_runs line 161
  33. theorem OAI.MeanPayoff.DetRealizer.digits_length line 169
  34. theorem OAI.MeanPayoff.DetRealizer.post_polynomial line 173
  35. def OAI.MeanPayoff.DetRealizer.program line 180
  36. def OAI.MeanPayoff.DetRealizer.limit line 181
  37. theorem OAI.MeanPayoff.DetRealizer.program_quiet line 182
  38. theorem OAI.MeanPayoff.DetRealizer.runs line 183
  39. theorem OAI.MeanPayoff.DetRealizer.pre_bound line 191
  40. theorem OAI.MeanPayoff.DetRealizer.post_bound line 197
  41. theorem OAI.MeanPayoff.DetRealizer.limit_bound line 201
  42. theorem OAI.MeanPayoff.DetRealizer.list_size line 206
  43. def OAI.MeanPayoff.DetRealizer.total line 215
  44. theorem OAI.MeanPayoff.DetRealizer.total_formula line 217
  45. theorem OAI.MeanPayoff.DetRealizer.total_bound line 222
  46. theorem OAI.MeanPayoff.DetRealizer.resource_quasi line 230
  47. theorem OAI.MeanPayoff.DetRealizer.polynomial_quasi line 253
  48. theorem OAI.MeanPayoff.DetRealizer.natural_quasi_real line 272
  49. theorem OAI.MeanPayoff.DetRealizer.total_quasi line 288