OAI/Computability/DepthThree/TapeForLoop.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeForLoop.BodyState line 16
  2. abbrev OAI.DepthThreeLowerBound.TapeForLoop.State line 17
  3. def OAI.DepthThreeLowerBound.TapeForLoop.bodyProgram line 19
  4. def OAI.DepthThreeLowerBound.TapeForLoop.bodyStart line 23
  5. def OAI.DepthThreeLowerBound.TapeForLoop.bodyDone line 25
  6. def OAI.DepthThreeLowerBound.TapeForLoop.again line 27
  7. def OAI.DepthThreeLowerBound.TapeForLoop.program line 31
  8. def OAI.DepthThreeLowerBound.TapeForLoop.start line 36
  9. def OAI.DepthThreeLowerBound.TapeForLoop.done line 38
  10. theorem OAI.DepthThreeLowerBound.TapeForLoop.body_done line 40
  11. theorem OAI.DepthThreeLowerBound.TapeForLoop.program_done line 43
  12. theorem OAI.DepthThreeLowerBound.TapeForLoop.runs_body line 47
  13. theorem OAI.DepthThreeLowerBound.TapeForLoop.runs_iteration line 65
  14. theorem OAI.DepthThreeLowerBound.TapeForLoop.runs_exit line 82
  15. theorem OAI.DepthThreeLowerBound.TapeForLoop.runs line 93
  16. theorem OAI.DepthThreeLowerBound.TapeForLoop.runs_zero line 120