OAI/Analysis/MatrixSigning/Machines/SchurCellMachine.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W07.SchurCellMachine.workspace line 14
  2. def OAI.KS.W07.SchurCellMachine.firstPorts line 18
  3. def OAI.KS.W07.SchurCellMachine.extend line 20
  4. theorem OAI.KS.W07.SchurCellMachine.first_spec line 23
  5. def OAI.KS.W07.SchurCellMachine.preparePair line 36
  6. def OAI.KS.W07.SchurCellMachine.pairAfter line 39
  7. theorem OAI.KS.W07.SchurCellMachine.preparePair_spec line 42
  8. def OAI.KS.W07.SchurCellMachine.multiply line 61
  9. def OAI.KS.W07.SchurCellMachine.divide line 63
  10. def OAI.KS.W07.SchurCellMachine.subtract line 65
  11. def OAI.KS.W07.SchurCellMachine.program line 68
  12. def OAI.KS.W07.SchurCellMachine.ticks line 72
  13. theorem OAI.KS.W07.SchurCellMachine.prepare_product_spec line 81
  14. theorem OAI.KS.W07.SchurCellMachine.prepare_division_spec line 91
  15. theorem OAI.KS.W07.SchurCellMachine.prepare_subtraction_spec line 101
  16. theorem OAI.KS.W07.SchurCellMachine.multiply_spec line 111
  17. theorem OAI.KS.W07.SchurCellMachine.divide_spec line 133
  18. theorem OAI.KS.W07.SchurCellMachine.subtract_spec line 152
  19. theorem OAI.KS.W07.SchurCellMachine.full_spec line 167