OAI/Computability/DegreeRigidity/OrdinalCodes/RankRecursion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.InternalRank.rankSet line 10
  2. theorem OAI.TuringRigidity.InternalRank.mem_rankSet line 16
  3. theorem OAI.TuringRigidity.InternalRank.rankSet_mem line 27
  4. theorem OAI.TuringRigidity.InternalRank.rankSet_transitive line 30
  5. def OAI.TuringRigidity.InternalRank.Step line 38
  6. def OAI.TuringRigidity.InternalRank.Graph line 42
  7. theorem OAI.TuringRigidity.InternalRank.Graph.correct line 49
  8. theorem OAI.TuringRigidity.InternalRank.Graph.unique line 69
  9. def OAI.TuringRigidity.InternalRank.Code.step line 84
  10. theorem OAI.TuringRigidity.InternalRank.Code.eval_step line 90
  11. def OAI.TuringRigidity.InternalRank.Code.graph line 95
  12. theorem OAI.TuringRigidity.InternalRank.Code.eval_graph line 99