OAI/Computability/DegreeRigidity/OrdinalCodes/IndexMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.IndexMatrix.machine line 8
2. theorem OAI.TuringRigidity.IndexMatrix.machine_primrec line 10
3. theorem OAI.TuringRigidity.IndexMatrix.machine_encode line 13
4. theorem OAI.TuringRigidity.IndexMatrix.run_uniform_recursive line 16
5. def OAI.TuringRigidity.IndexMatrix.validMatrix line 38
6. instance OAI.TuringRigidity.IndexMatrix.(instance at line 45) line 45
7. theorem OAI.TuringRigidity.IndexMatrix.valid_normal_form line 49
8. def OAI.TuringRigidity.IndexMatrix.checkMatrix line 78
9. theorem OAI.TuringRigidity.IndexMatrix.checkMatrix_primrec line 85
10. theorem OAI.TuringRigidity.IndexMatrix.validMatrix_recursive line 99