OAI/Computability/DepthThree/TapeInputGuardLength.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeInputGuard.requiredLength line 13
  2. theorem OAI.DepthThreeLowerBound.TapeInputGuard.requiredLength_parameters line 15
  3. def OAI.DepthThreeLowerBound.TapeInputGuard.outputStore line 18
  4. theorem OAI.DepthThreeLowerBound.TapeInputGuard.outputStore_length line 21
  5. theorem OAI.DepthThreeLowerBound.TapeInputGuard.outputStore_other line 25
  6. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.ProductState line 29
  7. def OAI.DepthThreeLowerBound.TapeInputGuard.productProgram line 31
  8. def OAI.DepthThreeLowerBound.TapeInputGuard.productStart line 35
  9. def OAI.DepthThreeLowerBound.TapeInputGuard.productDone line 36
  10. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_product line 38
  11. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.RingSumState line 82
  12. def OAI.DepthThreeLowerBound.TapeInputGuard.ringSumProgram line 83
  13. def OAI.DepthThreeLowerBound.TapeInputGuard.ringSumStart line 86
  14. def OAI.DepthThreeLowerBound.TapeInputGuard.ringSumDone line 87
  15. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.AddSumState line 89
  16. def OAI.DepthThreeLowerBound.TapeInputGuard.addSumProgram line 90
  17. def OAI.DepthThreeLowerBound.TapeInputGuard.addSumStart line 92
  18. def OAI.DepthThreeLowerBound.TapeInputGuard.addSumDone line 93
  19. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.SumState line 95
  20. def OAI.DepthThreeLowerBound.TapeInputGuard.sumProgram line 96
  21. def OAI.DepthThreeLowerBound.TapeInputGuard.sumStart line 98
  22. def OAI.DepthThreeLowerBound.TapeInputGuard.sumDone line 99
  23. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_sum line 101
  24. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.TailState line 140
  25. def OAI.DepthThreeLowerBound.TapeInputGuard.tailProgram line 141
  26. def OAI.DepthThreeLowerBound.TapeInputGuard.tailStart line 143
  27. def OAI.DepthThreeLowerBound.TapeInputGuard.tailDone line 144
  28. abbrev OAI.DepthThreeLowerBound.TapeInputGuard.LengthState line 146
  29. def OAI.DepthThreeLowerBound.TapeInputGuard.lengthProgram line 147
  30. def OAI.DepthThreeLowerBound.TapeInputGuard.lengthStart line 149
  31. def OAI.DepthThreeLowerBound.TapeInputGuard.lengthDone line 150
  32. def OAI.DepthThreeLowerBound.TapeInputGuard.lengthCost line 152
  33. theorem OAI.DepthThreeLowerBound.TapeInputGuard.runs_length line 154
  34. theorem OAI.DepthThreeLowerBound.TapeInputGuard.lengthProgram_done line 182