OAI/Computability/DepthThree/TapeParse.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeParse.inputStore line 12
  2. theorem OAI.DepthThreeLowerBound.TapeParse.initializedTapes_eq_store line 16
  3. def OAI.DepthThreeLowerBound.TapeParse.outputStore line 22
  4. theorem OAI.DepthThreeLowerBound.TapeParse.outputStore_input line 27
  5. theorem OAI.DepthThreeLowerBound.TapeParse.outputStore_data line 31
  6. theorem OAI.DepthThreeLowerBound.TapeParse.outputStore_hash line 35
  7. theorem OAI.DepthThreeLowerBound.TapeParse.outputStore_order line 39
  8. theorem OAI.DepthThreeLowerBound.TapeParse.outputStore_empty line 43
  9. abbrev OAI.DepthThreeLowerBound.TapeParse.WorkState line 50
  10. def OAI.DepthThreeLowerBound.TapeParse.workProgram line 52
  11. def OAI.DepthThreeLowerBound.TapeParse.workStart line 55
  12. def OAI.DepthThreeLowerBound.TapeParse.workDone line 56
  13. abbrev OAI.DepthThreeLowerBound.TapeParse.State line 58
  14. def OAI.DepthThreeLowerBound.TapeParse.program line 60
  15. def OAI.DepthThreeLowerBound.TapeParse.start line 63
  16. def OAI.DepthThreeLowerBound.TapeParse.done line 64
  17. def OAI.DepthThreeLowerBound.TapeParse.acceptFlag line 66
  18. theorem OAI.DepthThreeLowerBound.TapeParse.acceptFlag_done line 70
  19. theorem OAI.DepthThreeLowerBound.TapeParse.program_done line 72
  20. theorem OAI.DepthThreeLowerBound.TapeParse.runs_parse line 74