OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalInputSyntax.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.RelativeConstructible.ownStageFormulaline 10 - theorem
OAI.TuringRigidity.RelativeConstructible.ownStageFormula_specline 13 - def
OAI.TuringRigidity.RelativeConstructible.Construction.ordinalInputsline 37 - def
OAI.TuringRigidity.RelativeConstructible.Construction.ordinalInputFormulaline 42 - def
OAI.TuringRigidity.RelativeConstructible.ordinalBodySlotsline 47 - def
OAI.TuringRigidity.RelativeConstructible.Construction.ordinalMembershipline 52 - theorem
OAI.TuringRigidity.RelativeConstructible.ordinalBodySlots_specline 56 - theorem
OAI.TuringRigidity.RelativeConstructible.Construction.ordinalMembership_specline 69