OAI/Analysis/MatrixSigning/Arithmetic/BinaryMultiplySemantics.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.KS.W03.BinaryMultiply.RippleExec line 13
2. theorem OAI.KS.W03.BinaryMultiply.ripple_execution line 22
3. theorem OAI.KS.W03.BinaryMultiply.RippleExec.unique line 36
4. inductive OAI.KS.W03.BinaryMultiply.RawMultiplyExec line 48
5. theorem OAI.KS.W03.BinaryMultiply.multiplyRaw_execution line 55
6. theorem OAI.KS.W03.BinaryMultiply.RawMultiplyExec.unique line 63
7. inductive OAI.KS.W03.BinaryMultiply.TrimExec line 73
8. theorem OAI.KS.W03.BinaryMultiply.trim_execution line 79
9. theorem OAI.KS.W03.BinaryMultiply.TrimExec.unique line 85
10. inductive OAI.KS.W03.BinaryMultiply.MultiplyExec line 93
11. theorem OAI.KS.W03.BinaryMultiply.multiply_execution line 99
12. theorem OAI.KS.W03.BinaryMultiply.MultiplyExec.unique line 103
13. theorem OAI.KS.W03.BinaryMultiply.execution_correct_and_bounded line 111
14. theorem OAI.KS.W03.BinaryMultiply.exists_execution line 119