OAI/Computability/DegreeRigidity/SetModels/RegularCodeSplitting.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.RegularCodeSplitting.mem_basic_iff line 9
  2. theorem OAI.TuringRigidity.RegularCodeSplitting.basic_disjoint line 22
  3. def OAI.TuringRigidity.RegularCodeSplitting.remainder line 32
  4. theorem OAI.TuringRigidity.RegularCodeSplitting.remainder_isCode line 35
  5. theorem OAI.TuringRigidity.RegularCodeSplitting.remainder_mem line 48
  6. def OAI.TuringRigidity.RegularCodeSplitting.Partition line 54
  7. def OAI.TuringRigidity.RegularCodeSplitting.partitionFormula line 59
  8. theorem OAI.TuringRigidity.RegularCodeSplitting.partitionFormula_spec line 66
  9. theorem OAI.TuringRigidity.RegularCodeSplitting.partition_join line 71
  10. theorem OAI.TuringRigidity.RegularCodeSplitting.internal_partition line 87