OAI/Computability/DepthThree/TapeBranch.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DepthThreeLowerBound.TapeBranch.State line 12
2. def OAI.DepthThreeLowerBound.TapeBranch.test line 14
3. def OAI.DepthThreeLowerBound.TapeBranch.body line 15
4. def OAI.DepthThreeLowerBound.TapeBranch.rejected line 16
5. def OAI.DepthThreeLowerBound.TapeBranch.program line 18
6. theorem OAI.DepthThreeLowerBound.TapeBranch.rejected_halts line 27
7. theorem OAI.DepthThreeLowerBound.TapeBranch.body_halts line 31
8. theorem OAI.DepthThreeLowerBound.TapeBranch.runs_test line 37
9. theorem OAI.DepthThreeLowerBound.TapeBranch.runs_reject line 45
10. theorem OAI.DepthThreeLowerBound.TapeBranch.runs_accept line 55