OAI/Computability/DepthThree/TapeProductLength.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeProductLength.State line 12
  2. def OAI.DepthThreeLowerBound.TapeProductLength.program line 14
  3. def OAI.DepthThreeLowerBound.TapeProductLength.start line 18
  4. def OAI.DepthThreeLowerBound.TapeProductLength.done line 19
  5. def OAI.DepthThreeLowerBound.TapeProductLength.outputStore line 21
  6. theorem OAI.DepthThreeLowerBound.TapeProductLength.outputStore_destination line 24
  7. theorem OAI.DepthThreeLowerBound.TapeProductLength.outputStore_other line 28
  8. def OAI.DepthThreeLowerBound.TapeProductLength.cost line 32
  9. theorem OAI.DepthThreeLowerBound.TapeProductLength.frame_store line 34
  10. theorem OAI.DepthThreeLowerBound.TapeProductLength.runs_product line 55
  11. theorem OAI.DepthThreeLowerBound.TapeProductLength.program_done line 92