OAI/Computability/DepthThree/TapeProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeFlags line 8
  2. def OAI.DepthThreeLowerBound.TapeFlags.get line 12
  3. def OAI.DepthThreeLowerBound.TapeFlags.set line 14
  4. def OAI.DepthThreeLowerBound.TapeFlags.save line 17
  5. theorem OAI.DepthThreeLowerBound.TapeFlags.get_set_self line 19
  6. theorem OAI.DepthThreeLowerBound.TapeFlags.get_set_of_ne line 23
  7. theorem OAI.DepthThreeLowerBound.TapeFlags.save_symbol line 27
  8. theorem OAI.DepthThreeLowerBound.TapeFlags.save_flags line 29
  9. inductive OAI.DepthThreeLowerBound.TapeInstr line 33
  10. def OAI.DepthThreeLowerBound.TapeInstr.toStmt line 45
  11. abbrev OAI.DepthThreeLowerBound.TapeProgram line 55
  12. def OAI.DepthThreeLowerBound.TapeProgram.code line 61
  13. def OAI.DepthThreeLowerBound.TapeProgram.cfg line 64
  14. theorem OAI.DepthThreeLowerBound.TapeProgram.step_move line 67
  15. theorem OAI.DepthThreeLowerBound.TapeProgram.step_write line 72
  16. theorem OAI.DepthThreeLowerBound.TapeProgram.step_load line 78
  17. theorem OAI.DepthThreeLowerBound.TapeProgram.step_branch line 84
  18. theorem OAI.DepthThreeLowerBound.TapeProgram.step_scan_stop line 93
  19. theorem OAI.DepthThreeLowerBound.TapeProgram.step_scan_move line 100
  20. theorem OAI.DepthThreeLowerBound.TapeProgram.step_halt line 107