OAI/Analysis/MatrixSigning/Arithmetic/RationalSubtractCorrect.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W13.RationalSubtract.serializeTicks_le line 11
2. theorem OAI.KS.W13.RationalSubtract.preparation_linear line 17
3. theorem OAI.KS.W13.RationalSubtract.totalTicks_le_polynomial line 26
4. theorem OAI.KS.W13.RationalSubtract.polynomial_spec line 48
5. theorem OAI.KS.W13.RationalSubtract.init_eq line 54
6. theorem OAI.KS.W13.RationalSubtract.output_encoded_rationals line 59
7. theorem OAI.KS.W13.RationalSubtract.halts_encoded_rationals line 68
8. theorem OAI.KS.W13.RationalSubtract.output_length_le line 77
9. theorem OAI.KS.W13.RationalSubtract.uniform_rational_subtraction line 81