OAI/Analysis/MatrixSigning/Arithmetic/RationalCompareBranch.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W06.RationalCompare.stayActions line 11
  2. theorem OAI.KS.W06.RationalCompare.branch_spec_left line 13
  3. theorem OAI.KS.W06.RationalCompare.branch_spec_right line 36
  4. def OAI.KS.W06.RationalCompare.signSelect line 59
  5. def OAI.KS.W06.RationalCompare.magnitudeProgram line 63
  6. theorem OAI.KS.W06.RationalCompare.magnitude_spec line 67
  7. def OAI.KS.W06.RationalCompare.signedCrossLE line 83
  8. def OAI.KS.W06.RationalCompare.compareSelect line 88
  9. def OAI.KS.W06.RationalCompare.swapFirstTwo line 95
  10. def OAI.KS.W06.RationalCompare.signedCompareProgram line 97
  11. def OAI.KS.W06.RationalCompare.signedCompareAfter line 103
  12. theorem OAI.KS.W06.RationalCompare.signedCompare_spec line 112
  13. theorem OAI.KS.W06.RationalCompare.signedCompareAfter_output line 159