OAI/Computability/DegreeRigidity/Syntax/BoundedDefinability.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedDefinability.mix line 10
  2. theorem OAI.TuringRigidity.BoundedDefinability.mix_even line 13
  3. theorem OAI.TuringRigidity.BoundedDefinability.mix_odd line 16
  4. theorem OAI.TuringRigidity.BoundedDefinability.parity_ext line 19
  5. def OAI.TuringRigidity.BoundedDefinability.slotMap line 31
  6. theorem OAI.TuringRigidity.BoundedDefinability.slotMap_even line 34
  7. theorem OAI.TuringRigidity.BoundedDefinability.slotMap_odd line 36
  8. theorem OAI.TuringRigidity.BoundedDefinability.mix_slotMap line 39
  9. def OAI.TuringRigidity.BoundedDefinability.Definable line 43
  10. theorem OAI.TuringRigidity.BoundedDefinability.Definable.congr line 49
  11. theorem OAI.TuringRigidity.BoundedDefinability.Definable.subst line 53
  12. theorem OAI.TuringRigidity.BoundedDefinability.Definable.neg line 60
  13. theorem OAI.TuringRigidity.BoundedDefinability.Definable.and line 64
  14. def OAI.TuringRigidity.BoundedDefinability.bindSlots line 79
  15. theorem OAI.TuringRigidity.BoundedDefinability.bindSlots_zero line 82
  16. theorem OAI.TuringRigidity.BoundedDefinability.bindSlots_even_succ line 83
  17. theorem OAI.TuringRigidity.BoundedDefinability.bindSlots_odd line 85
  18. theorem OAI.TuringRigidity.BoundedDefinability.bind_mix line 88
  19. theorem OAI.TuringRigidity.BoundedDefinability.Definable.existsMem line 98
  20. theorem OAI.TuringRigidity.BoundedDefinability.Definable.existsParam line 105
  21. theorem OAI.TuringRigidity.BoundedDefinability.equal_definable line 119
  22. theorem OAI.TuringRigidity.BoundedDefinability.member_definable line 122
  23. theorem OAI.TuringRigidity.BoundedDefinability.equal_param line 125
  24. theorem OAI.TuringRigidity.BoundedDefinability.pairMem_param line 129
  25. theorem OAI.TuringRigidity.BoundedDefinability.Definable.sep_mem line 133