OAI/Analysis/MatrixSigning/Arithmetic/RationalCompareCorrectness.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W06.RationalCompare.signedFraction line 11
  2. theorem OAI.KS.W06.RationalCompare.fraction_le_iff line 14
  3. theorem OAI.KS.W06.RationalCompare.signedCrossLE_correct line 21
  4. theorem OAI.KS.W06.RationalCompare.magnitude_constructor_value line 40
  5. theorem OAI.KS.W06.RationalCompare.negativeBit_pos line 46
  6. theorem OAI.KS.W06.RationalCompare.signedFraction_num_den line 50
  7. theorem OAI.KS.W06.RationalCompare.canonical_final_output line 59
  8. theorem OAI.KS.W06.RationalCompare.magnitude_length_le line 68
  9. theorem OAI.KS.W06.RationalCompare.product_length_le line 73
  10. theorem OAI.KS.W06.RationalCompare.totalTicks_le_polynomial line 78
  11. theorem OAI.KS.W06.RationalCompare.canonical_comparison_spec line 106
  12. theorem OAI.KS.W06.RationalCompare.output_encoded_rationals line 120
  13. theorem OAI.KS.W06.RationalCompare.halts_encoded_rationals line 135
  14. theorem OAI.KS.W06.RationalCompare.uniform_rational_comparison line 149