OAI/Computability/Scheduling/StackMachine.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.ThreeMachine.StackCompiler.Action line 9
  2. def OAI.ThreeMachine.StackCompiler.Action.apply line 15
  3. abbrev OAI.ThreeMachine.StackCompiler.Store line 20
  4. abbrev OAI.ThreeMachine.StackCompiler.Heads line 21
  5. abbrev OAI.ThreeMachine.StackCompiler.Actions line 22
  6. structure OAI.ThreeMachine.StackCompiler.Program line 24
  7. structure OAI.ThreeMachine.StackCompiler.State line 28
  8. def OAI.ThreeMachine.StackCompiler.Program.step line 32
  9. def OAI.ThreeMachine.StackCompiler.Program.run line 36
  10. def OAI.ThreeMachine.StackCompiler.Program.Computes line 39
  11. def OAI.ThreeMachine.StackCompiler.symbol line 42
  12. def OAI.ThreeMachine.StackCompiler.unsymbol line 44
  13. theorem OAI.ThreeMachine.StackCompiler.unsymbol_symbol line 47
  14. theorem OAI.ThreeMachine.StackCompiler.unsymbol_zero line 50
  15. def OAI.ThreeMachine.StackCompiler.stackTape line 52
  16. theorem OAI.ThreeMachine.StackCompiler.head_stackTape line 55
  17. def OAI.ThreeMachine.StackCompiler.phaseOne line 60
  18. def OAI.ThreeMachine.StackCompiler.phaseTwo line 66
  19. def OAI.ThreeMachine.StackCompiler.applyTape line 71
  20. def OAI.ThreeMachine.StackCompiler.middleTape line 77
  21. theorem OAI.ThreeMachine.StackCompiler.blank_cons line 80
  22. theorem OAI.ThreeMachine.StackCompiler.tape_two_phases line 84
  23. abbrev OAI.ThreeMachine.StackCompiler.Control line 104
  24. def OAI.ThreeMachine.StackCompiler.numberControl line 109
  25. def OAI.ThreeMachine.StackCompiler.readControl line 112
  26. theorem OAI.ThreeMachine.StackCompiler.read_numberControl line 116
  27. theorem OAI.ThreeMachine.StackCompiler.read_zero line 119
  28. def OAI.ThreeMachine.StackCompiler.compile line 122
  29. abbrev OAI.ThreeMachine.StackCompiler.TapeCfg line 129
  30. def OAI.ThreeMachine.StackCompiler.Relates line 131
  31. def OAI.ThreeMachine.StackCompiler.middleCfg line 134
  32. def OAI.ThreeMachine.StackCompiler.readyCfg line 137
  33. theorem OAI.ThreeMachine.StackCompiler.relates_ready line 140
  34. theorem OAI.ThreeMachine.StackCompiler.step_ready line 143
  35. theorem OAI.ThreeMachine.StackCompiler.step_middle line 162
  36. theorem OAI.ThreeMachine.StackCompiler.halted_iff line 172
  37. theorem OAI.ThreeMachine.StackCompiler.two_steps line 178
  38. theorem OAI.ThreeMachine.StackCompiler.simulate line 192
  39. def OAI.ThreeMachine.StackCompiler.initialStore line 202
  40. theorem OAI.ThreeMachine.StackCompiler.relates_initial line 204
  41. theorem OAI.ThreeMachine.StackCompiler.simulate_initial line 212
  42. theorem OAI.ThreeMachine.StackCompiler.compile_produces line 216
  43. inductive OAI.ThreeMachine.StackCompiler.Program.Exec line 230
  44. theorem OAI.ThreeMachine.StackCompiler.Program.Exec.iterate line 234
  45. theorem OAI.ThreeMachine.StackCompiler.Program.Exec.halted line 240
  46. def OAI.ThreeMachine.StackCompiler.Program.State.mapControl line 246
  47. theorem OAI.ThreeMachine.StackCompiler.Program.Exec.continue line 248
  48. theorem OAI.ThreeMachine.StackCompiler.Program.lift_step line 258
  49. def OAI.ThreeMachine.StackCompiler.Program.stayActions line 272
  50. def OAI.ThreeMachine.StackCompiler.Program.seq line 274
  51. theorem OAI.ThreeMachine.StackCompiler.Program.seq_left_step line 282
  52. theorem OAI.ThreeMachine.StackCompiler.Program.seq_right_exec line 289
  53. theorem OAI.ThreeMachine.StackCompiler.Program.seq_exec line 303
  54. def OAI.ThreeMachine.StackCompiler.Program.instruction line 314
  55. theorem OAI.ThreeMachine.StackCompiler.Program.instruction_exec line 318
  56. def OAI.ThreeMachine.StackCompiler.Program.loop line 324
  57. theorem OAI.ThreeMachine.StackCompiler.Program.loop_body_step line 332
  58. theorem OAI.ThreeMachine.StackCompiler.Program.loop_stop line 339
  59. theorem OAI.ThreeMachine.StackCompiler.Program.loop_iterate line 344
  60. def OAI.ThreeMachine.StackCompiler.Program.transferActions line 366
  61. def OAI.ThreeMachine.StackCompiler.Program.transfer line 369
  62. def OAI.ThreeMachine.StackCompiler.Program.transferResult line 372
  63. def OAI.ThreeMachine.StackCompiler.Program.transferOnce line 375
  64. theorem OAI.ThreeMachine.StackCompiler.Program.transfer_instruction line 378
  65. theorem OAI.ThreeMachine.StackCompiler.Program.transfer_result_once line 394
  66. theorem OAI.ThreeMachine.StackCompiler.Program.transfer_exec line 406
  67. def OAI.ThreeMachine.StackCompiler.Program.popActions line 435
  68. def OAI.ThreeMachine.StackCompiler.Program.clear line 437
  69. theorem OAI.ThreeMachine.StackCompiler.Program.pop_instruction line 440
  70. theorem OAI.ThreeMachine.StackCompiler.Program.clear_exec line 448
  71. def OAI.ThreeMachine.StackCompiler.Program.spreadActions line 466
  72. def OAI.ThreeMachine.StackCompiler.Program.spread line 469
  73. def OAI.ThreeMachine.StackCompiler.Program.spreadResult line 472
  74. def OAI.ThreeMachine.StackCompiler.Program.spreadOnce line 476
  75. theorem OAI.ThreeMachine.StackCompiler.Program.spread_instruction line 479
  76. theorem OAI.ThreeMachine.StackCompiler.Program.spread_result_once line 495
  77. theorem OAI.ThreeMachine.StackCompiler.Program.spread_exec line 510
  78. def OAI.ThreeMachine.StackCompiler.Program.prepend line 536
  79. theorem OAI.ThreeMachine.StackCompiler.Program.prepend_exec line 539
  80. def OAI.ThreeMachine.StackCompiler.Program.copy line 565
  81. theorem OAI.ThreeMachine.StackCompiler.Program.copy_exec line 568