OAI/Computability/DepthThree/TapeHashOuter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DepthThreeLowerBound.TapeHashOuter.State line 10
2. def OAI.DepthThreeLowerBound.TapeHashOuter.program line 12
3. def OAI.DepthThreeLowerBound.TapeHashOuter.start line 15
4. def OAI.DepthThreeLowerBound.TapeHashOuter.done line 16
5. def OAI.DepthThreeLowerBound.TapeHashOuter.progressStore line 18
6. theorem OAI.DepthThreeLowerBound.TapeHashOuter.progress_zero line 23
7. theorem OAI.DepthThreeLowerBound.TapeHashOuter.progress_step line 28
8. theorem OAI.DepthThreeLowerBound.TapeHashOuter.row_cost_le line 41
9. theorem OAI.DepthThreeLowerBound.TapeHashOuter.runs_outer line 51
10. theorem OAI.DepthThreeLowerBound.TapeHashOuter.program_done line 87