OAI/Analysis/MatrixSigning/Arithmetic/RationalAddProducts.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W13.RationalAdd.corePorts line 12
  2. def OAI.KS.W13.RationalAdd.extend line 15
  3. theorem OAI.KS.W13.RationalAdd.extend_core line 18
  4. theorem OAI.KS.W13.RationalAdd.extend_13 line 23
  5. theorem OAI.KS.W13.RationalAdd.extend_14 line 24
  6. theorem OAI.KS.W13.RationalAdd.extend_15 line 25
  7. theorem OAI.KS.W13.RationalAdd.core_spec line 27
  8. def OAI.KS.W13.RationalAdd.prepareProgram line 39
  9. def OAI.KS.W13.RationalAdd.inputState line 42
  10. def OAI.KS.W13.RationalAdd.preparedState line 45
  11. theorem OAI.KS.W13.RationalAdd.prepare_spec line 48
  12. def OAI.KS.W13.RationalAdd.leftDenCopyPorts line 55
  13. def OAI.KS.W13.RationalAdd.rightDenCopyPorts line 56
  14. def OAI.KS.W13.RationalAdd.denominatorProductPorts line 57
  15. def OAI.KS.W13.RationalAdd.saveDenominators line 59
  16. def OAI.KS.W13.RationalAdd.savedState line 62
  17. theorem OAI.KS.W13.RationalAdd.saveDenominators_spec line 65
  18. def OAI.KS.W13.RationalAdd.crossProductsProgram line 90
  19. def OAI.KS.W13.RationalAdd.denominatorProductProgram line 93
  20. def OAI.KS.W13.RationalAdd.productsAfter line 96
  21. theorem OAI.KS.W13.RationalAdd.denominatorProduct_spec line 100
  22. def OAI.KS.W13.RationalAdd.productsProgram line 113
  23. def OAI.KS.W13.RationalAdd.productsTicks line 116
  24. theorem OAI.KS.W13.RationalAdd.products_spec line 120
  25. def OAI.KS.W13.RationalAdd.signedState line 128
  26. def OAI.KS.W13.RationalAdd.clearProductsProgram line 131
  27. def OAI.KS.W13.RationalAdd.clearProductsTicks line 135
  28. theorem OAI.KS.W13.RationalAdd.clearProducts_spec line 140