OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationInitialize.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.MultiplicationInitialize.firstPorts line 13
  2. def OAI.KS.W03.MultiplicationInitialize.secondPorts line 14
  3. def OAI.KS.W03.MultiplicationInitialize.firstProgram line 16
  4. def OAI.KS.W03.MultiplicationInitialize.secondProgram line 17
  5. def OAI.KS.W03.MultiplicationInitialize.program line 18
  6. def OAI.KS.W03.MultiplicationInitialize.inputBits line 20
  7. def OAI.KS.W03.MultiplicationInitialize.ticks line 22
  8. theorem OAI.KS.W03.MultiplicationInitialize.first_spec line 24
  9. theorem OAI.KS.W03.MultiplicationInitialize.second_spec line 48
  10. theorem OAI.KS.W03.MultiplicationInitialize.initialize_spec line 73
  11. theorem OAI.KS.W03.MultiplicationInitialize.input_port line 78
  12. theorem OAI.KS.W03.MultiplicationInitialize.inputBits_length line 80