OAI/Probability/Contingency/StackCompiler.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

Stack Compiler.

  1. inductive OAI.Contingency.BitModel.StackCode.Op line 13
  2. structure OAI.Contingency.BitModel.StackCode.Program line 22
  3. structure OAI.Contingency.BitModel.StackCode.Memory line 30
  4. structure OAI.Contingency.BitModel.StackCode.Config line 37
  5. def OAI.Contingency.BitModel.StackCode.branch line 41
  6. def OAI.Contingency.BitModel.StackCode.stackTape line 46
  7. def OAI.Contingency.BitModel.StackCode.inputTape line 49
  8. theorem OAI.Contingency.BitModel.StackCode.tape_keep line 53
  9. theorem OAI.Contingency.BitModel.StackCode.stack_push line 55
  10. theorem OAI.Contingency.BitModel.StackCode.stack_pop_empty line 59
  11. theorem OAI.Contingency.BitModel.StackCode.stack_pop_cons line 63
  12. theorem OAI.Contingency.BitModel.StackCode.stack_pop_head line 67
  13. theorem OAI.Contingency.BitModel.StackCode.input_read line 70
  14. theorem OAI.Contingency.BitModel.StackCode.inputTape_head line 76
  15. def OAI.Contingency.BitModel.StackCode.Memory.tapes line 79
  16. theorem OAI.Contingency.BitModel.StackCode.tapes_work line 82
  17. theorem OAI.Contingency.BitModel.StackCode.tapes_input line 85
  18. def OAI.Contingency.BitModel.StackCode.Memory.push line 88
  19. def OAI.Contingency.BitModel.StackCode.Memory.pop line 92
  20. def OAI.Contingency.BitModel.StackCode.Memory.read line 96
  21. def OAI.Contingency.BitModel.StackCode.effect line 99
  22. def OAI.Contingency.BitModel.StackCode.step line 109
  23. def OAI.Contingency.BitModel.StackCode.first line 114
  24. def OAI.Contingency.BitModel.StackCode.second line 115
  25. def OAI.Contingency.BitModel.StackCode.preserved line 117
  26. def OAI.Contingency.BitModel.StackCode.active line 121
  27. def OAI.Contingency.BitModel.StackCode.prepare line 125
  28. def OAI.Contingency.BitModel.StackCode.execute line 131
  29. def OAI.Contingency.BitModel.StackCode.compile line 144
  30. def OAI.Contingency.BitModel.StackCode.encode line 153
  31. theorem OAI.Contingency.BitModel.StackCode.compile_first line 156
  32. theorem OAI.Contingency.BitModel.StackCode.compile_second line 160
  33. theorem OAI.Contingency.BitModel.StackCode.move_preserved line 164
  34. theorem OAI.Contingency.BitModel.StackCode.move_active line 167
  35. theorem OAI.Contingency.BitModel.StackCode.tapes_push line 174
  36. theorem OAI.Contingency.BitModel.StackCode.tapes_pop line 184
  37. theorem OAI.Contingency.BitModel.StackCode.tapes_read line 196
  38. theorem OAI.Contingency.BitModel.StackCode.two_steps line 205
  39. def OAI.Contingency.BitModel.StackCode.initial line 255
  40. def OAI.Contingency.BitModel.StackCode.run line 258
  41. theorem OAI.Contingency.BitModel.StackCode.initial_eq line 261
  42. theorem OAI.Contingency.BitModel.StackCode.fold_pairs line 272
  43. theorem OAI.Contingency.BitModel.StackCode.coins_as_pairs line 281
  44. theorem OAI.Contingency.BitModel.StackCode.run_eq line 291
  45. def OAI.Contingency.BitModel.StackCode.coinPairs line 301
  46. theorem OAI.Contingency.BitModel.StackCode.count_second line 314
  47. def OAI.Contingency.BitModel.StackCode.mass line 323
  48. def OAI.Contingency.BitModel.StackCode.tail line 327
  49. theorem OAI.Contingency.BitModel.StackCode.encode_halt line 330
  50. theorem OAI.Contingency.BitModel.StackCode.encode_output line 333
  51. theorem OAI.Contingency.BitModel.StackCode.mass_compile line 336
  52. theorem OAI.Contingency.BitModel.StackCode.tail_compile line 348
  53. inductive OAI.Contingency.BitModel.StackCode.BinaryTrial.Cmp line 370
  54. instance OAI.Contingency.BitModel.StackCode.BinaryTrial.(instance at line 373) line 373
  55. def OAI.Contingency.BitModel.StackCode.BinaryTrial.advance line 377
  56. def OAI.Contingency.BitModel.StackCode.BinaryTrial.accept line 383
  57. inductive OAI.Contingency.BitModel.StackCode.BinaryTrial.Q line 387
  58. def OAI.Contingency.BitModel.StackCode.BinaryTrial.label line 396
  59. def OAI.Contingency.BitModel.StackCode.BinaryTrial.code line 398
  60. def OAI.Contingency.BitModel.StackCode.BinaryTrial.program line 406
  61. def OAI.Contingency.BitModel.StackCode.BinaryTrial.config line 409
  62. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.program_code line 411
  63. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.one_step line 415
  64. def OAI.Contingency.BitModel.StackCode.BinaryTrial.digitMemory line 420
  65. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.digit_stack0 line 422
  66. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.digit_stack1 line 424
  67. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.digit_stack2 line 426
  68. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.digit_stack3 line 428
  69. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.four_steps line 431
  70. structure OAI.Contingency.BitModel.StackCode.BinaryTrial.Digit line 439
  71. def OAI.Contingency.BitModel.StackCode.BinaryTrial.bits line 446
  72. def OAI.Contingency.BitModel.StackCode.BinaryTrial.wordMemory line 448
  73. def OAI.Contingency.BitModel.StackCode.BinaryTrial.wordCmp line 451
  74. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.pass line 454
  75. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.pass_stacks line 468
  76. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.pass_length line 481
  77. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.finish line 486
  78. def OAI.Contingency.BitModel.StackCode.BinaryTrial.cmpNat line 501
  79. def OAI.Contingency.BitModel.StackCode.BinaryTrial.beValue line 503
  80. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.advance_cmpNat line 505
  81. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.cmp_fold line 510
  82. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.comparison_correct line 521
  83. def OAI.Contingency.BitModel.StackCode.BinaryTrial.wordValue line 529
  84. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.wordValue_succ line 531
  85. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.wordValue_lt line 537
  86. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.wordValue_injective line 545
  87. def OAI.Contingency.BitModel.StackCode.BinaryTrial.wordFin line 560
  88. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.wordFin_bijective line 562
  89. def OAI.Contingency.BitModel.StackCode.BinaryTrial.wordEquiv line 569
  90. theorem OAI.Contingency.BitModel.StackCode.BinaryTrial.word_count line 574