OAI/Computability/DepthThree/TapeParameterSearch.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.erase_output line 10
  2. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.decrement_candidate line 25
  3. abbrev OAI.DepthThreeLowerBound.TapeParameterSearch.CubeState line 38
  4. def OAI.DepthThreeLowerBound.TapeParameterSearch.cubeProgram line 40
  5. def OAI.DepthThreeLowerBound.TapeParameterSearch.cubeStart line 45
  6. def OAI.DepthThreeLowerBound.TapeParameterSearch.cubeDone line 46
  7. def OAI.DepthThreeLowerBound.TapeParameterSearch.cubeCost line 48
  8. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.runs_cube line 52
  9. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.cube_done line 63
  10. abbrev OAI.DepthThreeLowerBound.TapeParameterSearch.DecreaseState line 66
  11. def OAI.DepthThreeLowerBound.TapeParameterSearch.decreaseProgram line 68
  12. def OAI.DepthThreeLowerBound.TapeParameterSearch.decreaseStart line 71
  13. def OAI.DepthThreeLowerBound.TapeParameterSearch.decreaseDone line 72
  14. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.runs_decrease line 74
  15. abbrev OAI.DepthThreeLowerBound.TapeParameterSearch.CleanupState line 85
  16. def OAI.DepthThreeLowerBound.TapeParameterSearch.cleanupProgram line 87
  17. def OAI.DepthThreeLowerBound.TapeParameterSearch.cleanupStart line 91
  18. def OAI.DepthThreeLowerBound.TapeParameterSearch.cleanupDone line 92
  19. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.runs_cleanup line 94
  20. abbrev OAI.DepthThreeLowerBound.TapeParameterSearch.SixthState line 105
  21. def OAI.DepthThreeLowerBound.TapeParameterSearch.sixthProgram line 107
  22. def OAI.DepthThreeLowerBound.TapeParameterSearch.sixthStart line 111
  23. def OAI.DepthThreeLowerBound.TapeParameterSearch.sixthDone line 112
  24. def OAI.DepthThreeLowerBound.TapeParameterSearch.sixthCost line 114
  25. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.runs_sixth line 118
  26. theorem OAI.DepthThreeLowerBound.TapeParameterSearch.sixth_done line 129