OAI/Computability/DepthThree/TapeMultiply.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeMultiply.tapes line 10
  2. theorem OAI.DepthThreeLowerBound.TapeMultiply.tapes_outer line 15
  3. theorem OAI.DepthThreeLowerBound.TapeMultiply.tapes_source line 20
  4. theorem OAI.DepthThreeLowerBound.TapeMultiply.tapes_scratch line 25
  5. theorem OAI.DepthThreeLowerBound.TapeMultiply.tapes_destination line 30
  6. theorem OAI.DepthThreeLowerBound.TapeMultiply.tapes_other line 36
  7. theorem OAI.DepthThreeLowerBound.TapeMultiply.update_outer line 42
  8. theorem OAI.DepthThreeLowerBound.TapeMultiply.overlay_source_scratch line 50
  9. theorem OAI.DepthThreeLowerBound.TapeMultiply.overlay_scratch_destination line 68
  10. abbrev OAI.DepthThreeLowerBound.TapeMultiply.BodyState line 88
  11. def OAI.DepthThreeLowerBound.TapeMultiply.bodyProgram line 90
  12. def OAI.DepthThreeLowerBound.TapeMultiply.bodyStart line 94
  13. def OAI.DepthThreeLowerBound.TapeMultiply.bodyDone line 95
  14. theorem OAI.DepthThreeLowerBound.TapeMultiply.runs_body line 97
  15. theorem OAI.DepthThreeLowerBound.TapeMultiply.body_done line 122
  16. abbrev OAI.DepthThreeLowerBound.TapeMultiply.State line 125
  17. def OAI.DepthThreeLowerBound.TapeMultiply.program line 127
  18. def OAI.DepthThreeLowerBound.TapeMultiply.start line 131
  19. def OAI.DepthThreeLowerBound.TapeMultiply.done line 132
  20. theorem OAI.DepthThreeLowerBound.TapeMultiply.runs_mul line 134
  21. theorem OAI.DepthThreeLowerBound.TapeMultiply.program_done line 172