OAI/Probability/Contingency/ParseNatRuns.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Parse Nat Runs.

  1. theorem OAI.Contingency.BitModel.StackCode.ParseNat.data_done line 14
  2. theorem OAI.Contingency.BitModel.StackCode.ParseNat.restore_empty line 19
  3. theorem OAI.Contingency.BitModel.StackCode.ParseNat.restore_bit line 24
  4. def OAI.Contingency.BitModel.StackCode.ParseNat.restoreMemory line 32
  5. theorem OAI.Contingency.BitModel.StackCode.ParseNat.restore_run line 36
  6. theorem OAI.Contingency.BitModel.StackCode.ParseNat.restoreMemory_fields line 46
  7. theorem OAI.Contingency.BitModel.StackCode.ParseNat.halt line 59
  8. theorem OAI.Contingency.BitModel.StackCode.ParseNat.parse_word line 64
  9. theorem OAI.Contingency.BitModel.StackCode.ParseNat.step_independent line 95
  10. theorem OAI.Contingency.BitModel.StackCode.ParseNat.fold_independent line 105
  11. theorem OAI.Contingency.BitModel.StackCode.ParseNat.parse_nat_tape line 120
  12. def OAI.Contingency.BitModel.StackCode.PrepareMaximum.reg line 150
  13. theorem OAI.Contingency.BitModel.StackCode.PrepareMaximum.reg_injective line 152
  14. abbrev OAI.Contingency.BitModel.StackCode.PrepareMaximum.parser line 157
  15. def OAI.Contingency.BitModel.StackCode.PrepareMaximum.program line 160
  16. theorem OAI.Contingency.BitModel.StackCode.PrepareMaximum.parser_noCoin line 162
  17. theorem OAI.Contingency.BitModel.StackCode.PrepareMaximum.noCoin line 168
  18. theorem OAI.Contingency.BitModel.StackCode.PrepareMaximum.prepare line 175
  19. abbrev OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.callee line 259
  20. def OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.program line 263
  21. def OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.result line 266
  22. theorem OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.prepared_first line 270
  23. theorem OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.refinement line 292
  24. theorem OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.tape_refinement line 321
  25. def OAI.Contingency.BitModel.StackCode.InputCall.op line 352
  26. def OAI.Contingency.BitModel.StackCode.InputCall.program line 361
  27. def OAI.Contingency.BitModel.StackCode.InputCall.MemoryRel line 365
  28. theorem OAI.Contingency.BitModel.StackCode.InputCall.push_work line 369
  29. theorem OAI.Contingency.BitModel.StackCode.InputCall.pop_work line 378
  30. theorem OAI.Contingency.BitModel.StackCode.InputCall.read_input line 387
  31. theorem OAI.Contingency.BitModel.StackCode.InputCall.emit_output line 396
  32. theorem OAI.Contingency.BitModel.StackCode.InputCall.effect_rel line 400
  33. def OAI.Contingency.BitModel.StackCode.InputCall.ConfigRel line 413
  34. theorem OAI.Contingency.BitModel.StackCode.InputCall.step_rel line 416
  35. theorem OAI.Contingency.BitModel.StackCode.InputCall.fold_rel line 427
  36. abbrev OAI.Contingency.BitModel.StackCode.EncodedInteger.callee line 448
  37. def OAI.Contingency.BitModel.StackCode.EncodedInteger.program line 452
  38. def OAI.Contingency.BitModel.StackCode.EncodedInteger.result line 455
  39. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.refinement line 460
  40. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.shifted_laws line 496
  41. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.stack_safe line 523
  42. def OAI.Contingency.BitModel.StackCode.EncodedInteger.machine line 555
  43. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.stack_summable line 557
  44. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.stack_expected line 564
  45. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.stack_uniform line 589
  46. theorem OAI.Contingency.BitModel.StackCode.EncodedInteger.integer_sampler line 604