OAI/Computability/DepthThree/TapeRouting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeRouting.joinCode line 12
  2. theorem OAI.DepthThreeLowerBound.TapeRouting.join_runs line 20
  3. theorem OAI.DepthThreeLowerBound.TapeRouting.join_done line 36
  4. abbrev OAI.DepthThreeLowerBound.TapeRouting.LoopState line 41
  5. def OAI.DepthThreeLowerBound.TapeRouting.loopTest line 43
  6. def OAI.DepthThreeLowerBound.TapeRouting.loopBody line 44
  7. def OAI.DepthThreeLowerBound.TapeRouting.loopDone line 45
  8. def OAI.DepthThreeLowerBound.TapeRouting.loopCode line 47
  9. theorem OAI.DepthThreeLowerBound.TapeRouting.loop_test_runs line 59
  10. theorem OAI.DepthThreeLowerBound.TapeRouting.loop_body_runs line 69
  11. theorem OAI.DepthThreeLowerBound.TapeRouting.loop_exit line 79
  12. theorem OAI.DepthThreeLowerBound.TapeRouting.loop_iter line 91
  13. theorem OAI.DepthThreeLowerBound.TapeRouting.loop_done line 108