OAI/Probability/Contingency/StackSequence.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

Stack Sequence.

  1. def OAI.Contingency.BitModel.StackCode.Sequence.relabel line 15
  2. def OAI.Contingency.BitModel.StackCode.Sequence.next line 24
  3. theorem OAI.Contingency.BitModel.StackCode.Sequence.branch_map line 28
  4. theorem OAI.Contingency.BitModel.StackCode.Sequence.effect_jump line 34
  5. theorem OAI.Contingency.BitModel.StackCode.Sequence.effect_halt line 39
  6. def OAI.Contingency.BitModel.StackCode.Sequence.rightProgram line 46
  7. def OAI.Contingency.BitModel.StackCode.Sequence.program line 48
  8. def OAI.Contingency.BitModel.StackCode.Sequence.left line 54
  9. def OAI.Contingency.BitModel.StackCode.Sequence.right line 57
  10. theorem OAI.Contingency.BitModel.StackCode.Sequence.step_left line 60
  11. theorem OAI.Contingency.BitModel.StackCode.Sequence.step_right line 69
  12. def OAI.Contingency.BitModel.StackCode.Sequence.FirstHalt line 83
  13. theorem OAI.Contingency.BitModel.StackCode.Sequence.firstHalt_result line 87
  14. theorem OAI.Contingency.BitModel.StackCode.Sequence.fold_left line 93
  15. theorem OAI.Contingency.BitModel.StackCode.Sequence.fold_right line 103
  16. theorem OAI.Contingency.BitModel.StackCode.Sequence.link_run line 115
  17. theorem OAI.Contingency.BitModel.StackCode.Sequence.halted_fold line 137
  18. theorem OAI.Contingency.BitModel.StackCode.Sequence.first_prefix line 147
  19. def OAI.Contingency.BitModel.StackCode.Sequence.Deterministic line 160
  20. theorem OAI.Contingency.BitModel.StackCode.Sequence.deterministic_fold line 162
  21. theorem OAI.Contingency.BitModel.StackCode.Sequence.deterministic_first line 176
  22. theorem OAI.Contingency.BitModel.StackCode.Sequence.deterministic_first_time line 190
  23. theorem OAI.Contingency.BitModel.StackCode.Sequence.tape_link line 208
  24. def OAI.Contingency.BitModel.StackCode.Registers.op line 236
  25. def OAI.Contingency.BitModel.StackCode.Registers.program line 245
  26. def OAI.Contingency.BitModel.StackCode.Registers.MemoryRel line 248
  27. theorem OAI.Contingency.BitModel.StackCode.Registers.push_rel line 252
  28. theorem OAI.Contingency.BitModel.StackCode.Registers.pop_rel line 259
  29. theorem OAI.Contingency.BitModel.StackCode.Registers.read_rel line 266
  30. theorem OAI.Contingency.BitModel.StackCode.Registers.effect_rel line 271
  31. def OAI.Contingency.BitModel.StackCode.Registers.ConfigRel line 284
  32. theorem OAI.Contingency.BitModel.StackCode.Registers.step_rel line 288
  33. theorem OAI.Contingency.BitModel.StackCode.Registers.fold_rel line 300
  34. theorem OAI.Contingency.BitModel.StackCode.Registers.effect_frame line 308
  35. theorem OAI.Contingency.BitModel.StackCode.Registers.step_frame line 312
  36. theorem OAI.Contingency.BitModel.StackCode.Registers.fold_frame line 320
  37. theorem OAI.Contingency.BitModel.StackCode.Registers.tape_refinement line 329
  38. def OAI.Contingency.BitModel.StackCode.Transfer.code line 354
  39. def OAI.Contingency.BitModel.StackCode.Transfer.program line 360
  40. def OAI.Contingency.BitModel.StackCode.Transfer.config line 361
  41. def OAI.Contingency.BitModel.StackCode.Transfer.exec line 362
  42. theorem OAI.Contingency.BitModel.StackCode.Transfer.exec_add line 365
  43. def OAI.Contingency.BitModel.StackCode.Transfer.memory line 369
  44. theorem OAI.Contingency.BitModel.StackCode.Transfer.two_steps line 373
  45. theorem OAI.Contingency.BitModel.StackCode.Transfer.empty_run line 377
  46. theorem OAI.Contingency.BitModel.StackCode.Transfer.run line 381
  47. theorem OAI.Contingency.BitModel.StackCode.Transfer.memory_fields line 391
  48. theorem OAI.Contingency.BitModel.StackCode.Transfer.deterministic line 411
  49. theorem OAI.Contingency.BitModel.StackCode.Transfer.tape line 422
  50. def OAI.Contingency.BitModel.StackCode.NoCoin line 441
  51. theorem OAI.Contingency.BitModel.StackCode.noCoin_effect line 445
  52. theorem OAI.Contingency.BitModel.StackCode.noCoin_deterministic line 450
  53. theorem OAI.Contingency.BitModel.StackCode.noCoin_registers line 460
  54. theorem OAI.Contingency.BitModel.StackCode.noCoin_relabel line 464
  55. theorem OAI.Contingency.BitModel.StackCode.noCoin_sequence line 468
  56. inductive OAI.Contingency.BitModel.StackCode.ParseNat.Q line 491
  57. def OAI.Contingency.BitModel.StackCode.ParseNat.label line 494
  58. def OAI.Contingency.BitModel.StackCode.ParseNat.code line 496
  59. def OAI.Contingency.BitModel.StackCode.ParseNat.program line 506
  60. def OAI.Contingency.BitModel.StackCode.ParseNat.config line 507
  61. def OAI.Contingency.BitModel.StackCode.ParseNat.exec line 508
  62. theorem OAI.Contingency.BitModel.StackCode.ParseNat.exec_add line 511
  63. theorem OAI.Contingency.BitModel.StackCode.ParseNat.exec_zero line 514
  64. theorem OAI.Contingency.BitModel.StackCode.ParseNat.exec_one line 515
  65. theorem OAI.Contingency.BitModel.StackCode.ParseNat.one_step line 517
  66. theorem OAI.Contingency.BitModel.StackCode.ParseNat.prefix_zero line 521
  67. theorem OAI.Contingency.BitModel.StackCode.ParseNat.prefix_one line 527
  68. def OAI.Contingency.BitModel.StackCode.ParseNat.prefixMemory line 536
  69. theorem OAI.Contingency.BitModel.StackCode.ParseNat.prefix_run line 540
  70. theorem OAI.Contingency.BitModel.StackCode.ParseNat.prefixMemory_fields line 551
  71. def OAI.Contingency.BitModel.StackCode.ParseNat.digitMemory line 567
  72. theorem OAI.Contingency.BitModel.StackCode.ParseNat.digit_run line 569
  73. def OAI.Contingency.BitModel.StackCode.ParseNat.dataMemory line 582
  74. theorem OAI.Contingency.BitModel.StackCode.ParseNat.data_run line 586
  75. theorem OAI.Contingency.BitModel.StackCode.ParseNat.dataMemory_fields line 598