OAI/Computability/DepthThree/TapeErase.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.TapeErase.State line 10
  2. instance OAI.DepthThreeLowerBound.TapeErase.(instance at line 18) line 18
  3. def OAI.DepthThreeLowerBound.TapeErase.code line 24
  4. theorem OAI.DepthThreeLowerBound.TapeErase.step_start line 37
  5. theorem OAI.DepthThreeLowerBound.TapeErase.step_scan_bit line 44
  6. theorem OAI.DepthThreeLowerBound.TapeErase.step_scan_end line 52
  7. theorem OAI.DepthThreeLowerBound.TapeErase.step_erase_symbol line 59
  8. theorem OAI.DepthThreeLowerBound.TapeErase.step_erase_home line 67
  9. theorem OAI.DepthThreeLowerBound.TapeErase.step_install line 75
  10. theorem OAI.DepthThreeLowerBound.TapeErase.mk₂_append_blanks line 83
  11. theorem OAI.DepthThreeLowerBound.TapeErase.runs_scan line 90
  12. theorem OAI.DepthThreeLowerBound.TapeErase.runs_finish line 112
  13. theorem OAI.DepthThreeLowerBound.TapeErase.runs_erase_back line 129
  14. theorem OAI.DepthThreeLowerBound.TapeErase.runs_erase line 153
  15. theorem OAI.DepthThreeLowerBound.TapeErase.step_done line 173