OAI/Analysis/MatrixSigning/Arithmetic/RationalAddCorrect.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W13.RationalAdd.preNormalizeTicks_le line 13
2. theorem OAI.KS.W13.RationalAdd.totalTicks_le_polynomial line 36
3. theorem OAI.KS.W13.RationalAdd.polynomial_spec line 72
4. theorem OAI.KS.W13.RationalAdd.init_eq line 78
5. theorem OAI.KS.W13.RationalAdd.output_encoded_rationals line 84
6. theorem OAI.KS.W13.RationalAdd.halts_encoded_rationals line 93
7. theorem OAI.KS.W13.RationalAdd.intermediate_stack_length_le line 102
8. theorem OAI.KS.W13.RationalAdd.intermediate_storage_le line 117
9. theorem OAI.KS.W13.RationalAdd.uniform_rational_addition line 128