OAI/Computability/DepthThree/TapeCopy.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.DepthThreeLowerBound.TapeCopy.State line 13
  2. instance OAI.DepthThreeLowerBound.TapeCopy.(instance at line 20) line 20
  3. def OAI.DepthThreeLowerBound.TapeCopy.onPair line 26
  4. theorem OAI.DepthThreeLowerBound.TapeCopy.onPair_src line 30
  5. theorem OAI.DepthThreeLowerBound.TapeCopy.onPair_dst line 34
  6. theorem OAI.DepthThreeLowerBound.TapeCopy.onPair_other line 38
  7. def OAI.DepthThreeLowerBound.TapeCopy.emit line 43
  8. def OAI.DepthThreeLowerBound.TapeCopy.code line 47
  9. theorem OAI.DepthThreeLowerBound.TapeCopy.step_emit line 59
  10. theorem OAI.DepthThreeLowerBound.TapeCopy.step_start line 85
  11. theorem OAI.DepthThreeLowerBound.TapeCopy.step_scan_bit line 93
  12. theorem OAI.DepthThreeLowerBound.TapeCopy.step_scan_end line 103
  13. theorem OAI.DepthThreeLowerBound.TapeCopy.step_rewind_move line 111
  14. theorem OAI.DepthThreeLowerBound.TapeCopy.step_rewind_home line 119
  15. theorem OAI.DepthThreeLowerBound.TapeCopy.write_mk₂ line 127
  16. theorem OAI.DepthThreeLowerBound.TapeCopy.runs_scan line 131
  17. theorem OAI.DepthThreeLowerBound.TapeCopy.runs_rewind line 157
  18. theorem OAI.DepthThreeLowerBound.TapeCopy.runs_copy line 189
  19. theorem OAI.DepthThreeLowerBound.TapeCopy.step_done line 212