OAI/Computability/PerfectCompleteness/Foundations/CutCallExtension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PerfectCompleteness.CutCallExtension.Extended line 19
2. def OAI.PerfectCompleteness.CutCallExtension.original line 21
3. def OAI.PerfectCompleteness.CutCallExtension.fresh line 25
4. def OAI.PerfectCompleteness.CutCallExtension.observe line 28
5. def OAI.PerfectCompleteness.CutCallExtension.splitAssembled line 32
6. theorem OAI.PerfectCompleteness.CutCallExtension.splitAssembled_surjective line 39
7. theorem OAI.PerfectCompleteness.CutCallExtension.split_assemble line 46
8. theorem OAI.PerfectCompleteness.CutCallExtension.observe_law line 50
9. theorem OAI.PerfectCompleteness.CutCallExtension.call_count line 62