OAI/Computability/DepthThree/TapeParameters.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters line 12
  2. def OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters line 17
  3. theorem OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters_zero line 22
  4. theorem OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters_one line 23
  5. theorem OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters_two line 24
  6. theorem OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters_three line 25
  7. theorem OAI.DepthThreeLowerBound.TapeParameters.cubeRegisters_four line 26
  8. theorem OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters_zero line 27
  9. theorem OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters_one line 28
  10. theorem OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters_two line 29
  11. theorem OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters_three line 30
  12. theorem OAI.DepthThreeLowerBound.TapeParameters.sixthRegisters_four line 31
  13. def OAI.DepthThreeLowerBound.TapeParameters.dataStore line 33
  14. def OAI.DepthThreeLowerBound.TapeParameters.outputStore line 36
  15. theorem OAI.DepthThreeLowerBound.TapeParameters.outputStore_data line 41
  16. theorem OAI.DepthThreeLowerBound.TapeParameters.outputStore_hash line 45
  17. theorem OAI.DepthThreeLowerBound.TapeParameters.outputStore_order line 49
  18. theorem OAI.DepthThreeLowerBound.TapeParameters.outputStore_other line 53
  19. abbrev OAI.DepthThreeLowerBound.TapeParameters.LengthState line 57
  20. def OAI.DepthThreeLowerBound.TapeParameters.lengthProgram line 59
  21. def OAI.DepthThreeLowerBound.TapeParameters.lengthStart line 63
  22. def OAI.DepthThreeLowerBound.TapeParameters.lengthDone line 64
  23. theorem OAI.DepthThreeLowerBound.TapeParameters.runs_length line 66
  24. abbrev OAI.DepthThreeLowerBound.TapeParameters.SquareState line 97
  25. def OAI.DepthThreeLowerBound.TapeParameters.squareProgram line 99
  26. def OAI.DepthThreeLowerBound.TapeParameters.squareStart line 102
  27. def OAI.DepthThreeLowerBound.TapeParameters.squareDone line 103
  28. def OAI.DepthThreeLowerBound.TapeParameters.squareCost line 104
  29. theorem OAI.DepthThreeLowerBound.TapeParameters.runs_square line 106
  30. abbrev OAI.DepthThreeLowerBound.TapeParameters.FinishState line 137
  31. def OAI.DepthThreeLowerBound.TapeParameters.finishProgram line 139
  32. def OAI.DepthThreeLowerBound.TapeParameters.finishStart line 143
  33. def OAI.DepthThreeLowerBound.TapeParameters.finishDone line 144
  34. abbrev OAI.DepthThreeLowerBound.TapeParameters.RootsState line 146
  35. def OAI.DepthThreeLowerBound.TapeParameters.rootsProgram line 148
  36. def OAI.DepthThreeLowerBound.TapeParameters.rootsStart line 151
  37. def OAI.DepthThreeLowerBound.TapeParameters.rootsDone line 152
  38. abbrev OAI.DepthThreeLowerBound.TapeParameters.WorkState line 154
  39. def OAI.DepthThreeLowerBound.TapeParameters.workProgram line 156
  40. def OAI.DepthThreeLowerBound.TapeParameters.workStart line 159
  41. def OAI.DepthThreeLowerBound.TapeParameters.workDone line 160
  42. abbrev OAI.DepthThreeLowerBound.TapeParameters.State line 162
  43. def OAI.DepthThreeLowerBound.TapeParameters.program line 164
  44. def OAI.DepthThreeLowerBound.TapeParameters.start line 167
  45. def OAI.DepthThreeLowerBound.TapeParameters.done line 168
  46. def OAI.DepthThreeLowerBound.TapeParameters.cost line 170
  47. theorem OAI.DepthThreeLowerBound.TapeParameters.candidate_zero line 175
  48. theorem OAI.DepthThreeLowerBound.TapeParameters.runs_parameters line 180
  49. theorem OAI.DepthThreeLowerBound.TapeParameters.program_done line 238