diff --git a/float/float_unbounded/double64.pvs b/float/float_unbounded/double64.pvs index 200a296d..4ed22ae9 100644 --- a/float/float_unbounded/double64.pvs +++ b/float/float_unbounded/double64.pvs @@ -30,21 +30,21 @@ BEGIN ;< (x,y) : MACRO bool = Flt?(x,y) ;<=(x,y) : MACRO bool = Fle?(x,y) - ;> (x,y) : MACRO bool = Flt?(x,y) - ;>=(x,y) : MACRO bool = Fle?(x,y) + ;> (x,y) : MACRO bool = Flt?(y,x) + ;>=(x,y) : MACRO bool = Fle?(y,x) r: VAR real ;< (x,r) : MACRO bool = Flt?(x,RtoD(r)) ;<=(x,r) : MACRO bool = Fle?(x,RtoD(r)) - ;> (x,r) : MACRO bool = Flt?(x,RtoD(r)) - ;>=(x,r) : MACRO bool = Fle?(x,RtoD(r)) + ;> (x,r) : MACRO bool = Flt?(RtoD(r),x) + ;>=(x,r) : MACRO bool = Fle?(RtoD(r),x) ;/=(x,r) : MACRO bool = x /= RtoD(r) ;/=(r,y) : MACRO bool = RtoD(r) /= y abs_d64(x) : MACRO double64 = Dabs(x) flr_d64(x) : MACRO double64 = Dfloor(x) - sqt_d64(nnx) : MACRO double64 = Dabs(nnx) + sqt_d64(nnx) : MACRO double64 = Dsqrt(nnx) exp_d64(x) : MACRO double64 = Dexp(x) lgn_d64(px) : MACRO double64 = Dln(px) sin_d64(x) : MACRO double64 = Dsin(x) diff --git a/float/float_unbounded/float32.pvs b/float/float_unbounded/float32.pvs index 716b6ab2..ec0c42c0 100644 --- a/float/float_unbounded/float32.pvs +++ b/float/float_unbounded/float32.pvs @@ -28,20 +28,20 @@ BEGIN ;< (x,y) : MACRO bool = Flt?(x,y) ;<=(x,y) : MACRO bool = Fle?(x,y) - ;> (x,y) : MACRO bool = Flt?(x,y) - ;>=(x,y) : MACRO bool = Fle?(x,y) + ;> (x,y) : MACRO bool = Flt?(y,x) + ;>=(x,y) : MACRO bool = Fle?(y,x) r: VAR real ;< (x,r) : MACRO bool = Flt?(x,RtoS(r)) ;<=(x,r) : MACRO bool = Fle?(x,RtoS(r)) - ;> (x,r) : MACRO bool = Flt?(x,RtoS(r)) - ;>=(x,r) : MACRO bool = Fle?(x,RtoS(r)) + ;> (x,r) : MACRO bool = Flt?(RtoS(r),x) + ;>=(x,r) : MACRO bool = Fle?(RtoS(r),x) abs_f32(x) : float32 = Sabs(x) flr_f32(x) : float32 = Sfloor(x) - sqt_f32(nnx) : float32 = Sabs(nnx) + sqt_f32(nnx) : float32 = Ssqrt(nnx) exp_f32(x) : float32 = Sexp(x) lgn_f32(px) : float32 = Sln(px) diff --git a/summaries/float-float_unbounded.summary b/summaries/float-float_unbounded.summary new file mode 100644 index 00000000..4da9671b --- /dev/null +++ b/summaries/float-float_unbounded.summary @@ -0,0 +1,1245 @@ +*** +*** Processing float/float_unbounded (15:7:26 7/24/2026) +*** Generated by proveit 7.1.0 (Nov 05, 2020) +*** +*** Warning: file roundoff_error_props.pvs is not reachable from top.pvs + Proof summary for theory top + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory float + vNum_TCC1.............................proved - complete [SHOSTAK](0.00 s) + radix_div_vNum........................proved - complete [SHOSTAK](0.00 s) + radix_less_vNum.......................proved - complete [SHOSTAK](0.00 s) + FtoR_TCC1.............................proved - complete [SHOSTAK](0.00 s) + ftor_zero_fnum........................proved - complete [SHOSTAK](0.00 s) + float_int_def.........................proved - complete [SHOSTAK](0.00 s) + Fplus_TCC1............................proved - complete [SHOSTAK](0.00 s) + Fplus_TCC2............................proved - complete [SHOSTAK](0.00 s) + Fplus_TCC3............................proved - complete [SHOSTAK](0.00 s) + Fminus_TCC1...........................proved - complete [SHOSTAK](0.00 s) + sum_float_commutes....................proved - complete [SHOSTAK](0.00 s) + mult_float_commutes...................proved - complete [SHOSTAK](0.00 s) + FexptCorrect_TCC1.....................proved - complete [SHOSTAK](0.00 s) + FexptCorrect..........................proved - complete [SHOSTAK](0.00 s) + sigma_TCC1............................proved - complete [SHOSTAK](0.00 s) + sigma_TCC2............................proved - complete [SHOSTAK](0.00 s) + FDivInt_TCC1..........................proved - complete [SHOSTAK](0.00 s) + FDivInt_def...........................proved - complete [SHOSTAK](0.00 s) + minimum_positive_bounded_value_TCC1...proved - complete [SHOSTAK](0.00 s) + positive_minumum_bounded_closest_to_zero...proved - complete [SHOSTAK](0.00 s) + representability_limits_for_bounded_floats_TCC1...proved - complete [SHOSTAK](0.00 s) + representability_limits_for_bounded_floats_TCC2...proved - complete [SHOSTAK](0.00 s) + representability_limits_for_bounded_floats...proved - complete [SHOSTAK](0.00 s) + hathatln_TCC1.........................proved - incomplete [SHOSTAK](0.00 s) + hathatln_TCC2.........................proved - incomplete [SHOSTAK](0.00 s) + hathatln..............................proved - incomplete [SHOSTAK](0.00 s) + hathat_int_TCC1.......................proved - complete [SHOSTAK](0.00 s) + hathat_int_TCC2.......................proved - complete [SHOSTAK](0.00 s) + hathat_int............................proved - incomplete [SHOSTAK](0.00 s) + Fsucc_TCC1............................proved - complete [SHOSTAK](0.00 s) + Fpred_TCC1............................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC2.......................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC3.......................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC4.......................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC5.......................proved - complete [SHOSTAK](0.00 s) + Fnormalize_TCC6.......................proved - complete [SHOSTAK](0.00 s) + Fulp_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Fulp_posreal_j........................proved - complete [SHOSTAK](0.00 s) + exact_rep_conservation_TCC1...........proved - complete [SHOSTAK](0.00 s) + FoppBounded...........................proved - complete [SHOSTAK](0.00 s) + rounded_opp?_TCC1.....................proved - complete [SHOSTAK](0.00 s) + FcanonicOpp...........................proved - complete [SHOSTAK](0.00 s) + FcanonicBounded.......................proved - complete [SHOSTAK](0.00 s) + canonic_bounded_j.....................proved - complete [SHOSTAK](0.00 s) + FpredCanonic..........................proved - complete [SHOSTAK](0.01 s) + RND_log_compute_TCC1..................proved - complete [SHOSTAK](0.00 s) + RND_log_compute_TCC2..................proved - complete [SHOSTAK](0.00 s) + RND_log_compute_TCC3..................proved - complete [SHOSTAK](0.00 s) + RND_log_compute_TCC4..................proved - complete [SHOSTAK](0.00 s) + RND_log_compute.......................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_TCC2..........................proved - complete [SHOSTAK](0.00 s) + RND_aux_TCC3..........................proved - complete [SHOSTAK](0.00 s) + RND_aux_TCC4..........................proved - complete [SHOSTAK](0.00 s) + RND_aux_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_TCC6..........................proved - incomplete [SHOSTAK](0.02 s) + RND_aux_alt_TCC1......................proved - complete [SHOSTAK](0.00 s) + RND_aux_alt_TCC2......................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_alt_TCC3......................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_alt_def.......................proved - incomplete [SHOSTAK](0.00 s) + RND_Min_TCC1..........................proved - complete [SHOSTAK](0.00 s) + RND_Min_TCC2..........................proved - complete [SHOSTAK](0.00 s) + RND_Min_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + RND_Min_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + RND_Max_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + Exp_incr_1_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Exp_incr_1............................proved - complete [SHOSTAK](0.00 s) + Exp_incr_2............................proved - complete [SHOSTAK](0.00 s) + Exp_increq_1_TCC1.....................proved - complete [SHOSTAK](0.00 s) + Exp_increq_1..........................proved - complete [SHOSTAK](0.00 s) + Exp_increq_2..........................proved - complete [SHOSTAK](0.00 s) + Exp_1.................................proved - complete [SHOSTAK](0.00 s) + EqExpEq...............................proved - complete [SHOSTAK](0.00 s) + expt_odd_TCC1.........................proved - complete [SHOSTAK](0.00 s) + expt_odd..............................proved - complete [SHOSTAK](0.00 s) + expt_even.............................proved - complete [SHOSTAK](0.00 s) + FoppCorrect...........................proved - complete [SHOSTAK](0.00 s) + FoppFopp..............................proved - complete [SHOSTAK](0.00 s) + Fopp_mult_left........................proved - complete [SHOSTAK](0.00 s) + Fopp_mult_right.......................proved - complete [SHOSTAK](0.00 s) + FabsCorrect...........................proved - complete [SHOSTAK](0.00 s) + FplusCorrect..........................proved - complete [SHOSTAK](0.00 s) + FplusAssociative......................proved - complete [SHOSTAK](0.00 s) + FmultAssociative......................proved - complete [SHOSTAK](0.00 s) + FminusCorrect.........................proved - complete [SHOSTAK](0.00 s) + FmultCorrect..........................proved - complete [SHOSTAK](0.00 s) + Fmult_1_r.............................proved - complete [SHOSTAK](0.00 s) + Fmult_1_l.............................proved - complete [SHOSTAK](0.00 s) + Fmult_2_r.............................proved - complete [SHOSTAK](0.00 s) + Fmult_2_l.............................proved - complete [SHOSTAK](0.00 s) + FDivKexpt_TCC1........................proved - complete [SHOSTAK](0.00 s) + FDivKexpt_TCC2........................proved - complete [SHOSTAK](0.00 s) + FDivKexpt_TCC3........................proved - complete [SHOSTAK](0.00 s) + FDivKexpt_def.........................proved - complete [SHOSTAK](0.00 s) + FabsBounded...........................proved - complete [SHOSTAK](0.00 s) + FabsCanonic...........................proved - complete [SHOSTAK](0.00 s) + LeR0Fnum..............................proved - complete [SHOSTAK](0.00 s) + LeFnumZERO............................proved - complete [SHOSTAK](0.00 s) + Lt0RFnum..............................proved - complete [SHOSTAK](0.00 s) + LtZEROFnum............................proved - complete [SHOSTAK](0.00 s) + GtR0Fnum..............................proved - complete [SHOSTAK](0.00 s) + GtFnumZERO............................proved - complete [SHOSTAK](0.00 s) + FleCorrect............................proved - complete [SHOSTAK](0.00 s) + FtoR_monotonic........................proved - complete [SHOSTAK](0.00 s) + rndf_monotone.........................proved - complete [SHOSTAK](0.00 s) + FltCorrect............................proved - complete [SHOSTAK](0.00 s) + Fle_transitive........................proved - complete [SHOSTAK](0.00 s) + Flt_transitive........................proved - complete [SHOSTAK](0.00 s) + Fle_neg_Flt...........................proved - complete [SHOSTAK](0.00 s) + Flt_Fle_Flt...........................proved - complete [SHOSTAK](0.00 s) + FminCorrect...........................proved - complete [SHOSTAK](0.00 s) + FmaxCorrect...........................proved - complete [SHOSTAK](0.00 s) + FsubnormalUnique......................proved - complete [SHOSTAK](0.00 s) + FnormalUnique.........................proved - complete [SHOSTAK](0.01 s) + NormalAndSubNormalNotEq...............proved - complete [SHOSTAK](0.00 s) + FcanonicUnique........................proved - complete [SHOSTAK](0.00 s) + Fle_definition........................proved - complete [SHOSTAK](0.00 s) + FnormalizeCorrect.....................proved - complete [SHOSTAK](0.00 s) + FnormalizeCanonicFnum_TCC1............proved - complete [SHOSTAK](0.00 s) + FnormalizeCanonicFnum.................proved - complete [SHOSTAK](0.00 s) + FulpCanonic...........................proved - complete [SHOSTAK](0.00 s) + Fulp_min..............................proved - complete [SHOSTAK](0.00 s) + Lexico................................proved - complete [SHOSTAK](0.01 s) + CanonicLeastExp.......................proved - complete [SHOSTAK](0.00 s) + Fast_canonic..........................proved - complete [SHOSTAK](0.00 s) + FulpOpp_TCC1..........................proved - complete [SHOSTAK](0.00 s) + FulpOpp...............................proved - complete [SHOSTAK](0.00 s) + FulpAbs_TCC1..........................proved - complete [SHOSTAK](0.00 s) + FulpAbs...............................proved - complete [SHOSTAK](0.00 s) + FulpMonotone..........................proved - complete [SHOSTAK](0.00 s) + FulpMonotoneAbs.......................proved - complete [SHOSTAK](0.00 s) + FloatPlusUlpBounded...................proved - complete [SHOSTAK](0.00 s) + FloatMinusUlpBounded..................proved - complete [SHOSTAK](0.00 s) + FpredFoppFsucc........................proved - complete [SHOSTAK](0.00 s) + FsuccFoppFpred........................proved - complete [SHOSTAK](0.00 s) + FsuccFpred............................proved - complete [SHOSTAK](0.00 s) + FpredFsucc............................proved - complete [SHOSTAK](0.00 s) + FpredBounded..........................proved - complete [SHOSTAK](0.00 s) + FsuccBounded..........................proved - complete [SHOSTAK](0.00 s) + FsuccCanonic..........................proved - complete [SHOSTAK](0.00 s) + FpredPos..............................proved - complete [SHOSTAK](0.00 s) + FsuccPos..............................proved - complete [SHOSTAK](0.00 s) + FpredDiff_TCC1........................proved - complete [SHOSTAK](0.00 s) + FpredDiff.............................proved - complete [SHOSTAK](0.00 s) + FsuccDiff.............................proved - complete [SHOSTAK](0.00 s) + FpredLt...............................proved - complete [SHOSTAK](0.00 s) + FpredLe_aux...........................proved - complete [SHOSTAK](0.04 s) + FpredLe_aux2..........................proved - complete [SHOSTAK](0.00 s) + FpredLe...............................proved - complete [SHOSTAK](0.00 s) + FsuccLe...............................proved - complete [SHOSTAK](0.00 s) + FpredProp_aux.........................proved - complete [SHOSTAK](0.01 s) + FpredProp.............................proved - complete [SHOSTAK](0.00 s) + FsuccLt...............................proved - complete [SHOSTAK](0.00 s) + FsuccProp.............................proved - complete [SHOSTAK](0.00 s) + FsuccZleEq_aux........................proved - complete [SHOSTAK](0.00 s) + FsuccZleEq............................proved - complete [SHOSTAK](0.01 s) + EvenFsuccOdd_aux_TCC1.................proved - complete [SHOSTAK](0.00 s) + EvenFsuccOdd_aux......................proved - complete [SHOSTAK](0.00 s) + EvenFsuccOdd..........................proved - complete [SHOSTAK](0.00 s) + OddFsuccEven_aux_TCC1.................proved - complete [SHOSTAK](0.00 s) + OddFsuccEven_aux......................proved - complete [SHOSTAK](0.00 s) + OddFsuccEven..........................proved - complete [SHOSTAK](0.00 s) + MinOppMax.............................proved - complete [SHOSTAK](0.00 s) + MaxOppMin.............................proved - complete [SHOSTAK](0.00 s) + ToZeroFopp............................proved - complete [SHOSTAK](0.00 s) + ClosestFopp...........................proved - complete [SHOSTAK](0.00 s) + EvenClosestFopp_TCC1..................proved - complete [SHOSTAK](0.00 s) + EvenClosestFopp.......................proved - complete [SHOSTAK](0.00 s) + RleRoundedR0..........................proved - complete [SHOSTAK](0.00 s) + rle_rounded_r0........................proved - complete [SHOSTAK](0.00 s) + RleRoundedLessR0......................proved - complete [SHOSTAK](0.00 s) + ulp_generic_monotone..................proved - complete [SHOSTAK](0.00 s) + RND_aux_le............................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_ge............................proved - incomplete [SHOSTAK](0.01 s) + RND_Min_isMin.........................proved - incomplete [SHOSTAK](0.00 s) + RND_Max_isMax.........................proved - incomplete [SHOSTAK](0.00 s) + RND_ToZero_ToZero.....................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_float_TCC1....................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_TCC2....................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_TCC3....................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_TCC4....................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_TCC5....................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_TCC6....................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_float_TCC7....................proved - incomplete [SHOSTAK](0.00 s) + RND_aux_float_def_TCC1................proved - complete [SHOSTAK](0.00 s) + RND_aux_float_def.....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_TCC1....................proved - complete [SHOSTAK](0.00 s) + RND_float_Min_TCC2....................proved - complete [SHOSTAK](0.00 s) + RND_float_Min_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_TCC4....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_def.....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_def.....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_ge_canonic..............proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_le_canonic..............proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_canonic.................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_canonic.................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_ge......................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_le......................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_ge......................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_le......................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_lt_canonic..............proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_gt_canonic..............proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_ge_0....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Min_lt_0....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_le_0....................proved - incomplete [SHOSTAK](0.00 s) + RND_float_Max_gt_0....................proved - incomplete [SHOSTAK](0.00 s) + Fmult_canonic_id_Min_TCC1.............proved - complete [SHOSTAK](0.00 s) + Fmult_canonic_id_Min..................proved - incomplete [SHOSTAK](0.00 s) + Fmult_canonic_id_Max..................proved - incomplete [SHOSTAK](0.00 s) + Fplus_canonic_id_Min_TCC1.............proved - complete [SHOSTAK](0.00 s) + Fplus_canonic_id_Min..................proved - incomplete [SHOSTAK](0.00 s) + Fplus_canonic_id_Max..................proved - incomplete [SHOSTAK](0.00 s) + MaxSuccMin_TCC1.......................proved - complete [SHOSTAK](0.00 s) + MaxSuccMin............................proved - complete [SHOSTAK](0.00 s) + LeMinMaxClosest.......................proved - complete [SHOSTAK](0.01 s) + isMin_Total...........................proved - incomplete [SHOSTAK](0.00 s) + isMin_Compatible......................proved - complete [SHOSTAK](0.00 s) + isMin_Monotone........................proved - complete [SHOSTAK](0.00 s) + isMin_RoundedMode.....................proved - incomplete [SHOSTAK](0.00 s) + isMin_Unique..........................proved - complete [SHOSTAK](0.00 s) + isMax_Total...........................proved - incomplete [SHOSTAK](0.00 s) + isMax_Compatible......................proved - complete [SHOSTAK](0.00 s) + isMax_Monotone........................proved - complete [SHOSTAK](0.00 s) + isMax_RoundedMode.....................proved - incomplete [SHOSTAK](0.00 s) + isMax_Unique..........................proved - complete [SHOSTAK](0.00 s) + ToZero_Total..........................proved - incomplete [SHOSTAK](0.00 s) + ToZero_Compatible.....................proved - complete [SHOSTAK](0.00 s) + ToZero_MinOrMax.......................proved - complete [SHOSTAK](0.00 s) + ToZero_Monotone.......................proved - complete [SHOSTAK](0.00 s) + ToZero_RoundedMode....................proved - incomplete [SHOSTAK](0.00 s) + ToZero_Unique.........................proved - complete [SHOSTAK](0.00 s) + Closest_Total.........................proved - incomplete [SHOSTAK](0.00 s) + Closest_total.........................proved - incomplete [SHOSTAK](0.00 s) + Closest_Compatible....................proved - complete [SHOSTAK](0.00 s) + Closest_compatible....................proved - complete [SHOSTAK](0.00 s) + Closest_MinOrMax......................proved - complete [SHOSTAK](0.00 s) + Closest_min_or_max....................proved - complete [SHOSTAK](0.00 s) + Closest_Monotone......................proved - complete [SHOSTAK](0.00 s) + Closest_monotone......................proved - complete [SHOSTAK](0.00 s) + Closest_RoundedMode...................proved - incomplete [SHOSTAK](0.00 s) + Closest_rounded_mode..................proved - incomplete [SHOSTAK](0.00 s) + RND_EClosest_isEclosest...............proved - incomplete [SHOSTAK](0.00 s) + Closest_bounded_exact_rep_TCC1........proved - incomplete [SHOSTAK](0.00 s) + Closest_bounded_exact_rep.............proved - incomplete [SHOSTAK](0.00 s) + ClosestRtoF_exact_rep_conv............proved - incomplete [SHOSTAK](0.00 s) + Closest_int_exact_rep.................proved - incomplete [SHOSTAK](0.00 s) + ClosestRNDF_FtoR_inverse..............proved - complete [SHOSTAK](0.00 s) + EvenClosest_Total.....................proved - incomplete [SHOSTAK](0.00 s) + EvenClosest_total.....................proved - incomplete [SHOSTAK](0.00 s) + EvenClosest_Compatible................proved - complete [SHOSTAK](0.00 s) + EvenClosest_compatible................proved - complete [SHOSTAK](0.00 s) + EvenClosest_MinOrMax..................proved - complete [SHOSTAK](0.00 s) + EvenClosest_min_or_max................proved - complete [SHOSTAK](0.00 s) + EvenClosest_Monotone..................proved - complete [SHOSTAK](0.00 s) + EvenClosest_monotone..................proved - complete [SHOSTAK](0.00 s) + EvenClosest_RoundedMode...............proved - incomplete [SHOSTAK](0.00 s) + EvenClosest_rounded_mode..............proved - incomplete [SHOSTAK](0.00 s) + EvenClosest_Unique....................proved - complete [SHOSTAK](0.00 s) + AFZClosest_Total......................proved - incomplete [SHOSTAK](0.00 s) + AFZClosest_Compatible.................proved - complete [SHOSTAK](0.00 s) + AFZClosest_MinOrMax...................proved - complete [SHOSTAK](0.00 s) + AFZClosest_Monotone...................proved - complete [SHOSTAK](0.00 s) + AFZClosest_RoundedMode................proved - incomplete [SHOSTAK](0.00 s) + AFZClosest_Unique.....................proved - incomplete [SHOSTAK](0.00 s) + RoundedProjectorEq....................proved - complete [SHOSTAK](0.00 s) + RoundedProjector......................proved - complete [SHOSTAK](0.00 s) + isMin_Rep.............................proved - complete [SHOSTAK](0.00 s) + RoundedModeRep........................proved - complete [SHOSTAK](0.00 s) + RoundedModeUlp........................proved - complete [SHOSTAK](0.00 s) + rnd_tozero_is_tozero?_j...............proved - incomplete [SHOSTAK](0.00 s) + ulp_monotone..........................proved - incomplete [SHOSTAK](0.00 s) + ClosestUlp............................proved - incomplete [SHOSTAK](0.00 s) + away_to_closest_by_half_to_nearest_ulp...proved - incomplete [SHOSTAK](0.00 s) + min_is_max_for_floats.................proved - incomplete [SHOSTAK](0.00 s) + min_is_max_implies_ftor...............proved - incomplete [SHOSTAK](0.00 s) + RoundedModeNonDecreasing..............proved - complete [SHOSTAK](0.00 s) + ClosestUlp2_TCC1......................proved - complete [SHOSTAK](0.00 s) + ClosestUlp2...........................proved - incomplete [SHOSTAK](0.00 s) + ClosestFabs...........................proved - incomplete [SHOSTAK](0.00 s) + SterbenzAux...........................proved - complete [SHOSTAK](0.00 s) + Sterbenz..............................proved - complete [SHOSTAK](0.00 s) + errorBoundedPlus......................proved - incomplete [SHOSTAK](0.00 s) + errorBoundedMult_aux..................proved - incomplete [SHOSTAK](0.01 s) + errorBoundedMult_aux2.................proved - incomplete [SHOSTAK](0.01 s) + errorBoundedMult......................proved - incomplete [SHOSTAK](0.00 s) + FulpLeN_TCC1..........................proved - complete [SHOSTAK](0.00 s) + FulpLeN...............................proved - complete [SHOSTAK](0.00 s) + FulpGe_TCC1...........................proved - complete [SHOSTAK](0.00 s) + FulpGe................................proved - complete [SHOSTAK](0.00 s) + FulpLe................................proved - complete [SHOSTAK](0.00 s) + FulpFpred1_TCC1.......................proved - complete [SHOSTAK](0.00 s) + FulpFpred1............................proved - complete [SHOSTAK](0.00 s) + FulpFpred2............................proved - complete [SHOSTAK](0.00 s) + Fopp_RtoF_TCC1........................proved - complete [SHOSTAK](0.00 s) + Fopp_RtoF.............................proved - complete [SHOSTAK](0.00 s) + ulp_abs...............................proved - incomplete [SHOSTAK](0.00 s) + injrnd_ulp............................proved - complete [SHOSTAK](0.00 s) + Fulp_ulp..............................proved - complete [SHOSTAK](0.00 s) + rndmaxismax_j.........................proved - incomplete [SHOSTAK](0.00 s) + rndminismin_j.........................proved - incomplete [SHOSTAK](0.00 s) + rndeclosest_j.........................proved - incomplete [SHOSTAK](0.00 s) + closest_ulp_pos.......................proved - incomplete [SHOSTAK](0.00 s) + closest_ulp...........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 305 formulas, 305 attempted, 305 succeeded (0.28 s) + + Proof summary for theory axpy + FcanonicBounded2......................proved - complete [SHOSTAK](0.00 s) + MinOrMax_Rlt..........................proved - incomplete [SHOSTAK](0.00 s) + MinOrMax_Fopp_TCC1....................proved - complete [SHOSTAK](0.00 s) + MinOrMax_Fopp.........................proved - complete [SHOSTAK](0.00 s) + MinOrMax1_TCC1........................proved - complete [SHOSTAK](0.00 s) + MinOrMax1_TCC2........................proved - complete [SHOSTAK](0.00 s) + MinOrMax1.............................proved - complete [SHOSTAK](0.00 s) + MinOrMax2_TCC1........................proved - complete [SHOSTAK](0.00 s) + MinOrMax2.............................proved - complete [SHOSTAK](0.00 s) + MinOrMax3_TCC1........................proved - complete [SHOSTAK](0.00 s) + MinOrMax3.............................proved - complete [SHOSTAK](0.00 s) + RoundLe_TCC1..........................proved - complete [SHOSTAK](0.00 s) + RoundLe_TCC2..........................proved - complete [SHOSTAK](0.00 s) + RoundLe_TCC3..........................proved - complete [SHOSTAK](0.00 s) + RoundLe...............................proved - incomplete [SHOSTAK](0.01 s) + RoundGe_TCC1..........................proved - complete [SHOSTAK](0.00 s) + RoundGe...............................proved - incomplete [SHOSTAK](0.01 s) + ExactSum_Near_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + ExactSum_Near.........................proved - incomplete [SHOSTAK](0.00 s) + Normal_iff_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Normal_iff............................proved - complete [SHOSTAK](0.00 s) + Axpy_aux1_TCC1........................proved - complete [SHOSTAK](0.00 s) + Axpy_aux1.............................proved - incomplete [SHOSTAK](0.00 s) + Axpy_aux1_aux1........................proved - incomplete [SHOSTAK](0.00 s) + Axpy_aux1_aux2........................proved - incomplete [SHOSTAK](0.00 s) + Axpy_aux2.............................proved - incomplete [SHOSTAK](0.00 s) + Axpy_aux3.............................proved - incomplete [SHOSTAK](0.01 s) + AxpyPos...............................proved - incomplete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1_TCC1...............proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1_TCC2...............proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1_TCC3...............proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1_TCC4...............proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1_TCC5...............proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1_aux1....................proved - complete [SHOSTAK](0.03 s) + Axpy_opt_aux1_TCC1....................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux1.........................proved - incomplete [SHOSTAK](0.02 s) + Axpy_opt_aux2_TCC1....................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux2_TCC2....................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux2.........................proved - incomplete [SHOSTAK](0.08 s) + Axpy_opt_aux3_TCC1....................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux3_TCC2....................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_aux3.........................proved - incomplete [SHOSTAK](0.03 s) + Axpy_optPos_TCC1......................proved - complete [SHOSTAK](0.00 s) + Axpy_optPos_TCC2......................proved - complete [SHOSTAK](0.00 s) + Axpy_optPos...........................proved - incomplete [SHOSTAK](0.00 s) + Axpy_optZero_TCC1.....................proved - complete [SHOSTAK](0.00 s) + Axpy_optZero_TCC2.....................proved - complete [SHOSTAK](0.00 s) + Axpy_optZero..........................proved - incomplete [SHOSTAK](0.01 s) + Axpy_opt_TCC1.........................proved - complete [SHOSTAK](0.00 s) + Axpy_opt_TCC2.........................proved - complete [SHOSTAK](0.00 s) + Axpy_opt..............................proved - incomplete [SHOSTAK](0.00 s) + Axpy_simpl............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 52 formulas, 52 attempted, 52 succeeded (0.23 s) + + Proof summary for theory float_props_rounding + exp_bound_TCC1........................proved - complete [SHOSTAK](0.00 s) + exp_bound.............................proved - incomplete [SHOSTAK](0.00 s) + closestrounding_preserves_fplowerbound...proved - complete [SHOSTAK](0.00 s) + rep_exp_bound_TCC1....................proved - complete [SHOSTAK](0.00 s) + rep_exp_bound.........................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_closest_rounding..........proved - complete [SHOSTAK](0.00 s) + unique_zero_RND_aux...................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RND_Min...................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RND_Max...................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RND_EClosest..............proved - incomplete [SHOSTAK](0.00 s) + closest?_ucf__j.......................proved - incomplete [SHOSTAK](0.00 s) + rnd_eclosest_is_particuLar_closest....proved - incomplete [SHOSTAK](0.00 s) + rnd_ucf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + rnd_prj_ucf...........................proved - incomplete [SHOSTAK](0.00 s) + rnd_opp_ucf...........................proved - incomplete [SHOSTAK](0.00 s) + rnd_ucf_monotonic.....................proved - incomplete [SHOSTAK](0.00 s) + rnc_ucf_increasing....................proved - incomplete [SHOSTAK](0.00 s) + rnd_ucf_is_canonic_rounding_closest_ucf_...proved - incomplete [SHOSTAK](0.00 s) + rnd_ucf_is_canonic_rounding_closest_ucf...proved - incomplete [SHOSTAK](0.00 s) + prj_rnd_ucf_ints......................proved - incomplete [SHOSTAK](0.00 s) + prj_rnd_ucf_zero......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 21 formulas, 21 attempted, 21 succeeded (0.01 s) + + Proof summary for theory unop_em_scheme + Fg_TCC1...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC2...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC3...............................proved - complete [SHOSTAK](0.00 s) + Fg_bounded............................proved - complete [SHOSTAK](0.00 s) + Fg_error..............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory binop_em_scheme + Fg_TCC1...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC2...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC3...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC4...............................proved - complete [SHOSTAK](0.00 s) + Fg_TCC5...............................proved - complete [SHOSTAK](0.00 s) + Fg_bounded............................proved - complete [SHOSTAK](0.00 s) + Fg_error..............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory cr_add + Fadd_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fadd_error............................proved - incomplete [SHOSTAK](0.00 s) + Fadd_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory cr_sub + Fsub_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fsub_error............................proved - incomplete [SHOSTAK](0.00 s) + Fsub_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory std_mul + Fmul_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fmul_error............................proved - incomplete [SHOSTAK](0.00 s) + Fmul_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Fmul_commutative......................proved - complete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory std_mul_props + Fmul_radix_power_error_ulp_TCC1.......proved - complete [SHOSTAK](0.00 s) + Fmul_radix_power_error_ulp............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory cr_div + Fdiv_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Fdiv_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fdiv_error_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Fdiv_error............................proved - incomplete [SHOSTAK](0.00 s) + Fdiv_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory cr_exp + IMP_binop_em_scheme_TCC1..............proved - complete [SHOSTAK](0.00 s) + Fexp_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Fexp_TCC2.............................proved - complete [SHOSTAK](0.00 s) + Fexp_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fexp_error_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Fexp_error............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory cr_mod + IMP_binop_em_scheme_TCC1..............proved - complete [SHOSTAK](0.00 s) + Fmod_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Fmod_TCC2.............................proved - complete [SHOSTAK](0.00 s) + Fmod_bounded..........................proved - incomplete [SHOSTAK](0.00 s) + Fmod_error_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Fmod_error............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory cr_neg + Fneg_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fneg_error............................proved - incomplete [SHOSTAK](0.00 s) + Fneg_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Fneg_exact............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory cr_flr + Ffloor_bounded........................proved - complete [SHOSTAK](0.00 s) + Ffloor_no_rounding_error..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory cr_sqt + Fsqrt_TCC1............................proved - complete [SHOSTAK](0.00 s) + Fsqrt_bounded.........................proved - incomplete [SHOSTAK](0.00 s) + Fsqrt_error_TCC1......................proved - complete [SHOSTAK](0.00 s) + Fsqrt_error...........................proved - incomplete [SHOSTAK](0.00 s) + Fsqrt_error_ulp.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory cr_sin + Fsin_bounded..........................proved - incomplete [SHOSTAK](0.00 s) + Fsin_error............................proved - incomplete [SHOSTAK](0.00 s) + Fsin_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory cr_abs + Fabs_bounded..........................proved - complete [SHOSTAK](0.00 s) + Fabs_exact............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory std_cos + Fcos_bounded..........................proved - incomplete [SHOSTAK](0.00 s) + Fcos_error............................proved - incomplete [SHOSTAK](0.00 s) + Fcos_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory std_atn + Fatn_bounded..........................proved - incomplete [SHOSTAK](0.00 s) + Fatn_error............................proved - incomplete [SHOSTAK](0.00 s) + Fatn_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory std_exp + Fexp_bounded..........................proved - incomplete [SHOSTAK](0.00 s) + Fexp_error............................proved - incomplete [SHOSTAK](0.00 s) + Fexp_error_ulp........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory accum_err_op2sch + accumulated_error.....................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory accum_err_op1sch + accumulated_error.....................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory accum_err_exact_op2sch + accumulated_error.....................proved - complete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory accum_err_op1sch_exact + accumulated_error.....................proved - complete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory accum_err_neg + neg_accum_err.........................proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_neg_TCC1..............proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_neg_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + accum_err_neg.........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory accum_err_abs + abs_accum_err.........................proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_abs_TCC1..............proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_abs_TCC2..............proved - incomplete [SHOSTAK](0.00 s) + accum_err_abs.........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory accum_err_add + add_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fadd_accum_err_bound..................proved - complete [SHOSTAK](0.00 s) + aelemmath_add_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_add_TCC2....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_add_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_add_TCC4....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_add_TCC5....................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory accum_err_sub + sub_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fsub_accum_err_bound..................proved - complete [SHOSTAK](0.00 s) + aelemmath_sub_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_sub_TCC2....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_sub_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_sub_TCC4....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_sub_TCC5....................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory accum_err_mul + mul_accum_err.........................proved - complete [SHOSTAK](0.00 s) + Fmul_accum_err_bound..................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_mul_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_mul_TCC2....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_mul_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_mul_TCC4....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_mul_TCC5....................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory aerr_mul_props + IMP_accum_err_mul_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_mul_TCC2................proved - complete [SHOSTAK](0.00 s) + power_of_radix_left_mult_pre_r_TCC1...proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_mul_l_TCC1............proved - complete [SHOSTAK](0.00 s) + aelemmath_exact_mul_l_TCC2............proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound_exact_l...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory accum_err_div + div_aerr_bound_TCC1...................proved - complete [SHOSTAK](0.00 s) + div_aerr_bound_TCC2...................proved - complete [SHOSTAK](0.00 s) + div_accum_err_TCC1....................proved - complete [SHOSTAK](0.00 s) + div_accum_err_TCC2....................proved - complete [SHOSTAK](0.00 s) + div_accum_err_TCC3....................proved - complete [SHOSTAK](0.00 s) + div_accum_err.........................proved - complete [SHOSTAK](0.01 s) + div_ulp_bound_TCC1....................proved - complete [SHOSTAK](0.00 s) + Fdiv_accum_err_bound..................proved - complete [SHOSTAK](0.00 s) + aelemmath_div_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_div_TCC2....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_div_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_div_TCC4....................proved - incomplete [SHOSTAK](0.00 s) + aelemmath_div_TCC5....................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.01 s) + + Proof summary for theory accum_err_sqt + sqrt_accum_err........................proved - incomplete [SHOSTAK](0.00 s) + sqt_ulp_bound_TCC1....................proved - complete [SHOSTAK](0.00 s) + Fsqrt_accum_err_bound.................proved - incomplete [SHOSTAK](0.00 s) + sqt_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_prf_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_prf_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_prf_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.00 s) + + Proof summary for theory accum_err_flr + floor_accum_err.......................proved - incomplete [SHOSTAK](0.00 s) + flr_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + flr_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory accum_err_flr_t + floor_accum_err.......................proved - incomplete [SHOSTAK](0.00 s) + flr_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + flr_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory accum_err_sin + sin_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fsin_accum_err_bound..................proved - incomplete [SHOSTAK](0.00 s) + sin_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + sin_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + sin_prf_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + sin_prf_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + sin_prf_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory trig_fp_bounds + IMP_derivative_props_TCC1.............proved - complete [SHOSTAK](0.00 s) + IMP_derivative_props_TCC2.............proved - complete [SHOSTAK](0.00 s) + sin_error_prep........................proved - incomplete [SHOSTAK](0.01 s) + cos_error_prep........................proved - incomplete [SHOSTAK](0.00 s) + sin_bound_TCC1........................proved - complete [SHOSTAK](0.00 s) + sin_bound_TCC2........................proved - complete [SHOSTAK](0.00 s) + sin_bound_TCC3........................proved - complete [SHOSTAK](0.00 s) + sin_bound_TCC4........................proved - complete [SHOSTAK](0.00 s) + sin_bound.............................proved - incomplete [SHOSTAK](0.00 s) + sin_error_bound_TCC1..................proved - complete [SHOSTAK](0.00 s) + sin_error_bound_TCC2..................proved - complete [SHOSTAK](0.00 s) + sin_error_bound_TCC3..................proved - complete [SHOSTAK](0.00 s) + sin_error_bound_TCC4..................proved - complete [SHOSTAK](0.00 s) + sin_error_bound.......................proved - incomplete [SHOSTAK](0.00 s) + cos_error_bound.......................proved - incomplete [SHOSTAK](0.00 s) + sin_bnd_simple........................proved - incomplete [SHOSTAK](0.00 s) + cos_bnd_simple........................proved - incomplete [SHOSTAK](0.00 s) + sin_error_eps.........................proved - incomplete [SHOSTAK](0.00 s) + cos_error_eps.........................proved - incomplete [SHOSTAK](0.00 s) + atan_error_eps_TCC1...................proved - complete [SHOSTAK](0.00 s) + atan_error_eps_TCC2...................proved - complete [SHOSTAK](0.00 s) + atan_error_eps_TCC3...................proved - incomplete [SHOSTAK](0.00 s) + atan_error_eps........................proved - incomplete [SHOSTAK](0.01 s) + generic_bounding......................proved - complete [SHOSTAK](0.00 s) + sin_ulp_bounded.......................proved - incomplete [SHOSTAK](0.00 s) + cos_ulp_bounded.......................proved - incomplete [SHOSTAK](0.00 s) + atan_ulp_bounded......................proved - incomplete [SHOSTAK](0.00 s) + div_ulp_TCC1..........................proved - complete [SHOSTAK](0.00 s) + div_ulp_TCC2..........................proved - complete [SHOSTAK](0.00 s) + div_ulp...............................proved - complete [SHOSTAK](0.00 s) + sqrt_ulp_TCC1.........................proved - complete [SHOSTAK](0.00 s) + sqrt_ulp..............................proved - incomplete [SHOSTAK](0.00 s) + atan_ulp..............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 33 formulas, 33 attempted, 33 succeeded (0.03 s) + + Proof summary for theory accum_err_cos + cos_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fcos_accum_err_bound..................proved - incomplete [SHOSTAK](0.00 s) + cos_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + cos_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + cos_prf_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + cos_prf_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + cos_prf_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory accum_err_atn + atn_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fatn_accum_err_bound..................proved - incomplete [SHOSTAK](0.00 s) + atn_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + atn_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + atn_prf_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + atn_prf_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + atn_prf_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + atn_t_aerr_bound_TCC1.................proved - incomplete [SHOSTAK](0.00 s) + atn_t_aerr_bound_TCC2.................proved - incomplete [SHOSTAK](0.00 s) + atn_t_aerr_bound_TCC3.................proved - incomplete [SHOSTAK](0.00 s) + atn_t_aerr_bound_TCC4.................proved - incomplete [SHOSTAK](0.00 s) + atn_t_accum_err.......................proved - incomplete [SHOSTAK](0.00 s) + atn_t_prf_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound_t.....................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.01 s) + + Proof summary for theory accum_err_exp + exp_aerr_bound_TCC1...................proved - incomplete [SHOSTAK](0.00 s) + exp_accum_err.........................proved - incomplete [SHOSTAK](0.00 s) + Fexp_accum_err_bound..................proved - incomplete [SHOSTAK](0.00 s) + exp_prf_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + exp_prf_TCC2..........................proved - incomplete [SHOSTAK](0.00 s) + exp_prf_TCC3..........................proved - incomplete [SHOSTAK](0.00 s) + exp_prf_TCC4..........................proved - incomplete [SHOSTAK](0.00 s) + exp_prf_TCC5..........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.00 s) + + Proof summary for theory ieee754sp + IMP_float_TCC1........................proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC1.........proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC2.........proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC3.........proved - complete [SHOSTAK](0.00 s) + single_precision_format_TCC1..........proved - complete [SHOSTAK](0.00 s) + sp_closest?_j.........................proved - incomplete [SHOSTAK](0.00 s) + sp_closest?_closestroundingpred_j.....proved - complete [SHOSTAK](0.00 s) + RtoS_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + RtoS_closest_single...................proved - incomplete [SHOSTAK](0.00 s) + rtos_canonicroundfun_exactrepconservation_j...proved - incomplete [SHOSTAK](0.00 s) + rtos_monotonic........................proved - incomplete [SHOSTAK](0.00 s) + neq_lt_rew............................proved - complete [SHOSTAK](0.01 s) + noteq_rew_rl1.........................proved - complete [SHOSTAK](0.00 s) + noteq_rew_rl2.........................proved - complete [SHOSTAK](0.00 s) + noteq_rew.............................proved - complete [SHOSTAK](0.00 s) + neq_rew...............................proved - complete [SHOSTAK](0.00 s) + leq_def...............................proved - complete [SHOSTAK](0.00 s) + Sulp_def..............................proved - complete [SHOSTAK](0.00 s) + StoR_round............................proved - incomplete [SHOSTAK](0.00 s) + StoR_RtoS.............................proved - incomplete [SHOSTAK](0.00 s) + StoR_RtoS_int_exactly_representable...proved - incomplete [SHOSTAK](0.00 s) + RtoS_StoR.............................proved - incomplete [SHOSTAK](0.00 s) + StoR_ext..............................proved - complete [SHOSTAK](0.00 s) + StoR_strictly_increasing..............proved - complete [SHOSTAK](0.00 s) + StoR_inc..............................proved - complete [SHOSTAK](0.00 s) + RtoS_inc..............................proved - incomplete [SHOSTAK](0.00 s) + RtoS_opp..............................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RtoS_TCC1.................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RtoS......................proved - incomplete [SHOSTAK](0.00 s) + sp_rep_exp_bound......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 30 formulas, 30 attempted, 30 succeeded (0.01 s) + + Proof summary for theory ieee754sp_add + IMP_cr_add_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sadd_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Sadd_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_sub + IMP_cr_sub_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Ssub_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Ssub_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_mul + IMP_std_mul_TCC1......................proved - complete [SHOSTAK](0.00 s) + Smul_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Smul_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Smul_commutative......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory ieee754sp_div + IMP_cr_div_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sdiv_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Sdiv_TCC2.............................proved - incomplete [SHOSTAK](0.00 s) + Sdiv_correctly_rounded_TCC1...........proved - complete [SHOSTAK](0.00 s) + Sdiv_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory ieee754sp_sqt + IMP_cr_sqt_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Ssqrt_TCC1............................proved - complete [SHOSTAK](0.00 s) + Ssqrt_TCC2............................proved - incomplete [SHOSTAK](0.00 s) + Ssqrt_correctly_rounded_TCC1..........proved - complete [SHOSTAK](0.00 s) + Ssqrt_correctly_rounded...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory ieee754sp_flr + IMP_cr_flr_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sfloor_TCC1...........................proved - incomplete [SHOSTAK](0.00 s) + Sfloor_correctly_rounded..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_neg + IMP_cr_neg_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sneg_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Sneg_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_abs + IMP_cr_abs_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sabs_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Sabs_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_mod + IMP_cr_mod_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Smod_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Smod_TCC2.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_sin + IMP_cr_sin_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Ssin_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Ssin_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_cos + IMP_std_cos_TCC1......................proved - complete [SHOSTAK](0.00 s) + Scos_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Scos_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_atn + IMP_std_atn_TCC1......................proved - complete [SHOSTAK](0.00 s) + Satan_TCC1............................proved - incomplete [SHOSTAK](0.00 s) + Satan_correctly_rounded...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_exp + IMP_std_exp_TCC1......................proved - complete [SHOSTAK](0.00 s) + Sexp_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Sexp_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754sp_ln + IMP_std_ln_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Sln_TCC1..............................proved - complete [SHOSTAK](0.00 s) + Sln_TCC2..............................proved - complete [SHOSTAK](0.00 s) + Sln_TCC3..............................proved - incomplete [SHOSTAK](0.00 s) + Sln_correctly_rounded_TCC1............proved - complete [SHOSTAK](0.00 s) + Sln_correctly_rounded_TCC2............proved - complete [SHOSTAK](0.00 s) + Sln_correctly_rounded.................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory std_ln + IMP_unop_em_scheme_TCC1...............proved - complete [SHOSTAK](0.00 s) + Fln_TCC1..............................proved - complete [SHOSTAK](0.00 s) + Fln_bounded...........................proved - incomplete [SHOSTAK](0.00 s) + Fln_error_TCC1........................proved - complete [SHOSTAK](0.00 s) + Fln_error.............................proved - incomplete [SHOSTAK](0.00 s) + Fln_error_ulp.........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory top_ieee754sp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory float32 + div_f32_TCC1..........................proved - complete [SHOSTAK](0.00 s) + mod_f32_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_f32_TCC1..........................proved - complete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory aerr754sp_add + IMP_accum_err_add_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_add_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_add_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Sadd_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754sp_sub + IMP_accum_err_sub_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sub_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sub_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Ssub_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754sp_mul + IMP_accum_err_mul_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_mul_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_mul_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Smul_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_mul_props_TCC1...............proved - incomplete [SHOSTAK](0.00 s) + Smulpow2l_aerr........................proved - incomplete [SHOSTAK](0.00 s) + Smulpow2r_aerr........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754sp_div + IMP_accum_err_div_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_div_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_div_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aeboundsp_div_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Sdiv_aerr_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + Sdiv_aerr_TCC2........................proved - incomplete [SHOSTAK](0.00 s) + Sdiv_aerr_TCC3........................proved - incomplete [SHOSTAK](0.00 s) + Sdiv_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory aerr754sp_sqt + IMP_accum_err_sqt_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sqt_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sqt_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aeboundsp_sqt_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Ssqrt_aerr_TCC1.......................proved - incomplete [SHOSTAK](0.00 s) + Ssqrt_aerr_TCC2.......................proved - incomplete [SHOSTAK](0.00 s) + Ssqrt_aerr............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754sp_flr + IMP_accum_err_flr_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_flr_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_flr_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aeboundsp_flr_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Sfloor_aerr...........................proved - incomplete [SHOSTAK](0.00 s) + flr_exact_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + aeboundsp_flr_t_TCC1..................proved - incomplete [SHOSTAK](0.00 s) + Sfloor_t_aerr.........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory aerr754sp_neg + IMP_accum_err_neg_TCC1................proved - complete [SHOSTAK](0.00 s) + Sneg_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr754sp_abs + IMP_accum_err_abs_TCC1................proved - complete [SHOSTAK](0.00 s) + Sabs_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr754sp_sin + IMP_accum_err_sin_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sin_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sin_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Ssin_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754sp_cos + IMP_accum_err_cos_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_cos_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_cos_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Scos_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754sp_atn + IMP_accum_err_atn_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_atn_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_atn_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Satan_aerr............................proved - incomplete [SHOSTAK](0.00 s) + Satan_t_aerr..........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory aerr754sp_exp + IMP_accum_err_exp_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_exp_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_exp_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Sexp_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754sp_ln + IMP_accum_err_ln_TCC1.................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_ln_TCC2.................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_ln_TCC3.................proved - incomplete [SHOSTAK](0.00 s) + aeboundsp_ln_TCC1.....................proved - incomplete [SHOSTAK](0.00 s) + Sln_aerr_TCC1.........................proved - incomplete [SHOSTAK](0.00 s) + Sln_aerr_TCC2.........................proved - incomplete [SHOSTAK](0.00 s) + Sln_aerr..............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory accum_err_ln + ln_aerr_bound_TCC1....................proved - complete [SHOSTAK](0.00 s) + ln_aerr_bound_TCC2....................proved - complete [SHOSTAK](0.00 s) + ln_aerr_bound_TCC3....................proved - incomplete [SHOSTAK](0.00 s) + ln_accum_err_TCC1.....................proved - complete [SHOSTAK](0.00 s) + ln_accum_err_TCC2.....................proved - complete [SHOSTAK](0.00 s) + ln_accum_err..........................proved - incomplete [SHOSTAK](0.00 s) + ln_ulp_bound_TCC1.....................proved - complete [SHOSTAK](0.00 s) + ln_ulp_bound_TCC2.....................proved - complete [SHOSTAK](0.00 s) + Fln_accum_err_bound_TCC1..............proved - complete [SHOSTAK](0.00 s) + Fln_accum_err_bound...................proved - incomplete [SHOSTAK](0.00 s) + ln_prf_TCC1...........................proved - complete [SHOSTAK](0.00 s) + ln_prf_TCC2...........................proved - complete [SHOSTAK](0.00 s) + ln_prf_TCC3...........................proved - incomplete [SHOSTAK](0.00 s) + ln_prf_TCC4...........................proved - incomplete [SHOSTAK](0.00 s) + ln_prf_TCC5...........................proved - incomplete [SHOSTAK](0.00 s) + ln_prf_TCC6...........................proved - incomplete [SHOSTAK](0.00 s) + ln_prf_TCC7...........................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound_TCC1..................proved - incomplete [SHOSTAK](0.00 s) + accum_err_bound.......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.01 s) + + Proof summary for theory aerr754sp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory ieee754dp + precomputed_rep_int_limit.............proved - complete [SHOSTAK](0.00 s) + IMP_float_TCC1........................proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC1.........proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC2.........proved - complete [SHOSTAK](0.00 s) + IMP_float_props_rounding_TCC3.........proved - complete [SHOSTAK](0.00 s) + double_precision_format_TCC1..........proved - complete [SHOSTAK](0.00 s) + dp_closest?_j.........................proved - incomplete [SHOSTAK](0.00 s) + dp_closest?_closestroundingpred_j.....proved - complete [SHOSTAK](0.00 s) + RtoD_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + RtoD_closest_double...................proved - incomplete [SHOSTAK](0.00 s) + rtod_canonicroundfun_exactrepconservation_j...proved - incomplete [SHOSTAK](0.00 s) + rtod_monotonic........................proved - incomplete [SHOSTAK](0.00 s) + neq_lt_rew............................proved - complete [SHOSTAK](0.01 s) + noteq_rew_rl1.........................proved - complete [SHOSTAK](0.00 s) + noteq_rew_rl2.........................proved - complete [SHOSTAK](0.00 s) + noteq_rew.............................proved - complete [SHOSTAK](0.00 s) + neq_rew...............................proved - complete [SHOSTAK](0.00 s) + leq_def...............................proved - complete [SHOSTAK](0.00 s) + Dulp_def..............................proved - complete [SHOSTAK](0.00 s) + DtoR_round............................proved - incomplete [SHOSTAK](0.00 s) + DtoR_RtoD.............................proved - incomplete [SHOSTAK](0.00 s) + DtoR_RtoD_int_exactly_representable...proved - incomplete [SHOSTAK](0.00 s) + RtoD_DtoR.............................proved - incomplete [SHOSTAK](0.00 s) + DtoR_ext..............................proved - complete [SHOSTAK](0.00 s) + DtoR_strictly_increasing..............proved - complete [SHOSTAK](0.00 s) + DtoR_inc..............................proved - complete [SHOSTAK](0.00 s) + RtoD_inc..............................proved - incomplete [SHOSTAK](0.00 s) + RtoD_opp..............................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RtoD_TCC1.................proved - incomplete [SHOSTAK](0.00 s) + unique_zero_RtoD......................proved - incomplete [SHOSTAK](0.00 s) + dp_rep_exp_bound......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 31 formulas, 31 attempted, 31 succeeded (0.01 s) + + Proof summary for theory ieee754dp_add + IMP_cr_add_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dadd_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dadd_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_sub + IMP_cr_sub_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dsub_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dsub_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_mul + IMP_std_mul_TCC1......................proved - complete [SHOSTAK](0.00 s) + Dmul_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dmul_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Dmul_commutative......................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory ieee754dp_div + IMP_cr_div_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Ddiv_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Ddiv_TCC2.............................proved - incomplete [SHOSTAK](0.00 s) + Ddiv_correctly_rounded_TCC1...........proved - complete [SHOSTAK](0.00 s) + Ddiv_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory ieee754dp_sqt + IMP_cr_sqt_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dsqrt_TCC1............................proved - complete [SHOSTAK](0.00 s) + Dsqrt_TCC2............................proved - incomplete [SHOSTAK](0.00 s) + Dsqrt_correctly_rounded_TCC1..........proved - complete [SHOSTAK](0.00 s) + Dsqrt_correctly_rounded_TCC2..........proved - complete [SHOSTAK](0.00 s) + Dsqrt_correctly_rounded...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.00 s) + + Proof summary for theory ieee754dp_flr + IMP_cr_flr_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dfloor_TCC1...........................proved - incomplete [SHOSTAK](0.00 s) + Dfloor_correctly_rounded..............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_neg + IMP_cr_neg_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dneg_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dneg_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Dneg_Fopp.............................proved - incomplete [SHOSTAK](0.00 s) + Dneg_correct..........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory ieee754dp_abs + IMP_cr_abs_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dabs_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dabs_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_mod + IMP_cr_mod_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dmod_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dmod_TCC2.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_sin + IMP_cr_sin_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dsin_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dsin_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_cos + IMP_std_cos_TCC1......................proved - complete [SHOSTAK](0.00 s) + Dcos_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dcos_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_atn + IMP_std_atn_TCC1......................proved - complete [SHOSTAK](0.00 s) + Datan_TCC1............................proved - incomplete [SHOSTAK](0.00 s) + Datan_correctly_rounded...............proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_exp + IMP_std_exp_TCC1......................proved - complete [SHOSTAK](0.00 s) + Dexp_TCC1.............................proved - incomplete [SHOSTAK](0.00 s) + Dexp_correctly_rounded................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.00 s) + + Proof summary for theory ieee754dp_ln + IMP_std_ln_TCC1.......................proved - complete [SHOSTAK](0.00 s) + Dln_TCC1..............................proved - complete [SHOSTAK](0.00 s) + Dln_TCC2..............................proved - complete [SHOSTAK](0.00 s) + Dln_TCC3..............................proved - incomplete [SHOSTAK](0.00 s) + Dln_correctly_rounded_TCC1............proved - complete [SHOSTAK](0.00 s) + Dln_correctly_rounded_TCC2............proved - complete [SHOSTAK](0.00 s) + Dln_correctly_rounded.................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory top_ieee754dp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory double64 + mod_d64_TCC1..........................proved - incomplete [SHOSTAK](0.00 s) + sqt_d64_TCC1..........................proved - complete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr754dp_add + IMP_accum_err_add_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_add_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_add_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dadd_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754dp_sub + IMP_accum_err_sub_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sub_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sub_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dsub_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754dp_mul + IMP_accum_err_mul_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_mul_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_mul_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dmul_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + IMP_aerr_mul_props_TCC1...............proved - incomplete [SHOSTAK](0.00 s) + Dmulpow2l_aerr........................proved - incomplete [SHOSTAK](0.00 s) + Dmulpow2r_aerr........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754dp_div + IMP_accum_err_div_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_div_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_div_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aebounddp_div_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Ddiv_aerr_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + Ddiv_aerr_TCC2........................proved - incomplete [SHOSTAK](0.00 s) + Ddiv_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754dp_sqt + IMP_accum_err_sqt_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sqt_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sqt_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aebounddp_sqt_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Dsqrt_aerr_TCC1.......................proved - incomplete [SHOSTAK](0.00 s) + Dsqrt_aerr_TCC2.......................proved - incomplete [SHOSTAK](0.00 s) + Dsqrt_aerr............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754dp_flr + IMP_accum_err_flr_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_flr_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_flr_TCC3................proved - incomplete [SHOSTAK](0.00 s) + aebounddp_flr_TCC1....................proved - incomplete [SHOSTAK](0.00 s) + Dfloor_aerr...........................proved - incomplete [SHOSTAK](0.00 s) + flr_exact_TCC1........................proved - incomplete [SHOSTAK](0.00 s) + aebounddp_flr_t_TCC1..................proved - incomplete [SHOSTAK](0.00 s) + Dfloor_t_aerr.........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.00 s) + + Proof summary for theory aerr754dp_neg + IMP_accum_err_neg_TCC1................proved - complete [SHOSTAK](0.00 s) + Dneg_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr754dp_abs + IMP_accum_err_abs_TCC1................proved - complete [SHOSTAK](0.00 s) + Dabs_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.00 s) + + Proof summary for theory aerr754dp_sin + IMP_accum_err_sin_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sin_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_sin_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dsin_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754dp_cos + IMP_accum_err_cos_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_cos_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_cos_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dcos_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754dp_atn + IMP_accum_err_atn_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_atn_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_atn_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Datan_aerr............................proved - incomplete [SHOSTAK](0.00 s) + Datan_t_aerr..........................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.00 s) + + Proof summary for theory aerr754dp_exp + IMP_accum_err_exp_TCC1................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_exp_TCC2................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_exp_TCC3................proved - incomplete [SHOSTAK](0.00 s) + Dexp_aerr.............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.00 s) + + Proof summary for theory aerr754dp_ln + IMP_accum_err_ln_TCC1.................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_ln_TCC2.................proved - complete [SHOSTAK](0.00 s) + IMP_accum_err_ln_TCC3.................proved - incomplete [SHOSTAK](0.00 s) + aebounddp_ln_TCC1.....................proved - incomplete [SHOSTAK](0.00 s) + Dln_aerr_TCC1.........................proved - incomplete [SHOSTAK](0.00 s) + Dln_aerr_TCC2.........................proved - incomplete [SHOSTAK](0.00 s) + Dln_aerr..............................proved - incomplete [SHOSTAK](0.00 s) + Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.00 s) + + Proof summary for theory aerr754dp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory total_ieee754sp + Sdiv_TCC1.............................proved - complete [SHOSTAK](0.00 s) + Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s) + + Proof summary for theory total_ieee754dp + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + + Proof summary for theory strategies + Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) + +Grand Totals: 918 proofs, 918 attempted, 918 succeeded (0.70 s)