OAI/Computability/DegreeRigidity/Syntax/BoundedSetTheory.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.TuringRigidity.BoundedSetTheory.Formula line 10
  2. def OAI.TuringRigidity.BoundedSetTheory.cons line 17
  3. theorem OAI.TuringRigidity.BoundedSetTheory.cons_zero line 21
  4. theorem OAI.TuringRigidity.BoundedSetTheory.cons_succ line 22
  5. def OAI.TuringRigidity.BoundedSetTheory.Formula.Eval line 25
  6. def OAI.TuringRigidity.BoundedSetTheory.Formula.Realize line 32
  7. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.absolute line 39
  8. def OAI.TuringRigidity.BoundedSetTheory.Pairing line 55
  9. def OAI.TuringRigidity.BoundedSetTheory.Union line 58
  10. def OAI.TuringRigidity.BoundedSetTheory.PowerSet line 61
  11. def OAI.TuringRigidity.BoundedSetTheory.Separation line 64
  12. theorem OAI.TuringRigidity.BoundedSetTheory.pair_mem line 68
  13. theorem OAI.TuringRigidity.BoundedSetTheory.singleton_mem line 83
  14. theorem OAI.TuringRigidity.BoundedSetTheory.orderedPair_mem line 87
  15. theorem OAI.TuringRigidity.BoundedSetTheory.union_mem line 91
  16. theorem OAI.TuringRigidity.BoundedSetTheory.internal_power line 107
  17. theorem OAI.TuringRigidity.BoundedSetTheory.sep_mem line 119
  18. def OAI.TuringRigidity.BoundedSetTheory.Formula.disj line 142
  19. def OAI.TuringRigidity.BoundedSetTheory.Formula.allMem line 143
  20. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_disj line 145
  21. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_allMem line 157
  22. def OAI.TuringRigidity.BoundedSetTheory.Formula.singleton line 162
  23. def OAI.TuringRigidity.BoundedSetTheory.Formula.unorderedPair line 165
  24. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_singleton line 169
  25. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_unorderedPair line 181
  26. def OAI.TuringRigidity.BoundedSetTheory.Formula.orderedPair line 193
  27. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_orderedPair line 198
  28. def OAI.TuringRigidity.BoundedSetTheory.Formula.pairMem line 213
  29. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_pairMem line 215