OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalCodeOperations.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.OrdinalCoding.codePowerAtline 10 - def
OAI.TuringRigidity.OrdinalCoding.codeSumAtline 13 - def
OAI.TuringRigidity.OrdinalCoding.codeScaleAtline 16 - def
OAI.TuringRigidity.OrdinalCoding.codeScaleline 19 - theorem
OAI.TuringRigidity.OrdinalCoding.codePowerAt_soundline 22 - theorem
OAI.TuringRigidity.OrdinalCoding.codePowerAt_sourceTline 29 - theorem
OAI.TuringRigidity.OrdinalCoding.codeSumAt_soundline 36 - theorem
OAI.TuringRigidity.OrdinalCoding.codeSumAt_sourceTline 43 - theorem
OAI.TuringRigidity.OrdinalCoding.codeScaleAt_soundline 50 - theorem
OAI.TuringRigidity.OrdinalCoding.codeScaleAt_sourceTline 60 - theorem
OAI.TuringRigidity.OrdinalCoding.codeScale_internalline 70