OAI/Computability/DegreeRigidity/Effective/LocalColumnCertificates.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.LocalColumnCertificates.Output line 8
  2. theorem OAI.TuringRigidity.LocalColumnCertificates.output_sigma line 12
  3. def OAI.TuringRigidity.LocalColumnCertificates.Presents line 29
  4. theorem OAI.TuringRigidity.LocalColumnCertificates.output_iff line 32
  5. def OAI.TuringRigidity.LocalColumnCertificates.Noncoding line 43
  6. theorem OAI.TuringRigidity.LocalColumnCertificates.noncoding_sigma line 50
  7. theorem OAI.TuringRigidity.LocalColumnCertificates.noncoding_condition_iff line 61
  8. theorem OAI.TuringRigidity.LocalColumnCertificates.noncoding_iff line 70
  9. def OAI.TuringRigidity.LocalColumnCertificates.Allowed line 78
  10. theorem OAI.TuringRigidity.LocalColumnCertificates.allowed_sigma line 84
  11. def OAI.TuringRigidity.LocalColumnCertificates.Extension line 94
  12. theorem OAI.TuringRigidity.LocalColumnCertificates.extension_sigma line 99
  13. theorem OAI.TuringRigidity.LocalColumnCertificates.extension_condition_iff line 108
  14. theorem OAI.TuringRigidity.LocalColumnCertificates.extension_iff line 127
  15. def OAI.TuringRigidity.LocalColumnCertificates.Bad line 135
  16. theorem OAI.TuringRigidity.LocalColumnCertificates.bad_sigma line 141
  17. theorem OAI.TuringRigidity.LocalColumnCertificates.guarded_search line 151
  18. theorem OAI.TuringRigidity.LocalColumnCertificates.bad_condition_iff line 157
  19. theorem OAI.TuringRigidity.LocalColumnCertificates.bad_iff line 165