OAI/Analysis/MatrixSigning/Arithmetic/DivisionOutput.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W19.DivisionOutput.quotientPorts line 11
2. def OAI.KS.W19.DivisionOutput.remainderPorts line 12
3. def OAI.KS.W19.DivisionOutput.pairPorts line 13
4. def OAI.KS.W19.DivisionOutput.canonQ line 14
5. def OAI.KS.W19.DivisionOutput.canonR line 15
6. def OAI.KS.W19.DivisionOutput.emit line 16
7. def OAI.KS.W19.DivisionOutput.tailProgram line 17
8. def OAI.KS.W19.DivisionOutput.program line 18
9. def OAI.KS.W19.DivisionOutput.canonical line 20
10. def OAI.KS.W19.DivisionOutput.pairWire line 21
11. theorem OAI.KS.W19.DivisionOutput.canonical_length line 23
12. theorem OAI.KS.W19.DivisionOutput.quotient_spec line 27
13. theorem OAI.KS.W19.DivisionOutput.remainder_spec line 39
14. theorem OAI.KS.W19.DivisionOutput.emit_spec line 51
15. theorem OAI.KS.W19.DivisionOutput.output_spec line 67
16. theorem OAI.KS.W19.DivisionOutput.read_pair line 77