OAI/Computability/DegreeRigidity/Effective/EffectivePresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.EffectivePresentation.pick line 11
2. theorem OAI.TuringRigidity.EffectivePresentation.pick_recursive line 13
3. def OAI.TuringRigidity.EffectivePresentation.selected line 21
4. theorem OAI.TuringRigidity.EffectivePresentation.selected_reduces line 25
5. theorem OAI.TuringRigidity.EffectivePresentation.selected_column line 34
6. def OAI.TuringRigidity.EffectivePresentation.emptyAntichain line 39
7. theorem OAI.TuringRigidity.EffectivePresentation.emptyAntichain_holds line 41
8. def OAI.TuringRigidity.EffectivePresentation.emptyRelation line 44
9. theorem OAI.TuringRigidity.EffectivePresentation.emptyRelation_below line 47
10. theorem OAI.TuringRigidity.EffectivePresentation.emptyRelation_holds line 50
11. theorem OAI.TuringRigidity.EffectivePresentation.effective_coding line 54