OAI/Computability/DegreeRigidity/Constructibility/SingleRealConstruction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.RelativeConstructible.bitOracle line 9
2. theorem OAI.TuringRigidity.RelativeConstructible.bitOracle_part line 11
3. def OAI.TuringRigidity.RelativeConstructible.Construction.stageInputs line 17
4. theorem OAI.TuringRigidity.RelativeConstructible.Construction.stageInputs_child line 22
5. theorem OAI.TuringRigidity.RelativeConstructible.Construction.stageInputs_mem line 30
6. def OAI.TuringRigidity.RelativeConstructible.Construction.singleFormula line 43
7. theorem OAI.TuringRigidity.RelativeConstructible.Construction.singleFormula_spec line 54
8. def OAI.TuringRigidity.RelativeConstructible.Construction.singleMembership line 97
9. def OAI.TuringRigidity.RelativeConstructible.Construction.singleInputs line 100
10. theorem OAI.TuringRigidity.RelativeConstructible.Construction.singleInputs_mem line 104
11. theorem OAI.TuringRigidity.RelativeConstructible.Construction.singleMembership_of_inputs line 118
12. theorem OAI.TuringRigidity.RelativeConstructible.Construction.singleMembership_spec line 142