OAI/Computability/DegreeRigidity/CohenForcing/EncodedForcing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.EncodedForcing.word line 9
  2. def OAI.TuringRigidity.EncodedForcing.left line 10
  3. def OAI.TuringRigidity.EncodedForcing.rawRight line 11
  4. def OAI.TuringRigidity.EncodedForcing.right line 12
  5. def OAI.TuringRigidity.EncodedForcing.active line 13
  6. def OAI.TuringRigidity.EncodedForcing.condition line 15
  7. def OAI.TuringRigidity.EncodedForcing.code line 19
  8. theorem OAI.TuringRigidity.EncodedForcing.condition_code line 21
  9. theorem OAI.TuringRigidity.EncodedForcing.word_primrec line 25
  10. theorem OAI.TuringRigidity.EncodedForcing.left_primrec line 26
  11. theorem OAI.TuringRigidity.EncodedForcing.rawRight_primrec line 27
  12. theorem OAI.TuringRigidity.EncodedForcing.right_primrec line 29
  13. theorem OAI.TuringRigidity.EncodedForcing.active_primrec line 32
  14. theorem OAI.TuringRigidity.EncodedForcing.recursive_primrecPred line 35
  15. theorem OAI.TuringRigidity.EncodedForcing.prefix_recursive line 41
  16. def OAI.TuringRigidity.EncodedForcing.columns line 47
  17. theorem OAI.TuringRigidity.EncodedForcing.bounded_conjunction_iff line 49
  18. theorem OAI.TuringRigidity.EncodedForcing.extends_recursive line 66