OAI/Computability/DegreeRigidity/SetModels/RelationPresentation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.RelationPresentation.ACode line 11
  2. def OAI.TuringRigidity.RelationPresentation.ACode.Good line 16
  3. def OAI.TuringRigidity.RelationPresentation.ACode.decode line 18
  4. def OAI.TuringRigidity.RelationPresentation.ACode.Holds line 20
  5. theorem OAI.TuringRigidity.RelationPresentation.ACode.holds_iff line 23
  6. theorem OAI.TuringRigidity.RelationPresentation.ACode.sigma line 27
  7. theorem OAI.TuringRigidity.RelationPresentation.ACode.exists_code line 31
  8. structure OAI.TuringRigidity.RelationPresentation.SCode line 38
  9. def OAI.TuringRigidity.RelationPresentation.SCode.Good line 43
  10. def OAI.TuringRigidity.RelationPresentation.SCode.decode line 45
  11. def OAI.TuringRigidity.RelationPresentation.SCode.Graph line 47
  12. theorem OAI.TuringRigidity.RelationPresentation.SCode.graph_iff line 50
  13. theorem OAI.TuringRigidity.RelationPresentation.SCode.sigma line 55
  14. theorem OAI.TuringRigidity.RelationPresentation.SCode.exists_code line 60
  15. structure OAI.TuringRigidity.RelationPresentation.RCode line 67
  16. def OAI.TuringRigidity.RelationPresentation.RCode.Good line 71
  17. def OAI.TuringRigidity.RelationPresentation.RCode.decode line 73
  18. def OAI.TuringRigidity.RelationPresentation.RCode.Holds line 76
  19. theorem OAI.TuringRigidity.RelationPresentation.RCode.sigma line 82
  20. theorem OAI.TuringRigidity.RelationPresentation.RCode.holds_iff line 94
  21. theorem OAI.TuringRigidity.RelationPresentation.RCode.exists_code line 123
  22. theorem OAI.TuringRigidity.RelationPresentation.sigma5_decoding line 135