OAI/Computability/MeanPayoff/FiniteTrees.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MeanPayoff.BinaryStack.advance_initial line 7
  2. def OAI.MeanPayoff.RandomTree.wait line 16
  3. theorem OAI.MeanPayoff.RandomTree.expect_wait line 20
  4. theorem OAI.MeanPayoff.RandomTree.depth_wait line 26
  5. theorem OAI.MeanPayoff.RandomTree.all_wait line 32
  6. theorem OAI.MeanPayoff.RandomTree.consume_wait line 38
  7. def OAI.MeanPayoff.RegisterBits.tree line 48
  8. def OAI.MeanPayoff.RegisterBits.Compile.schedule line 54
  9. theorem OAI.MeanPayoff.RegisterBits.Compile.schedule_expect line 60
  10. theorem OAI.MeanPayoff.RegisterBits.Compile.schedule_all line 66
  11. def OAI.MeanPayoff.RegisterBits.Compile.overhead line 72
  12. theorem OAI.MeanPayoff.RegisterBits.Compile.schedule_depth line 74
  13. theorem OAI.MeanPayoff.RegisterBits.Compile.consume_schedule_step line 95
  14. theorem OAI.MeanPayoff.RegisterBits.Compile.consume_simulation line 104
  15. def OAI.MeanPayoff.RegisterBits.Compile.initializedTree line 124
  16. theorem OAI.MeanPayoff.RegisterBits.Compile.initialized_depth line 128
  17. theorem OAI.MeanPayoff.RegisterBits.Compile.initialized_simulation line 134
  18. theorem OAI.MeanPayoff.BinaryStack.run_after_halt line 152
  19. theorem OAI.MeanPayoff.RegisterBits.Compile.embed_halted line 162
  20. theorem OAI.MeanPayoff.RegisterBits.Compile.initialized_all line 165
  21. theorem OAI.MeanPayoff.RegisterBits.Compile.initialized_expect line 169
  22. def OAI.MeanPayoff.RegisterBits.Compile.bound line 173
  23. theorem OAI.MeanPayoff.RegisterBits.Compile.padded_run line 176
  24. def OAI.MeanPayoff.RegisterBits.Compile.machine line 193
  25. theorem OAI.MeanPayoff.RegisterBits.Compile.machine_packet line 196
  26. theorem OAI.MeanPayoff.RegisterBits.Compile.machine_probability line 216
  27. inductive OAI.MeanPayoff.BinaryData.Data line 258
  28. def OAI.MeanPayoff.BinaryData.encode line 263
  29. theorem OAI.MeanPayoff.BinaryData.encode_nonempty line 267
  30. theorem OAI.MeanPayoff.BinaryData.encode_positive line 268
  31. inductive OAI.MeanPayoff.BinaryData.Take.Label line 274
  32. def OAI.MeanPayoff.BinaryData.Take.equiv line 278
  33. def OAI.MeanPayoff.BinaryData.Take.enc line 279
  34. theorem OAI.MeanPayoff.BinaryData.Take.dec line 280
  35. def OAI.MeanPayoff.BinaryData.Take.program line 282
  36. def OAI.MeanPayoff.BinaryData.Take.cfg line 299
  37. def OAI.MeanPayoff.BinaryData.Take.stopped line 301
  38. theorem OAI.MeanPayoff.BinaryData.Take.config_ext line 304
  39. theorem OAI.MeanPayoff.BinaryData.Take.advance_front line 308
  40. theorem OAI.MeanPayoff.BinaryData.Take.advance_add line 317
  41. theorem OAI.MeanPayoff.BinaryData.Take.start_step line 326
  42. theorem OAI.MeanPayoff.BinaryData.Take.check_step line 333
  43. theorem OAI.MeanPayoff.BinaryData.Take.read_step line 340
  44. theorem OAI.MeanPayoff.BinaryData.Take.put_step line 347
  45. theorem OAI.MeanPayoff.BinaryData.Take.depth_false line 354
  46. theorem OAI.MeanPayoff.BinaryData.Take.depth_true line 361
  47. theorem OAI.MeanPayoff.BinaryData.Take.scan_nil line 368
  48. theorem OAI.MeanPayoff.BinaryData.Take.scan_pair line 373
  49. theorem OAI.MeanPayoff.BinaryData.Take.scan line 378
  50. theorem OAI.MeanPayoff.BinaryData.Take.check_empty line 393
  51. theorem OAI.MeanPayoff.BinaryData.Take.restore_step line 400
  52. theorem OAI.MeanPayoff.BinaryData.Take.restore_put line 407
  53. theorem OAI.MeanPayoff.BinaryData.Take.restore_empty line 414
  54. theorem OAI.MeanPayoff.BinaryData.Take.restore_all line 418
  55. theorem OAI.MeanPayoff.BinaryData.Take.takes line 428