OAI/Computability/DegreeRigidity/SetModels/InternalNameEvaluation.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.activeRelationline 11 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.active_pairline 15 - def
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.activeFormulaline 25 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.activeRelation_memline 28 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.active_wellFoundedline 36 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.value_eqline 42 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.name_value_memline 69 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalNameEvaluation.extension_subsetline 84