OAI/Computability/PerfectCompleteness/Sampling/OriginalUniformCut.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.OriginalUniformCut.uniform_equiv line 18
2. theorem OAI.PerfectCompleteness.OriginalUniformCut.uniform_map_product line 24
3. def OAI.PerfectCompleteness.OriginalUniformCut.recordStepEquiv line 37
4. def OAI.PerfectCompleteness.OriginalUniformCut.toStoppedTape line 59
5. theorem OAI.PerfectCompleteness.OriginalUniformCut.evaluate_toStoppedTape line 74
6. theorem OAI.PerfectCompleteness.OriginalUniformCut.uniform_toStoppedTape line 95
7. def OAI.PerfectCompleteness.OriginalUniformCut.referenceLaw line 147
8. theorem OAI.PerfectCompleteness.OriginalUniformCut.referenceLaw_uniform line 156
9. theorem OAI.PerfectCompleteness.OriginalUniformCut.reconstruct_referenceLaw line 163