OAI/Computability/DegreeRigidity/Syntax/SentenceCodeDefinability.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.SentenceCoding.defOr line 13
  2. theorem OAI.TuringRigidity.SentenceCoding.defImp line 17
  3. theorem OAI.TuringRigidity.SentenceCoding.defAllMem line 21
  4. theorem OAI.TuringRigidity.SentenceCoding.defAllParam line 25
  5. theorem OAI.TuringRigidity.SentenceCoding.defMemberParam line 29
  6. theorem OAI.TuringRigidity.SentenceCoding.defSubset line 33
  7. def OAI.TuringRigidity.SentenceCoding.UnaryGraph line 36
  8. def OAI.TuringRigidity.SentenceCoding.BinaryGraph line 39
  9. theorem OAI.TuringRigidity.SentenceCoding.unaryGraph_definable line 42
  10. theorem OAI.TuringRigidity.SentenceCoding.binaryGraph_definable line 57
  11. theorem OAI.TuringRigidity.SentenceCoding.atom_primrec line 80
  12. theorem OAI.TuringRigidity.SentenceCoding.cell_primrec line 82
  13. theorem OAI.TuringRigidity.SentenceCoding.binary_primrec line 85
  14. theorem OAI.TuringRigidity.SentenceCoding.unary_primrec line 89
  15. theorem OAI.TuringRigidity.SentenceCoding.atomic_primrec line 93