OAI/Computability/DepthThree/TapeDecodeBlocks.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DepthThreeLowerBound.TapeDecodeBlocks.TailState line 10
  2. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.tailProgram line 12
  3. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.tailStart line 16
  4. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.tailDone line 17
  5. abbrev OAI.DepthThreeLowerBound.TapeDecodeBlocks.RestState line 19
  6. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.restProgram line 21
  7. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.restStart line 24
  8. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.restDone line 25
  9. abbrev OAI.DepthThreeLowerBound.TapeDecodeBlocks.State line 27
  10. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.program line 29
  11. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.start line 32
  12. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.done line 33
  13. theorem OAI.DepthThreeLowerBound.TapeDecodeBlocks.program_done line 35
  14. def OAI.DepthThreeLowerBound.TapeDecodeBlocks.outputStore line 37
  15. theorem OAI.DepthThreeLowerBound.TapeDecodeBlocks.outputStore_block line 43
  16. theorem OAI.DepthThreeLowerBound.TapeDecodeBlocks.outputStore_other line 49
  17. theorem OAI.DepthThreeLowerBound.TapeDecodeBlocks.runs_decode line 56