OAI/Computability/Scheduling/RegisterMachine.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ThreeMachine.StackCompiler.Packed line 9
  2. def OAI.ThreeMachine.StackCompiler.Packed.ofProgram line 19
  3. def OAI.ThreeMachine.StackCompiler.Packed.seq line 20
  4. def OAI.ThreeMachine.StackCompiler.Packed.branch line 21
  5. def OAI.ThreeMachine.StackCompiler.Packed.loop line 23
  6. def OAI.ThreeMachine.StackCompiler.Packed.Runs line 26
  7. theorem OAI.ThreeMachine.StackCompiler.Packed.Runs.seq line 28
  8. theorem OAI.ThreeMachine.StackCompiler.Packed.Runs.mono line 32
  9. abbrev OAI.ThreeMachine.StackCompiler.Tree.Registers line 39
  10. def OAI.ThreeMachine.StackCompiler.Tree.reg line 41
  11. def OAI.ThreeMachine.StackCompiler.Tree.temp line 42
  12. def OAI.ThreeMachine.StackCompiler.Tree.memory line 44
  13. theorem OAI.ThreeMachine.StackCompiler.Tree.memory_reg line 47
  14. theorem OAI.ThreeMachine.StackCompiler.Tree.memory_temp line 49
  15. theorem OAI.ThreeMachine.StackCompiler.Tree.reg_ne_temp line 51
  16. theorem OAI.ThreeMachine.StackCompiler.Tree.temp_ne_reg line 56
  17. theorem OAI.ThreeMachine.StackCompiler.Tree.reg_eq_reg line 57
  18. theorem OAI.ThreeMachine.StackCompiler.Tree.temp_eq_temp line 58
  19. theorem OAI.ThreeMachine.StackCompiler.Tree.memory_update line 60
  20. def OAI.ThreeMachine.StackCompiler.Tree.nil line 69
  21. def OAI.ThreeMachine.StackCompiler.Tree.pair line 70
  22. theorem OAI.ThreeMachine.StackCompiler.Tree.nil_runs line 73
  23. theorem OAI.ThreeMachine.StackCompiler.Tree.pair_runs line 78
  24. def OAI.ThreeMachine.StackCompiler.Tree.work line 93
  25. theorem OAI.ThreeMachine.StackCompiler.Tree.work_reg line 96
  26. theorem OAI.ThreeMachine.StackCompiler.Tree.work_temp line 98
  27. theorem OAI.ThreeMachine.StackCompiler.Tree.work_update_temp line 101
  28. theorem OAI.ThreeMachine.StackCompiler.Tree.work_update_reg line 110
  29. theorem OAI.ThreeMachine.StackCompiler.Tree.work_empty line 119
  30. def OAI.ThreeMachine.StackCompiler.Tree.selectFinish line 124
  31. def OAI.ThreeMachine.StackCompiler.Tree.selectPair line 128
  32. def OAI.ThreeMachine.StackCompiler.Tree.selectAux line 134
  33. def OAI.ThreeMachine.StackCompiler.Tree.select line 138
  34. theorem OAI.ThreeMachine.StackCompiler.Tree.selectFinish_runs line 141
  35. theorem OAI.ThreeMachine.StackCompiler.Tree.selectPair_runs line 180
  36. theorem OAI.ThreeMachine.StackCompiler.Tree.selectAux_runs line 229
  37. theorem OAI.ThreeMachine.StackCompiler.Tree.select_runs line 254
  38. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.loop_stop line 273
  39. theorem OAI.ThreeMachine.StackCompiler.Program.Runs.loop_iterate line 277
  40. def OAI.ThreeMachine.StackCompiler.Tree.skip line 297
  41. theorem OAI.ThreeMachine.StackCompiler.Tree.skip_runs line 299
  42. def OAI.ThreeMachine.StackCompiler.Tree.copy line 303
  43. theorem OAI.ThreeMachine.StackCompiler.Tree.copy_runs line 306
  44. def OAI.ThreeMachine.StackCompiler.Tree.weight line 319
  45. theorem OAI.ThreeMachine.StackCompiler.Tree.one_le_weight line 321
  46. theorem OAI.ThreeMachine.StackCompiler.Tree.size_le_weight line 323
  47. inductive OAI.ThreeMachine.StackCompiler.Tree.Code line 328
  48. def OAI.ThreeMachine.StackCompiler.Tree._root_.OAI.ThreeMachine.StackCompiler.Data.nonempty line 338
  49. theorem OAI.ThreeMachine.StackCompiler.Tree._root_.OAI.ThreeMachine.StackCompiler.Data.encode_head line 340
  50. inductive OAI.ThreeMachine.StackCompiler.Tree.Eval line 343
  51. def OAI.ThreeMachine.StackCompiler.Tree.Code.compile line 359
  52. theorem OAI.ThreeMachine.StackCompiler.Tree.Eval.compile line 371