OAI/Computability/DegreeRigidity/Syntax/FiniteFragment.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.Formula.scope line 11
2. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.realize_congr line 17
3. def OAI.TuringRigidity.BoundedSetTheory.Formula.width line 36
4. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.scope_le_width line 42
5. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.takeEnv line 47
6. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.length_takeEnv line 51
7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.takeEnv_mem line 56
8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.takeEnv_agree line 66
9. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.witnessBody line 74
10. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.eval_witnessBody line 77
11. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.occurrences line 92
12. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.fragment line 98
13. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.occurrence_width line 101
14. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.Witnesses line 118
15. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.realize_of_witnesses line 124