OAI/Computability/DegreeRigidity/Syntax/AtomicEncoding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.AtomicForcing.eq_of_encode_eq line 10
  2. theorem OAI.TuringRigidity.AtomicForcing.eq_encode_congr line 32
  3. theorem OAI.TuringRigidity.AtomicForcing.mem_congr_left line 40
  4. theorem OAI.TuringRigidity.AtomicForcing.mem_congr_right line 48
  5. theorem OAI.TuringRigidity.AtomicForcing.mem_encode_congr line 59
  6. def OAI.TuringRigidity.AtomicForcing.EncodedEq line 67
  7. def OAI.TuringRigidity.AtomicForcing.EncodedMem line 69
  8. theorem OAI.TuringRigidity.AtomicForcing.encodedEq_toEncoded line 72
  9. theorem OAI.TuringRigidity.AtomicForcing.encodedMem_toEncoded line 77