OAI/Computability/DegreeRigidity/Effective/CodingGeneric.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.CodingGeneric.Dense line 8
  2. theorem OAI.TuringRigidity.CodingGeneric.extend_dense line 11
  3. def OAI.TuringRigidity.CodingGeneric.stage line 21
  4. theorem OAI.TuringRigidity.CodingGeneric.stage_spec line 26
  5. theorem OAI.TuringRigidity.CodingGeneric.stage_mono line 33
  6. def OAI.TuringRigidity.CodingGeneric.leftReal line 40
  7. def OAI.TuringRigidity.CodingGeneric.rightReal line 42
  8. theorem OAI.TuringRigidity.CodingGeneric.leftReal_extends line 45
  9. theorem OAI.TuringRigidity.CodingGeneric.rightReal_extends line 54
  10. theorem OAI.TuringRigidity.CodingGeneric.coding_agreement line 63
  11. abbrev OAI.TuringRigidity.CodingGeneric.RequirementIndex line 75
  12. def OAI.TuringRigidity.CodingGeneric.requirements line 77
  13. theorem OAI.TuringRigidity.CodingGeneric.requirements_dense line 83
  14. theorem OAI.TuringRigidity.CodingGeneric.readColumn_not_reduces line 91
  15. theorem OAI.TuringRigidity.CodingGeneric.common_noncomputable_columns line 109
  16. theorem OAI.TuringRigidity.CodingGeneric.coding_first_clause line 137