OAI/Computability/DegreeRigidity/Syntax/SentenceCode.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.SentenceCoding.atom line 9
  2. def OAI.TuringRigidity.SentenceCoding.cell line 10
  3. def OAI.TuringRigidity.SentenceCoding.binary line 11
  4. def OAI.TuringRigidity.SentenceCoding.unary line 12
  5. theorem OAI.TuringRigidity.SentenceCoding.encode_equal line 14
  6. theorem OAI.TuringRigidity.SentenceCoding.encode_member line 16
  7. theorem OAI.TuringRigidity.SentenceCoding.encode_conj line 18
  8. theorem OAI.TuringRigidity.SentenceCoding.encode_neg line 20
  9. theorem OAI.TuringRigidity.SentenceCoding.encode_ex line 22
  10. theorem OAI.TuringRigidity.SentenceCoding.cell_left_lt line 25
  11. theorem OAI.TuringRigidity.SentenceCoding.cell_right_le line 29
  12. theorem OAI.TuringRigidity.SentenceCoding.binary_left_lt line 31
  13. theorem OAI.TuringRigidity.SentenceCoding.binary_right_lt line 33
  14. theorem OAI.TuringRigidity.SentenceCoding.unary_child_lt line 35
  15. def OAI.TuringRigidity.SentenceCoding.Step line 38
  16. def OAI.TuringRigidity.SentenceCoding.Children line 45
  17. theorem OAI.TuringRigidity.SentenceCoding.step_encode line 50
  18. def OAI.TuringRigidity.SentenceCoding.Closed line 56
  19. theorem OAI.TuringRigidity.SentenceCoding.Closed.valid line 58