OAI/Computability/DegreeRigidity/SetModels/SetModelMultiplicationStep.lean
15 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.SetModelArithmetic.numberPairline 10 - theorem
OAI.TuringRigidity.SetModelArithmetic.numberPair_injectiveline 12 - def
OAI.TuringRigidity.SetModelArithmetic.pairNumbersline 17 - theorem
OAI.TuringRigidity.SetModelArithmetic.mem_pairNumbersline 19 - def
OAI.TuringRigidity.SetModelArithmetic.addStepline 29 - theorem
OAI.TuringRigidity.SetModelArithmetic.addStep_numberPairline 33 - theorem
OAI.TuringRigidity.SetModelArithmetic.addStep_closedline 39 - def
OAI.TuringRigidity.SetModelArithmetic.addStepSetline 45 - theorem
OAI.TuringRigidity.SetModelArithmetic.pair_mem_addStepSetline 48 - def
OAI.TuringRigidity.SetModelArithmetic.addStepFormulaline 57 - theorem
OAI.TuringRigidity.SetModelArithmetic.eval_addStepFormulaline 62 - theorem
OAI.TuringRigidity.SetModelArithmetic.addStepSet_memline 85 - theorem
OAI.TuringRigidity.SetModelArithmetic.iterate_addStepline 103 - def
OAI.TuringRigidity.SetModelArithmetic.multiplicationIterationline 109 - theorem
OAI.TuringRigidity.SetModelArithmetic.multiplicationIteration_memline 111