OAI/Probability/Contingency/BinaryAddition.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Binary Addition.

  1. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.value_append line 16
  2. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.full_output_value line 24
  3. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.add_tape line 31
  4. theorem OAI.Contingency.BitModel.StackCode.BinaryAdd.add_naturals line 62
  5. inductive OAI.Contingency.BitModel.StackCode.WeightedScan.Q line 95
  6. def OAI.Contingency.BitModel.StackCode.WeightedScan.label line 107
  7. def OAI.Contingency.BitModel.StackCode.WeightedScan.code line 109
  8. def OAI.Contingency.BitModel.StackCode.WeightedScan.program line 120
  9. def OAI.Contingency.BitModel.StackCode.WeightedScan.config line 121
  10. def OAI.Contingency.BitModel.StackCode.WeightedScan.exec line 123
  11. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.exec_add line 126
  12. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.exec_zero line 129
  13. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.exec_one line 130
  14. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.one_step line 132
  15. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.first_step line 136
  16. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.second_step line 141
  17. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.third_step line 146
  18. def OAI.Contingency.BitModel.StackCode.WeightedScan.digitMemory line 150
  19. def OAI.Contingency.BitModel.StackCode.WeightedScan.wordMemory line 153
  20. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.three_steps line 157
  21. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.pass line 165
  22. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.wordMemory_stacks line 177
  23. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.end_word line 207
  24. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.advance line 212
  25. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.restore_empty line 216
  26. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.restore_bit line 221
  27. def OAI.Contingency.BitModel.StackCode.WeightedScan.restoreMemory line 231
  28. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.restore_run line 235
  29. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.restoreMemory_stacks line 245
  30. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.selected_empty line 257
  31. def OAI.Contingency.BitModel.StackCode.WeightedScan.emitMemory line 267
  32. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.selected_bit line 270
  33. def OAI.Contingency.BitModel.StackCode.WeightedScan.selectedMemory line 280
  34. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.selected_run line 284
  35. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.selectedMemory_output line 294
  36. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.skip_weight line 306
  37. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.hit_weight line 333
  38. def OAI.Contingency.BitModel.StackCode.WeightedScan.weightTotal line 364
  39. def OAI.Contingency.BitModel.StackCode.WeightedScan.indexedWeights line 366
  40. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.indexed_total line 370
  41. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.scan_run line 378
  42. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.step_independent line 427
  43. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.fold_independent line 437
  44. theorem OAI.Contingency.BitModel.StackCode.WeightedScan.scan_tape line 452
  45. def OAI.Contingency.BitModel.StackCode.Internal.work line 489
  46. def OAI.Contingency.BitModel.StackCode.Internal.input line 491
  47. def OAI.Contingency.BitModel.StackCode.Internal.output line 493
  48. theorem OAI.Contingency.BitModel.StackCode.Internal.work_inj line 495
  49. theorem OAI.Contingency.BitModel.StackCode.Internal.work_ne_input line 496
  50. theorem OAI.Contingency.BitModel.StackCode.Internal.work_ne_output line 497
  51. theorem OAI.Contingency.BitModel.StackCode.Internal.input_ne_output line 498
  52. theorem OAI.Contingency.BitModel.StackCode.Internal.input_ne_work line 499
  53. theorem OAI.Contingency.BitModel.StackCode.Internal.output_ne_work line 500
  54. theorem OAI.Contingency.BitModel.StackCode.Internal.output_ne_input line 501
  55. def OAI.Contingency.BitModel.StackCode.Internal.op line 503
  56. def OAI.Contingency.BitModel.StackCode.Internal.program line 512
  57. def OAI.Contingency.BitModel.StackCode.Internal.MemoryRel line 516
  58. theorem OAI.Contingency.BitModel.StackCode.Internal.push_work line 520
  59. theorem OAI.Contingency.BitModel.StackCode.Internal.pop_work line 529
  60. theorem OAI.Contingency.BitModel.StackCode.Internal.read_input line 538
  61. theorem OAI.Contingency.BitModel.StackCode.Internal.emit_output line 547
  62. theorem OAI.Contingency.BitModel.StackCode.Internal.effect_rel line 556
  63. def OAI.Contingency.BitModel.StackCode.Internal.ConfigRel line 569
  64. theorem OAI.Contingency.BitModel.StackCode.Internal.step_rel line 572
  65. theorem OAI.Contingency.BitModel.StackCode.Internal.fold_rel line 583
  66. def OAI.Contingency.BitModel.StackCode.Internal.loaded line 593
  67. theorem OAI.Contingency.BitModel.StackCode.Internal.loaded_rel line 596
  68. theorem OAI.Contingency.BitModel.StackCode.Internal.loaded_run line 606
  69. theorem OAI.Contingency.BitModel.StackCode.Internal.effect_frame line 621
  70. theorem OAI.Contingency.BitModel.StackCode.Internal.step_frame line 627
  71. theorem OAI.Contingency.BitModel.StackCode.Internal.fold_frame line 636
  72. theorem OAI.Contingency.BitModel.StackCode.Internal.tape_fold line 647
  73. theorem OAI.Contingency.BitModel.StackCode.Internal.loaded_tape line 658