OAI/Analysis/MatrixSigning/Arithmetic/MultiplicationBody.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W03.MultiplicationBody.registers line 14
  2. def OAI.KS.W03.MultiplicationBody.copyPorts line 17
  3. def OAI.KS.W03.MultiplicationBody.addPorts line 18
  4. def OAI.KS.W03.MultiplicationBody.reversePorts line 19
  5. def OAI.KS.W03.MultiplicationBody.copyProgram line 21
  6. def OAI.KS.W03.MultiplicationBody.addProgram line 23
  7. def OAI.KS.W03.MultiplicationBody.reverseProgram line 25
  8. def OAI.KS.W03.MultiplicationBody.shiftInstruction line 27
  9. def OAI.KS.W03.MultiplicationBody.shiftProgram line 30
  10. def OAI.KS.W03.MultiplicationBody.body line 33
  11. theorem OAI.KS.W03.MultiplicationBody.copy_spec line 36
  12. theorem OAI.KS.W03.MultiplicationBody.add_spec line 46
  13. theorem OAI.KS.W03.MultiplicationBody.reverse_spec line 75
  14. theorem OAI.KS.W03.MultiplicationBody.shift_spec line 99
  15. theorem OAI.KS.W03.MultiplicationBody.body_spec line 115