OAI/Analysis/MatrixSigning/Arithmetic/SubtractionBorrow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W19.subtractionBorrow line 10
2. theorem OAI.KS.W19.borrow_column_lift line 18
3. theorem OAI.KS.W19.subtractionBorrow_identity line 25
4. theorem OAI.KS.W19.subtractionBorrow_true_iff line 58
5. def OAI.KS.W19.saturatingSubtractBits line 65
6. theorem OAI.KS.W19.saturatingSubtractBits_correct line 68
7. theorem OAI.KS.W19.saturatingSubtractBits_length line 84