OAI/Analysis/MatrixSigning/Arithmetic/DivisionLoopModel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W19.DivisionLoop.advance line 11
2. theorem OAI.KS.W19.DivisionLoop.advance_correct line 16
3. def OAI.KS.W19.DivisionLoop.process line 44
4. theorem OAI.KS.W19.DivisionLoop.bitsValue_append_digit line 50
5. theorem OAI.KS.W19.DivisionLoop.process_correct line 56
6. theorem OAI.KS.W19.DivisionLoop.process_payload_correct line 75
7. theorem OAI.KS.W19.DivisionLoop.advance_quotient_length line 83
8. theorem OAI.KS.W19.DivisionLoop.advance_remainder_length line 89
9. theorem OAI.KS.W19.DivisionLoop.process_quotient_length line 98
10. theorem OAI.KS.W19.DivisionLoop.process_remainder_length line 106