OAI/Computability/DepthThree/TapeRewind.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DepthThreeLowerBound.cursorTape_left_nil line 11
2. theorem OAI.DepthThreeLowerBound.cursorTape_left_append line 16
3. inductive OAI.DepthThreeLowerBound.TapeRewind.State line 25
4. instance OAI.DepthThreeLowerBound.TapeRewind.(instance at line 30) line 30
5. def OAI.DepthThreeLowerBound.TapeRewind.program line 36
6. theorem OAI.DepthThreeLowerBound.TapeRewind.step_cursor line 40
7. theorem OAI.DepthThreeLowerBound.TapeRewind.step_home line 48
8. theorem OAI.DepthThreeLowerBound.TapeRewind.runs_cursor line 54