OAI/Analysis/MatrixSigning/Arithmetic/RationalAddSigned.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W13.RationalAdd.readyState line 14
  2. def OAI.KS.W13.RationalAdd.numeratorAt line 17
  3. def OAI.KS.W13.RationalAdd.finishNumeratorProgram line 20
  4. theorem OAI.KS.W13.RationalAdd.finishNumerator_spec line 30
  5. def OAI.KS.W13.RationalAdd.addPorts line 62
  6. def OAI.KS.W13.RationalAdd.rightSubtractPorts line 63
  7. def OAI.KS.W13.RationalAdd.equalProgram line 64
  8. def OAI.KS.W13.RationalAdd.leftLargeProgram line 65
  9. def OAI.KS.W13.RationalAdd.rightLargeProgram line 66
  10. def OAI.KS.W13.RationalAdd.arithmeticBudget line 68
  11. theorem OAI.KS.W13.RationalAdd.equal_spec line 70
  12. theorem OAI.KS.W13.RationalAdd.leftLarge_spec line 84
  13. theorem OAI.KS.W13.RationalAdd.rightLarge_spec line 101
  14. def OAI.KS.W13.RationalAdd.compareLeftCopyPorts line 118
  15. def OAI.KS.W13.RationalAdd.compareRightCopyPorts line 119
  16. def OAI.KS.W13.RationalAdd.comparePorts line 120
  17. def OAI.KS.W13.RationalAdd.copyCompareProgram line 121
  18. def OAI.KS.W13.RationalAdd.comparedState line 125
  19. theorem OAI.KS.W13.RationalAdd.copyCompare_spec line 128
  20. def OAI.KS.W13.RationalAdd.orderedBranch line 149
  21. theorem OAI.KS.W13.RationalAdd.orderedBranch_spec line 154
  22. def OAI.KS.W13.RationalAdd.differentProgram line 182
  23. def OAI.KS.W13.RationalAdd.equalSignSelect line 184
  24. def OAI.KS.W13.RationalAdd.signedProgram line 187
  25. def OAI.KS.W13.RationalAdd.signedBudget line 189
  26. theorem OAI.KS.W13.RationalAdd.signed_spec line 191