OAI/Probability/Contingency/IntegerDrawMachine.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Integer Draw Machine.

  1. structure OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame line 15
  2. def OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.coins line 27
  3. def OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.rejected line 30
  4. def OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.next line 33
  5. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.run line 36
  6. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.invariant line 43
  7. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.RejectFrame.length line 51
  8. def OAI.Contingency.BitModel.StackCode.IntegerDraw.rejectedMemory line 57
  9. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rejected_run line 60
  10. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rejected_invariant line 75
  11. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rejected_length line 86
  12. structure OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame line 94
  13. def OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.coins line 107
  14. def OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.accepted line 110
  15. def OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.next line 113
  16. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.run line 116
  17. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.output line 122
  18. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.AcceptFrame.length line 127
  19. structure OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame line 132
  20. def OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame.coins line 140
  21. def OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame.prepared line 143
  22. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame.run line 146
  23. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame.invariant line 153
  24. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.PrepareFrame.length line 158
  25. def OAI.Contingency.BitModel.StackCode.IntegerDraw.executionBits line 164
  26. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.execution_run line 167
  27. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.execution_length line 181
  28. def OAI.Contingency.BitModel.StackCode.IntegerDraw.machine line 188
  29. def OAI.Contingency.BitModel.StackCode.IntegerDraw.pairedBits line 190
  30. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.compiled_execution line 192
  31. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pairedBits_length line 205
  32. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.compiled_length line 212
  33. def OAI.Contingency.BitModel.StackCode.IntegerDraw.trace line 232
  34. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.trace_length line 234
  35. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.trace_append line 236
  36. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.trace_one line 242
  37. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.trace_two line 243
  38. def OAI.Contingency.BitModel.StackCode.IntegerDraw.makePairs line 245
  39. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.makePairs_bits line 248
  40. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.makePairs_length line 251
  41. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.makePairs_coins line 254
  42. def OAI.Contingency.BitModel.StackCode.IntegerDraw.streamDigits line 260
  43. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamDigits_bound line 263
  44. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamDigits_length line 265
  45. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamDigits_coins line 268
  46. def OAI.Contingency.BitModel.StackCode.IntegerDraw.streamPrepare line 272
  47. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamPrepare_coins line 280
  48. def OAI.Contingency.BitModel.StackCode.IntegerDraw.streamReject line 296
  49. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamReject_coins line 308
  50. def OAI.Contingency.BitModel.StackCode.IntegerDraw.streamAccept line 319
  51. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.streamAccept_coins line 332
  52. def OAI.Contingency.BitModel.StackCode.IntegerDraw.prepTime line 356
  53. def OAI.Contingency.BitModel.StackCode.IntegerDraw.retryTime line 357
  54. def OAI.Contingency.BitModel.StackCode.IntegerDraw.successTime line 358
  55. def OAI.Contingency.BitModel.StackCode.IntegerDraw.startTime line 359
  56. def OAI.Contingency.BitModel.StackCode.IntegerDraw.candidate line 361
  57. def OAI.Contingency.BitModel.StackCode.IntegerDraw.accepted line 364
  58. def OAI.Contingency.BitModel.StackCode.IntegerDraw.retries line 366
  59. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.retries_length line 369
  60. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.retries_coins line 371
  61. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.first_accept line 382
  62. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.halted_fold line 405
  63. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.first_accept_later line 411
  64. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.accepts_halt line 430
  65. def OAI.Contingency.BitModel.CoordinateLaw.indexEquiv line 461
  66. theorem OAI.Contingency.BitModel.CoordinateLaw.indexEquiv_left line 466
  67. def OAI.Contingency.BitModel.CoordinateLaw.split line 468
  68. theorem OAI.Contingency.BitModel.CoordinateLaw.split_left line 473
  69. theorem OAI.Contingency.BitModel.CoordinateLaw.count_restrict line 476
  70. theorem OAI.Contingency.BitModel.CoordinateLaw.cardinal_split line 488
  71. theorem OAI.Contingency.BitModel.CoordinateLaw.probability_restrict line 493
  72. theorem OAI.Contingency.BitModel.CoordinateLaw.count_all line 501
  73. theorem OAI.Contingency.BitModel.StackCode.prepare_observe line 520
  74. theorem OAI.Contingency.BitModel.StackCode.prepare_output line 532
  75. theorem OAI.Contingency.BitModel.StackCode.machine_run_succ line 544
  76. def OAI.Contingency.BitModel.StackCode.coinLast line 550
  77. theorem OAI.Contingency.BitModel.StackCode.count_last line 558
  78. theorem OAI.Contingency.BitModel.StackCode.mass_compile_odd line 569
  79. theorem OAI.Contingency.BitModel.StackCode.tail_compile_odd line 583
  80. theorem OAI.Contingency.BitModel.StackCode.mass_compile_all line 595
  81. theorem OAI.Contingency.BitModel.StackCode.tail_compile_all line 607
  82. theorem OAI.Contingency.BitModel.StackCode.half_tendsto line 619
  83. theorem OAI.Contingency.BitModel.StackCode.mass_limit_compile line 625
  84. theorem OAI.Contingency.BitModel.StackCode.tail_limit_compile line 630
  85. theorem OAI.Contingency.BitModel.StackCode.tail_summable_compile line 635
  86. theorem OAI.Contingency.BitModel.StackCode.expected_compile line 643