OAI/Computability/DepthThree/TapeSearchBody.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeSearchBody.amount line 10
  2. def OAI.DepthThreeLowerBound.TapeSearchBody.incrementCost line 11
  3. abbrev OAI.DepthThreeLowerBound.TapeSearchBody.IncrementState line 13
  4. def OAI.DepthThreeLowerBound.TapeSearchBody.tailProgram line 15
  5. def OAI.DepthThreeLowerBound.TapeSearchBody.incrementProgram line 18
  6. def OAI.DepthThreeLowerBound.TapeSearchBody.incrementStart line 22
  7. def OAI.DepthThreeLowerBound.TapeSearchBody.incrementDone line 23
  8. theorem OAI.DepthThreeLowerBound.TapeSearchBody.increment_store line 26
  9. theorem OAI.DepthThreeLowerBound.TapeSearchBody.runs_increment line 34
  10. theorem OAI.DepthThreeLowerBound.TapeSearchBody.increment_done line 58
  11. abbrev OAI.DepthThreeLowerBound.TapeSearchBody.State line 62
  12. def OAI.DepthThreeLowerBound.TapeSearchBody.program line 64
  13. def OAI.DepthThreeLowerBound.TapeSearchBody.start line 69
  14. def OAI.DepthThreeLowerBound.TapeSearchBody.done line 70
  15. def OAI.DepthThreeLowerBound.TapeSearchBody.cost line 72
  16. theorem OAI.DepthThreeLowerBound.TapeSearchBody.runs_body line 75
  17. theorem OAI.DepthThreeLowerBound.TapeSearchBody.program_done line 92