IntegerDraw.lean`

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

Integer Draw.

inductive OAI.Contingency.BitModel.StackCode.IntegerDraw.Q line 16
def OAI.Contingency.BitModel.StackCode.IntegerDraw.label line 34
def OAI.Contingency.BitModel.StackCode.IntegerDraw.code line 36
def OAI.Contingency.BitModel.StackCode.IntegerDraw.program line 53
def OAI.Contingency.BitModel.StackCode.IntegerDraw.config line 55
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.one_step line 57
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.four_steps line 62
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pass line 70
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.decision line 84
structure OAI.Contingency.BitModel.StackCode.IntegerDraw.Pair line 90
def OAI.Contingency.BitModel.StackCode.IntegerDraw.pairBits line 95
def OAI.Contingency.BitModel.StackCode.IntegerDraw.moveMemory line 97
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.move_from line 99
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.move_to line 102
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.move_other line 105
def OAI.Contingency.BitModel.StackCode.IntegerDraw.moveWord line 108
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.moveWord_stacks line 111
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.restore_two line 126
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.restore_pass line 134
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.restore_finish line 145
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reverse_two line 151
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reverse_pass line 159
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reverse_finish line 170
def OAI.Contingency.BitModel.StackCode.IntegerDraw.emitMemory line 176
def OAI.Contingency.BitModel.StackCode.IntegerDraw.emitWord line 179
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.emit_two line 182
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.emit_pass line 190
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.emitWord_stacks line 201
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.emit_finish line 211
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.push_input line 228
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pop_input line 229
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.push_output line 230
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pop_output line 231
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pop_stack line 232
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pop_other line 233
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.moveWord_output line 234
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.wordMemory_output line 239
def OAI.Contingency.BitModel.StackCode.IntegerDraw.loadMemory line 245
def OAI.Contingency.BitModel.StackCode.IntegerDraw.loadWord line 247
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.load_two line 249
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.load_pass line 256
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.loadWord_stacks line 267
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.load_finish line 282
def OAI.Contingency.BitModel.StackCode.IntegerDraw.clearWord line 288
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.discard_one line 290
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.discard_pass line 295
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.clearWord_stacks line 307
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.discard_finish line 320
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pairBits_length line 326
def OAI.Contingency.BitModel.StackCode.IntegerDraw.successBits line 332
def OAI.Contingency.BitModel.StackCode.IntegerDraw.successMemory line 335
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.success_run line 338
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.success_output line 361
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.success_length line 375
def OAI.Contingency.BitModel.StackCode.IntegerDraw.rejectBits line 398
def OAI.Contingency.BitModel.StackCode.IntegerDraw.rejectMemory line 401
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reject_run line 404
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reject_stacks line 426
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.reject_length line 443
def OAI.Contingency.BitModel.StackCode.IntegerDraw.prepareBits line 451
def OAI.Contingency.BitModel.StackCode.IntegerDraw.prepareMemory line 454
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.prepare_run line 457
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.prepare_stacks line 473
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.prepare_length line 488
def OAI.Contingency.BitModel.StackCode.IntegerDraw.digitCoord line 510
def OAI.Contingency.BitModel.StackCode.IntegerDraw.digitNoise line 512
def OAI.Contingency.BitModel.StackCode.IntegerDraw.blockEquiv line 514
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.block_count line 529
def OAI.Contingency.BitModel.StackCode.IntegerDraw.digits line 543
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.digits_length line 547
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.digits_bound line 549
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.digits_coin line 551
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.digits_bits line 554
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.pass_uniform line 565
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.candidate_count line 573
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.bounded_words line 578
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.accepted_count line 589
theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.accepted_probability line 597