OAI/Analysis/MatrixSigning/Arithmetic/RationalAddPrimitives.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W13.RationalAdd.rawAddProgram line 15
2. def OAI.KS.W13.RationalAdd.addTrimProgram line 18
3. def OAI.KS.W13.RationalAdd.canonicalAddProgram line 21
4. def OAI.KS.W13.RationalAdd.addResult line 24
5. def OAI.KS.W13.RationalAdd.canonicalAddTicks line 27
6. theorem OAI.KS.W13.RationalAdd.rawAdd_spec line 30
7. theorem OAI.KS.W13.RationalAdd.canonicalAdd_spec line 56
8. theorem OAI.KS.W13.RationalAdd.canonicalAddTicks_le line 68
9. theorem OAI.KS.W13.RationalAdd.addResult_length_le line 74
10. theorem OAI.KS.W13.RationalAdd.addResult_canonical line 82