OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationNormalize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W03.MultiplicationNormalize.reversePorts line 12
2. def OAI.KS.W03.MultiplicationNormalize.trimPorts line 13
3. def OAI.KS.W03.MultiplicationNormalize.reverseProgram line 15
4. def OAI.KS.W03.MultiplicationNormalize.trimProgram line 16
5. def OAI.KS.W03.MultiplicationNormalize.program line 17
6. theorem OAI.KS.W03.MultiplicationNormalize.reverse_spec line 19
7. theorem OAI.KS.W03.MultiplicationNormalize.trim_spec line 44
8. theorem OAI.KS.W03.MultiplicationNormalize.normalize_spec line 69
9. theorem OAI.KS.W03.MultiplicationNormalize.output_port line 76