OAI/Computability/DegreeRigidity/Effective/FiniteTuple.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_rename line 11
  2. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.code line 30
  3. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.space line 34
  4. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend line 38
  5. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend_nil line 41
  6. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend_cons line 42
  7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.space_mem line 45
  8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.mem_space line 57
  9. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.code_mem_space line 79
  10. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.code_mem line 83
  11. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.code_injective_length line 92
  12. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend_tail line 104
  13. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend_congr line 110
  14. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.rotate line 118
  15. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.prepend_rotate line 122