OAI/Computability/MeanPayoff/Packets.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MeanPayoff.WorkStack.heads line 9
  2. def OAI.MeanPayoff.WorkStack.canonical line 12
  3. theorem OAI.MeanPayoff.WorkStack.heads_update line 15
  4. theorem OAI.MeanPayoff.WorkStack.double_step_canonical line 22
  5. theorem OAI.MeanPayoff.WorkStack.canonical_initial line 55
  6. theorem OAI.MeanPayoff.WorkStack.simulate_canonical line 63
  7. def OAI.MeanPayoff.OutputFinish.machine line 79
  8. def OAI.MeanPayoff.OutputFinish.state line 86
  9. def OAI.MeanPayoff.OutputFinish.stopped line 88
  10. theorem OAI.MeanPayoff.OutputFinish.step_cons line 91
  11. theorem OAI.MeanPayoff.OutputFinish.step_nil line 104
  12. theorem OAI.MeanPayoff.OutputFinish.copies line 108
  13. theorem OAI.MeanPayoff.MachineRun.run_after_halt line 121
  14. def OAI.MeanPayoff.WorkStack.compiled line 131
  15. theorem OAI.MeanPayoff.WorkStack.restart_canonical line 134
  16. theorem OAI.MeanPayoff.WorkStack.compiled_run line 146
  17. def OAI.MeanPayoff.PrefixCount.front line 180
  18. def OAI.MeanPayoff.PrefixCount.back line 182
  19. def OAI.MeanPayoff.PrefixCount.concat line 184
  20. theorem OAI.MeanPayoff.PrefixCount.front_concat line 187
  21. theorem OAI.MeanPayoff.PrefixCount.back_concat line 189
  22. def OAI.MeanPayoff.PrefixCount.equiv line 192
  23. theorem OAI.MeanPayoff.PrefixCount.successful_count line 208
  24. theorem OAI.MeanPayoff.PrefixCount.success_transfer line 219
  25. theorem OAI.MeanPayoff.PrefixCount.two_phase_success line 227
  26. theorem OAI.MeanPayoff.WorkStack.run_congr line 236
  27. theorem OAI.MeanPayoff.WorkStack.prefix_even_run line 244
  28. def OAI.MeanPayoff.WorkStack.Ready line 260
  29. def OAI.MeanPayoff.WorkStack.output line 264
  30. theorem OAI.MeanPayoff.WorkStack.compiled_packet line 267
  31. theorem OAI.MeanPayoff.WorkStack.compiled_success line 287
  32. theorem OAI.MeanPayoff.correctList_packet line 307