OAI/Computability/MeanPayoff/DriverExecution.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.advance line 8
  2. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Exec line 9
  3. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Exec.refl line 11
  4. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Exec.one line 12
  5. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Exec.trans line 13
  6. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.down_pass line 20
  7. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.up_pass line 73
  8. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.pair line 132
  9. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.bool line 136
  10. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.list_bound line 137
  11. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.unit_list line 148
  12. theorem OAI.MeanPayoff.TreeDevice.Certified.Size.bool_list line 151
  13. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.Small.size line 157
  14. theorem OAI.MeanPayoff.TreeDevice.Certified.Array.small_of_size line 160
  15. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.small_of_size line 165
  16. theorem OAI.MeanPayoff.TreeDevice.Certified.DetMass.Small.size line 167
  17. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.small_of_size line 180
  18. theorem OAI.MeanPayoff.TreeDevice.Certified.DetRaw.Small.size line 187
  19. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.FrameSmall.size line 202
  20. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.frameSmall_of_size line 211
  21. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.Small.size line 218
  22. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.small_of_size line 230
  23. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.iterate_small line 237
  24. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.tick line 248
  25. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.tick_eval line 249
  26. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.fold_tick line 250
  27. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.tick_prefix line 258
  28. def OAI.MeanPayoff.TreeDevice.Certified.DetDriver.run line 277
  29. theorem OAI.MeanPayoff.TreeDevice.Certified.DetDriver.run_eval line 278