OAI/Computability/DegreeRigidity/OrdinalCodes/NaturalDefinitions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.DefinesNatural line 9
2. def OAI.TuringRigidity.BoundedSetTheory.Formula.unaryVars line 15
3. def OAI.TuringRigidity.BoundedSetTheory.Formula.unary line 21
4. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.unary_spec line 23
5. def OAI.TuringRigidity.BoundedSetTheory.Formula.numericComposition line 30
6. def OAI.TuringRigidity.BoundedSetTheory.Formula.numericPair line 33
7. def OAI.TuringRigidity.BoundedSetTheory.Formula.pairedUnary line 36
8. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.pairedUnary_spec line 39
9. theorem OAI.TuringRigidity.BoundedSetTheory.definesNatural_zero line 56
10. theorem OAI.TuringRigidity.BoundedSetTheory.definesNatural_succ line 60
11. theorem OAI.TuringRigidity.BoundedSetTheory.DefinesNatural.comp line 65
12. theorem OAI.TuringRigidity.BoundedSetTheory.DefinesNatural.pair line 80