OAI/Computability/DepthThree/TapeRemainderOuter.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DepthThreeLowerBound.TapeRemainderOuter.ScratchEmpty line 12
  2. abbrev OAI.DepthThreeLowerBound.TapeRemainderOuter.BodyState line 15
  3. def OAI.DepthThreeLowerBound.TapeRemainderOuter.tailProgram line 18
  4. def OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyProgram line 22
  5. def OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyStart line 25
  6. def OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyDone line 26
  7. def OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyCost line 28
  8. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyProgram_done line 31
  9. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.cleanup_result line 35
  10. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.runs_body line 68
  11. def OAI.DepthThreeLowerBound.TapeRemainderOuter.iterationCost line 106
  12. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.bodyCost_le line 108
  13. abbrev OAI.DepthThreeLowerBound.TapeRemainderOuter.State line 114
  14. def OAI.DepthThreeLowerBound.TapeRemainderOuter.program line 116
  15. def OAI.DepthThreeLowerBound.TapeRemainderOuter.start line 119
  16. def OAI.DepthThreeLowerBound.TapeRemainderOuter.done line 120
  17. def OAI.DepthThreeLowerBound.TapeRemainderOuter.frame line 122
  18. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.frame_counter line 126
  19. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.frame_output line 129
  20. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.frame_poly line 132
  21. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.frame_degree line 135
  22. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.frame_clean line 139
  23. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.update_counter line 144
  24. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.update_output line 152
  25. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.runs_loop line 160
  26. theorem OAI.DepthThreeLowerBound.TapeRemainderOuter.program_done line 198