OAI/Computability/DegreeRigidity/Constructibility/ConstructionInputData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.TuringRigidity.RelativeConstructible.ConstructionInput line 9
2. def OAI.TuringRigidity.RelativeConstructible.pathReal line 14
3. def OAI.TuringRigidity.RelativeConstructible.ConstructionInput.value line 18
4. def OAI.TuringRigidity.RelativeConstructible.ConstructionInput.prefix line 24
5. theorem OAI.TuringRigidity.RelativeConstructible.ConstructionInput.prefix_value line 29
6. def OAI.TuringRigidity.RelativeConstructible.ConstructionInput.Indexed line 34
7. theorem OAI.TuringRigidity.RelativeConstructible.ConstructionInput.prefix_indexed line 39
8. def OAI.TuringRigidity.RelativeConstructible.Construction.inputData line 43
9. theorem OAI.TuringRigidity.RelativeConstructible.Construction.inputs_eq_data line 52
10. theorem OAI.TuringRigidity.RelativeConstructible.Construction.inputData_indexed line 66
11. def OAI.TuringRigidity.RelativeConstructible.Construction.membershipFormula line 83
12. theorem OAI.TuringRigidity.RelativeConstructible.Construction.membershipFormula_spec line 86
13. theorem OAI.TuringRigidity.RelativeConstructible.Construction.finite_membership_definition line 110