OAI/Analysis/MatrixSigning/Arithmetic/RationalMagnitudeDivision.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W30.RationalMagnitudeMachine.divisionWork line 13
2. def OAI.KS.W30.RationalMagnitudeMachine.quotientWork line 15
3. def OAI.KS.W30.RationalMagnitudeMachine.reversedQuotientWork line 17
4. def OAI.KS.W30.RationalMagnitudeMachine.remainderWork line 19
5. theorem OAI.KS.W30.RationalMagnitudeMachine.divide_spec line 22
6. theorem OAI.KS.W30.RationalMagnitudeMachine.reverseQuotient_spec line 40
7. theorem OAI.KS.W30.RationalMagnitudeMachine.clearRemainder_spec line 55
8. theorem OAI.KS.W30.RationalMagnitudeMachine.takeNumerator_spec line 69
9. theorem OAI.KS.W30.RationalMagnitudeMachine.trimNumerator_input line 84
10. theorem OAI.KS.W30.RationalMagnitudeMachine.trimNumerator_output line 91
11. theorem OAI.KS.W30.RationalMagnitudeMachine.trimNumerator_spec line 98
12. theorem OAI.KS.W30.RationalMagnitudeMachine.reduceNumerator_spec line 106
13. theorem OAI.KS.W30.RationalMagnitudeMachine.takeDenominator_spec line 131
14. theorem OAI.KS.W30.RationalMagnitudeMachine.trimDenominator_input line 146
15. theorem OAI.KS.W30.RationalMagnitudeMachine.trimDenominator_output line 153
16. theorem OAI.KS.W30.RationalMagnitudeMachine.trimDenominator_spec line 160
17. theorem OAI.KS.W30.RationalMagnitudeMachine.reduceDenominator_spec line 168