OAI/Computability/DepthThree/TapePower.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapePower.State line 13
  2. instance OAI.DepthThreeLowerBound.TapePower.(instance at line 17) line 17
  3. def OAI.DepthThreeLowerBound.TapePower.start line 25
  4. def OAI.DepthThreeLowerBound.TapePower.done line 29
  5. def OAI.DepthThreeLowerBound.TapePower.program line 33
  6. def OAI.DepthThreeLowerBound.TapePower.resultTapes line 40
  7. def OAI.DepthThreeLowerBound.TapePower.resultRegister line 47
  8. def OAI.DepthThreeLowerBound.TapePower.cost line 51
  9. theorem OAI.DepthThreeLowerBound.TapePower.swap_tapes line 55
  10. theorem OAI.DepthThreeLowerBound.TapePower.runs_power line 76
  11. theorem OAI.DepthThreeLowerBound.TapePower.program_done line 96
  12. theorem OAI.DepthThreeLowerBound.TapePower.resultTapes_result line 103
  13. theorem OAI.DepthThreeLowerBound.TapePower.resultTapes_source line 115
  14. theorem OAI.DepthThreeLowerBound.TapePower.resultTapes_scratch line 123
  15. theorem OAI.DepthThreeLowerBound.TapePower.resultTapes_other line 131
  16. theorem OAI.DepthThreeLowerBound.TapePower.cost_eq_sum line 140