OAI/Computability/DegreeRigidity/Effective/EffectiveCohen.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.EffectiveCohen.word_decision line 9
  2. def OAI.TuringRigidity.EffectiveCohen.decider line 44
  3. theorem OAI.TuringRigidity.EffectiveCohen.decider_recursive line 46
  4. theorem OAI.TuringRigidity.EffectiveCohen.decider_spec line 50
  5. def OAI.TuringRigidity.EffectiveCohen.grow line 56
  6. theorem OAI.TuringRigidity.EffectiveCohen.grow_primrec line 58
  7. def OAI.TuringRigidity.EffectiveCohen.stage line 61
  8. theorem OAI.TuringRigidity.EffectiveCohen.stage_recursive line 65
  9. theorem OAI.TuringRigidity.EffectiveCohen.stage_prefix line 86
  10. theorem OAI.TuringRigidity.EffectiveCohen.stage_length line 91
  11. theorem OAI.TuringRigidity.EffectiveCohen.stage_prefix_of_le line 100
  12. def OAI.TuringRigidity.EffectiveCohen.generic line 105
  13. theorem OAI.TuringRigidity.EffectiveCohen.generic_extends line 107
  14. theorem OAI.TuringRigidity.EffectiveCohen.generic_reduces line 116
  15. def OAI.TuringRigidity.EffectiveCohen.OneGeneric line 124
  16. theorem OAI.TuringRigidity.EffectiveCohen.generic_oneGeneric line 128
  17. theorem OAI.TuringRigidity.EffectiveCohen.relative_generic line 137