OAI/Analysis/MatrixSigning/Arithmetic/RationalDivisionStages.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W30.RationalDivision.corePorts line 11
  2. def OAI.KS.W30.RationalDivision.«stacks» line 13
  3. def OAI.KS.W30.RationalDivision.liftCore line 15
  4. theorem OAI.KS.W30.RationalDivision.stacks_core line 17
  5. theorem OAI.KS.W30.RationalDivision.stacks_spare_value line 21
  6. theorem OAI.KS.W30.RationalDivision.stacks_spare line 33
  7. theorem OAI.KS.W30.RationalDivision.liftCore_spec line 42
  8. def OAI.KS.W30.RationalDivision.parseNumerator line 48
  9. def OAI.KS.W30.RationalDivision.storeDenominator line 49
  10. def OAI.KS.W30.RationalDivision.serializeNumerator line 50
  11. def OAI.KS.W30.RationalDivision.storeNumerator line 51
  12. def OAI.KS.W30.RationalDivision.restoreDenominator line 52
  13. def OAI.KS.W30.RationalDivision.reciprocal line 53
  14. def OAI.KS.W30.RationalDivision.prepareInverse line 54
  15. def OAI.KS.W30.RationalDivision.prependNumerator line 55
  16. def OAI.KS.W30.RationalDivision.multiply line 56
  17. def OAI.KS.W30.RationalDivision.inputBits line 58
  18. def OAI.KS.W30.RationalDivision.inputState line 60
  19. def OAI.KS.W30.RationalDivision.outputState line 62
  20. theorem OAI.KS.W30.RationalDivision.parseNumerator_spec line 65
  21. theorem OAI.KS.W30.RationalDivision.storeDenominator_spec line 71
  22. def OAI.KS.W30.RationalDivision.serializerTicks line 84
  23. theorem OAI.KS.W30.RationalDivision.serializeNumerator_spec line 87
  24. theorem OAI.KS.W30.RationalDivision.storeNumerator_spec line 94
  25. theorem OAI.KS.W30.RationalDivision.restoreDenominator_spec line 106
  26. theorem OAI.KS.W30.RationalDivision.reciprocal_spec line 117
  27. theorem OAI.KS.W30.RationalDivision.prepareInverse_spec line 124
  28. theorem OAI.KS.W30.RationalDivision.prependNumerator_spec line 136
  29. theorem OAI.KS.W30.RationalDivision.multiply_spec line 146