OAI/Computability/DegreeRigidity/OrdinalCodes/OrdinalProductSyntax.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.OrdinalArithmetic.productDomainMatrix line 9
2. theorem OAI.TuringRigidity.OrdinalArithmetic.productDomainMatrix_eval line 13
3. def OAI.TuringRigidity.OrdinalArithmetic.productRelationMatrix line 30
4. theorem OAI.TuringRigidity.OrdinalArithmetic.productRelationMatrix_eval line 36
5. def OAI.TuringRigidity.OrdinalArithmetic.productMatrix line 61
6. theorem OAI.TuringRigidity.OrdinalArithmetic.productMatrix_eval line 65
7. def OAI.TuringRigidity.OrdinalArithmetic.productSentence line 73
8. theorem OAI.TuringRigidity.OrdinalArithmetic.productSentence_bound line 76
9. theorem OAI.TuringRigidity.OrdinalArithmetic.productSentence_semantics line 78
10. theorem OAI.TuringRigidity.OrdinalArithmetic.productSentence_sound line 96
11. theorem OAI.TuringRigidity.OrdinalArithmetic.productSentence_spec_of_certificate line 107
12. theorem OAI.TuringRigidity.OrdinalArithmetic.productSentence_sourceT line 121