OAI/Computability/DeterministicSum/Structured.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Structured assembly, instruction-exact semantics, initialized-memory frames and loops.

  1. lemma OAI.DeterministicThreeSum.run_add line 10
  2. structure OAI.DeterministicThreeSum.Structured.Data line 20
  3. def OAI.DeterministicThreeSum.Structured.state line 24
  4. def OAI.DeterministicThreeSum.Structured.operand line 26
  5. def OAI.DeterministicThreeSum.Structured.put line 28
  6. inductive OAI.DeterministicThreeSum.Structured.Atom line 31
  7. def OAI.DeterministicThreeSum.Structured.Atom.instruction line 37
  8. def OAI.DeterministicThreeSum.Structured.Atom.eval line 43
  9. def OAI.DeterministicThreeSum.Structured.test line 49
  10. inductive OAI.DeterministicThreeSum.Structured.Command line 52
  11. def OAI.DeterministicThreeSum.Structured.Command.size line 61
  12. def OAI.DeterministicThreeSum.Structured.Command.compile line 68
  13. lemma OAI.DeterministicThreeSum.Structured.Command.length_compile line 79
  14. inductive OAI.DeterministicThreeSum.Structured.Command.Eval line 83
  15. def OAI.DeterministicThreeSum.Structured.Contains line 97
  16. lemma OAI.DeterministicThreeSum.Structured.contains_self line 100
  17. lemma OAI.DeterministicThreeSum.Structured.Contains.head line 101
  18. lemma OAI.DeterministicThreeSum.Structured.Contains.tail line 104
  19. lemma OAI.DeterministicThreeSum.Structured.Contains.left line 108
  20. lemma OAI.DeterministicThreeSum.Structured.Contains.right line 112
  21. lemma OAI.DeterministicThreeSum.Structured.step_atom line 118
  22. lemma OAI.DeterministicThreeSum.Structured.step_jump line 135
  23. lemma OAI.DeterministicThreeSum.Structured.step_branch line 139
  24. lemma OAI.DeterministicThreeSum.run_one_of_step line 149
  25. lemma OAI.DeterministicThreeSum.run_comp line 151
  26. theorem OAI.DeterministicThreeSum.Structured.Command.compile_correct line 157
  27. def OAI.DeterministicThreeSum.Structured.Command.decisionProgram line 201
  28. lemma OAI.DeterministicThreeSum.Structured.Command.decision_compiles line 204
  29. lemma OAI.DeterministicThreeSum.Structured.Data.ext line 240
  30. lemma OAI.DeterministicThreeSum.Structured.operand_register line 243
  31. lemma OAI.DeterministicThreeSum.Structured.operand_literal line 245
  32. lemma OAI.DeterministicThreeSum.Structured.loop_iterations line 248
  33. lemma OAI.DeterministicThreeSum.Structured.eval_increment line 274
  34. def OAI.DeterministicThreeSum.Structured.fillCommand line 282
  35. def OAI.DeterministicThreeSum.Structured.filled line 287
  36. lemma OAI.DeterministicThreeSum.Structured.filled_zero line 291
  37. theorem OAI.DeterministicThreeSum.Structured.fillCommand_correct line 299
  38. def OAI.DeterministicThreeSum.Structured.Atom.writes line 355
  39. def OAI.DeterministicThreeSum.Structured.Command.writes line 359
  40. def OAI.DeterministicThreeSum.Structured.Atom.noStore line 366
  41. def OAI.DeterministicThreeSum.Structured.Command.noStore line 370
  42. lemma OAI.DeterministicThreeSum.Structured.atom_register_frame line 376
  43. lemma OAI.DeterministicThreeSum.Structured.register_frame line 386
  44. lemma OAI.DeterministicThreeSum.Structured.atom_memory_frame line 399
  45. lemma OAI.DeterministicThreeSum.Structured.memory_frame line 407
  46. theorem OAI.DeterministicThreeSum.Structured.bounded_loop line 418
  47. lemma OAI.DeterministicThreeSum.Structured.eval_assign line 442
  48. lemma OAI.DeterministicThreeSum.Structured.eval_load line 445