OAI/Combinatorics/UniformKServer/LiteralBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniformKServer.LiteralBound.program line 13
2. abbrev OAI.UniformKServer.LiteralBound.Init line 14
3. def OAI.UniformKServer.LiteralBound.finishes line 16
4. theorem OAI.UniformKServer.LiteralBound.primitive_finishes line 19
5. theorem OAI.UniformKServer.LiteralBound.finishes_run line 24
6. theorem OAI.UniformKServer.LiteralBound.exists_time line 29
7. theorem OAI.UniformKServer.LiteralBound.monotone_time line 37
8. theorem OAI.UniformKServer.LiteralBound.correct_at line 43