OAI/Computability/DepthThree/TapeRemainder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DepthThreeLowerBound.TapeRemainder.State line 10
2. def OAI.DepthThreeLowerBound.TapeRemainder.program line 12
3. def OAI.DepthThreeLowerBound.TapeRemainder.start line 16
4. def OAI.DepthThreeLowerBound.TapeRemainder.done line 17
5. def OAI.DepthThreeLowerBound.TapeRemainder.cost line 19
6. theorem OAI.DepthThreeLowerBound.TapeRemainder.cost_le line 21
7. theorem OAI.DepthThreeLowerBound.TapeRemainder.input_frame line 25
8. theorem OAI.DepthThreeLowerBound.TapeRemainder.output_frame line 37
9. theorem OAI.DepthThreeLowerBound.TapeRemainder.runs_remainder line 48
10. theorem OAI.DepthThreeLowerBound.TapeRemainder.program_done line 73