OAI/Analysis/MatrixSigning/Arithmetic/RationalMagnitudeSetup.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W30.RationalMagnitudeMachine.stacks_core line 12
2. theorem OAI.KS.W30.RationalMagnitudeMachine.stacks_spare_value line 16
3. theorem OAI.KS.W30.RationalMagnitudeMachine.stacks_spare line 32
4. theorem OAI.KS.W30.RationalMagnitudeMachine.core_spec line 41
5. def OAI.KS.W30.RationalMagnitudeMachine.copiedNumeratorWork line 51
6. theorem OAI.KS.W30.RationalMagnitudeMachine.copyNumerator_spec line 54
7. theorem OAI.KS.W30.RationalMagnitudeMachine.reverseNumeratorCopy_spec line 68
8. theorem OAI.KS.W30.RationalMagnitudeMachine.copyDenominator_spec line 82
9. theorem OAI.KS.W30.RationalMagnitudeMachine.prepare_spec line 96
10. theorem OAI.KS.W30.RationalMagnitudeMachine.gcd_spec line 103
11. def OAI.KS.W30.RationalMagnitudeMachine.reversedGCDWork line 111
12. def OAI.KS.W30.RationalMagnitudeMachine.divisorWork line 113
13. def OAI.KS.W30.RationalMagnitudeMachine.divisorState line 115
14. theorem OAI.KS.W30.RationalMagnitudeMachine.reverseGCD_spec line 118
15. theorem OAI.KS.W30.RationalMagnitudeMachine.placeGCD_spec line 133
16. theorem OAI.KS.W30.RationalMagnitudeMachine.computeGCD_spec line 149