OAI/Computability/DepthThree/TapeInputBlockLoop.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.Registers line 12
  2. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.source line 14
  3. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.index line 15
  4. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.count line 16
  5. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.scratch line 17
  6. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.destination line 18
  7. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.register_eq line 20
  8. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.index_ne_source line 23
  9. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.blockStore line 26
  10. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_source line 32
  11. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_index line 37
  12. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_count line 42
  13. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.blockStore_destination line 47
  14. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_count line 52
  15. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_index line 61
  16. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.update_blockStore_destination line 70
  17. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.BodyState line 76
  18. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.bodyProgram line 78
  19. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.bodyStart line 83
  20. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.bodyDone line 84
  21. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.body_done line 86
  22. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.runs_body line 89
  23. abbrev OAI.DepthThreeLowerBound.TapeInputBlockLoop.State line 122
  24. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.program line 124
  25. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.start line 128
  26. def OAI.DepthThreeLowerBound.TapeInputBlockLoop.done line 129
  27. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.program_done line 131
  28. theorem OAI.DepthThreeLowerBound.TapeInputBlockLoop.runs_block line 134