OAI/Computability/DepthThree/TapeCancel.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeCancel.ReadState line 10
  2. abbrev OAI.DepthThreeLowerBound.TapeCancel.ClearState line 11
  3. abbrev OAI.DepthThreeLowerBound.TapeCancel.State line 12
  4. def OAI.DepthThreeLowerBound.TapeCancel.readProgram line 14
  5. def OAI.DepthThreeLowerBound.TapeCancel.clearProgram line 18
  6. def OAI.DepthThreeLowerBound.TapeCancel.haltProgram line 22
  7. def OAI.DepthThreeLowerBound.TapeCancel.program line 24
  8. def OAI.DepthThreeLowerBound.TapeCancel.start line 27
  9. def OAI.DepthThreeLowerBound.TapeCancel.done line 28
  10. def OAI.DepthThreeLowerBound.TapeCancel.resultStore line 30
  11. def OAI.DepthThreeLowerBound.TapeCancel.cost line 33
  12. theorem OAI.DepthThreeLowerBound.TapeCancel.set_eq_split line 35
  13. theorem OAI.DepthThreeLowerBound.TapeCancel.clear_at line 43
  14. theorem OAI.DepthThreeLowerBound.TapeCancel.update_output line 57
  15. theorem OAI.DepthThreeLowerBound.TapeCancel.runs_cancel line 65
  16. theorem OAI.DepthThreeLowerBound.TapeCancel.program_done line 127