OAI/Computability/DegreeRigidity/OrdinalCodes/NumericParameters.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.NumericSyntax.params line 10
  2. def OAI.TuringRigidity.NumericSyntax.Covers line 13
  3. def OAI.TuringRigidity.NumericSyntax.Numeric line 15
  4. theorem OAI.TuringRigidity.NumericSyntax.Numeric.congr line 20
  5. theorem OAI.TuringRigidity.NumericSyntax.Numeric.subst line 24
  6. theorem OAI.TuringRigidity.NumericSyntax.Numeric.neg line 30
  7. theorem OAI.TuringRigidity.NumericSyntax.Numeric.and line 34
  8. theorem OAI.TuringRigidity.NumericSyntax.Numeric.existsMem line 38
  9. theorem OAI.TuringRigidity.NumericSyntax.Numeric.existsNat line 45
  10. theorem OAI.TuringRigidity.NumericSyntax.defOr line 53
  11. theorem OAI.TuringRigidity.NumericSyntax.defImp line 55
  12. theorem OAI.TuringRigidity.NumericSyntax.defIff line 57
  13. theorem OAI.TuringRigidity.NumericSyntax.defAllMem line 59
  14. theorem OAI.TuringRigidity.NumericSyntax.defAllNat line 61
  15. theorem OAI.TuringRigidity.NumericSyntax.equal_definable line 64
  16. theorem OAI.TuringRigidity.NumericSyntax.member_definable line 66
  17. theorem OAI.TuringRigidity.NumericSyntax.memberNat line 68
  18. theorem OAI.TuringRigidity.NumericSyntax.equalZero line 70
  19. theorem OAI.TuringRigidity.NumericSyntax.defSubset line 72
  20. theorem OAI.TuringRigidity.NumericSyntax.defPairMem line 74
  21. theorem OAI.TuringRigidity.NumericSyntax.defOrderedPair line 76
  22. theorem OAI.TuringRigidity.NumericSyntax.unaryGraph_definable line 79
  23. theorem OAI.TuringRigidity.NumericSyntax.binaryGraph_definable line 96