OAI/Computability/DepthThree/TapeDecodeBlock.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DepthThreeLowerBound.TapeDecodeBlock.FinishState line 12
2. def OAI.DepthThreeLowerBound.TapeDecodeBlock.finishProgram line 14
3. def OAI.DepthThreeLowerBound.TapeDecodeBlock.finishStart line 18
4. def OAI.DepthThreeLowerBound.TapeDecodeBlock.finishDone line 19
5. abbrev OAI.DepthThreeLowerBound.TapeDecodeBlock.State line 21
6. def OAI.DepthThreeLowerBound.TapeDecodeBlock.program line 23
7. def OAI.DepthThreeLowerBound.TapeDecodeBlock.start line 26
8. def OAI.DepthThreeLowerBound.TapeDecodeBlock.done line 27
9. theorem OAI.DepthThreeLowerBound.TapeDecodeBlock.program_done line 29
10. def OAI.DepthThreeLowerBound.TapeDecodeBlock.outputStore line 32
11. theorem OAI.DepthThreeLowerBound.TapeDecodeBlock.runs_block line 35