OAI/Computability/DegreeRigidity/Syntax/BoundedRelations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.Formula.imp line 10
2. def OAI.TuringRigidity.BoundedSetTheory.Formula.iff line 11
3. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_imp line 13
4. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_iff line 23
5. def OAI.TuringRigidity.BoundedSetTheory.Formula.subset line 27
6. def OAI.TuringRigidity.BoundedSetTheory.Formula.transitive line 28
7. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_subset line 30
8. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_transitive line 35
9. def OAI.TuringRigidity.BoundedSetTheory.Formula.functionGraph line 40
10. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_functionGraph line 46
11. inductive OAI.TuringRigidity.BoundedSetTheory.SigmaFormula line 56
12. def OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.Realize line 60
13. def OAI.TuringRigidity.BoundedSetTheory.SigmaReplacement line 64
14. theorem OAI.TuringRigidity.BoundedSetTheory.replacement_image line 71