OAI/Computability/DepthThree/TapeInputPrepare.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeInputPrepare.SumMinusState line 13
  2. def OAI.DepthThreeLowerBound.TapeInputPrepare.sumMinusProgram line 15
  3. def OAI.DepthThreeLowerBound.TapeInputPrepare.sumMinusStart line 20
  4. def OAI.DepthThreeLowerBound.TapeInputPrepare.sumMinusDone line 22
  5. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.sumMinusProgram_done line 25
  6. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_decrement line 28
  7. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_sumMinus line 36
  8. abbrev OAI.DepthThreeLowerBound.TapeInputPrepare.OffsetState line 71
  9. def OAI.DepthThreeLowerBound.TapeInputPrepare.offsetProgram line 73
  10. def OAI.DepthThreeLowerBound.TapeInputPrepare.offsetStart line 77
  11. def OAI.DepthThreeLowerBound.TapeInputPrepare.offsetDone line 78
  12. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.offsetProgram_done line 80
  13. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_offset line 82
  14. def OAI.DepthThreeLowerBound.TapeInputPrepare.terminalProgram line 107
  15. abbrev OAI.DepthThreeLowerBound.TapeInputPrepare.HashState line 109
  16. def OAI.DepthThreeLowerBound.TapeInputPrepare.hashProgram line 111
  17. def OAI.DepthThreeLowerBound.TapeInputPrepare.hashStart line 116
  18. def OAI.DepthThreeLowerBound.TapeInputPrepare.hashDone line 117
  19. abbrev OAI.DepthThreeLowerBound.TapeInputPrepare.PolynomialState line 119
  20. def OAI.DepthThreeLowerBound.TapeInputPrepare.polynomialProgram line 121
  21. def OAI.DepthThreeLowerBound.TapeInputPrepare.polynomialStart line 124
  22. def OAI.DepthThreeLowerBound.TapeInputPrepare.polynomialDone line 125
  23. abbrev OAI.DepthThreeLowerBound.TapeInputPrepare.CoefficientsState line 127
  24. def OAI.DepthThreeLowerBound.TapeInputPrepare.coefficientsProgram line 129
  25. def OAI.DepthThreeLowerBound.TapeInputPrepare.coefficientsStart line 135
  26. def OAI.DepthThreeLowerBound.TapeInputPrepare.coefficientsDone line 136
  27. def OAI.DepthThreeLowerBound.TapeInputPrepare.State line 138
  28. instance OAI.DepthThreeLowerBound.TapeInputPrepare.(instance at line 144) line 144
  29. def OAI.DepthThreeLowerBound.TapeInputPrepare.program line 147
  30. def OAI.DepthThreeLowerBound.TapeInputPrepare.start line 153
  31. def OAI.DepthThreeLowerBound.TapeInputPrepare.done line 159
  32. def OAI.DepthThreeLowerBound.TapeInputPrepare.outputStore line 165
  33. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.outputStore_offset line 170
  34. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.outputStore_length line 174
  35. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.outputStore_other line 178
  36. def OAI.DepthThreeLowerBound.TapeInputPrepare.cost line 183
  37. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_hash line 193
  38. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_polynomial line 215
  39. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_coefficients line 233
  40. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.runs_prepare line 265
  41. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.cost_le line 293
  42. theorem OAI.DepthThreeLowerBound.TapeInputPrepare.program_done line 304