OAI/Computability/DegreeRigidity/Effective/CodingForcing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.CodingForcing.Condition line 7
  2. def OAI.TuringRigidity.CodingForcing.CodingLocation line 13
  3. def OAI.TuringRigidity.CodingForcing.Extends line 17
  4. theorem OAI.TuringRigidity.CodingForcing.extends_refl line 22
  5. theorem OAI.TuringRigidity.CodingForcing.getD_of_prefix line 27
  6. theorem OAI.TuringRigidity.CodingForcing.extends_trans line 32
  7. theorem OAI.TuringRigidity.CodingForcing.extends_antisymm line 43
  8. def OAI.TuringRigidity.CodingForcing.activate line 52
  9. theorem OAI.TuringRigidity.CodingForcing.activate_extends line 55
  10. theorem OAI.TuringRigidity.CodingForcing.active_dense line 61
  11. def OAI.TuringRigidity.CodingForcing.append line 66
  12. theorem OAI.TuringRigidity.CodingForcing.append_extends line 72
  13. theorem OAI.TuringRigidity.CodingForcing.arbitrary_left_extension line 80
  14. theorem OAI.TuringRigidity.CodingForcing.length_dense line 86
  15. theorem OAI.TuringRigidity.CodingForcing.codingLocation_unbounded line 91