|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
critical-bugs
Sprache: Unknown
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[575] Hlasm[2081] Haskell[2399]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (19:0:22 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
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.09 s)
radix_div_vNum.......................proved - complete [shostak]( 0.12 s)
radix_less_vNum......................proved - complete [shostak]( 0.19 s)
FtoR_TCC1............................proved - complete [shostak]( 0.03 s)
float_int_def........................proved - complete [shostak]( 0.03 s)
Fplus_TCC1...........................proved - complete [shostak]( 0.06 s)
Fplus_TCC2...........................proved - complete [shostak]( 0.05 s)
Fplus_TCC3...........................proved - complete [shostak]( 0.14 s)
Fminus_TCC1..........................proved - complete [shostak]( 0.12 s)
sum_float_commutes...................proved - complete [shostak](-1.22 s)
mult_float_commutes..................proved - complete [shostak]( 0.03 s)
FexptCorrect_TCC1....................proved - complete [shostak]( 0.03 s)
FexptCorrect.........................proved - complete [shostak]( 0.27 s)
sigma_TCC1...........................proved - complete [shostak]( 0.04 s)
sigma_TCC2...........................proved - complete [shostak]( 0.02 s)
FDivInt_TCC1.........................proved - complete [shostak]( 0.31 s)
FDivInt_def..........................proved - complete [shostak]( 0.22 s)
hathatln_TCC1........................proved - incomplete [shostak]( 0.17 s)
hathatln_TCC2........................proved - incomplete [shostak]( 0.10 s)
hathatln.............................proved - incomplete [shostak]( 0.11 s)
hathat_int_TCC1......................proved - complete [shostak]( 0.03 s)
hathat_int_TCC2......................proved - complete [shostak]( 0.03 s)
hathat_int...........................proved - incomplete [shostak]( 0.29 s)
Fsucc_TCC1...........................proved - complete [shostak]( 0.03 s)
Fpred_TCC1...........................proved - complete [shostak]( 0.08 s)
Fnormalize_TCC1......................proved - complete [shostak]( 0.08 s)
Fnormalize_TCC2......................proved - complete [shostak]( 0.11 s)
Fnormalize_TCC3......................proved - complete [shostak]( 0.14 s)
Fnormalize_TCC4......................proved - complete [shostak]( 0.14 s)
Fnormalize_TCC5......................proved - complete [shostak]( 0.79 s)
Fnormalize_TCC6......................proved - complete [shostak]( 0.19 s)
Fulp_TCC1............................proved - complete [shostak]( 0.07 s)
FcanonicOpp..........................proved - complete [shostak]( 0.90 s)
FcanonicBounded......................proved - complete [shostak]( 0.08 s)
FpredCanonic.........................proved - complete [shostak]( 3.83 s)
RND_log_compute_TCC1.................proved - complete [shostak]( 0.05 s)
RND_log_compute_TCC2.................proved - complete [shostak]( 0.13 s)
RND_log_compute_TCC3.................proved - complete [shostak]( 0.06 s)
RND_log_compute_TCC4.................proved - complete [shostak]( 0.14 s)
RND_log_compute......................proved - incomplete [shostak]( 1.48 s)
RND_aux_TCC1.........................proved - complete [shostak]( 0.10 s)
RND_aux_TCC2.........................proved - complete [shostak]( 0.66 s)
RND_aux_TCC3.........................proved - complete [shostak]( 0.07 s)
RND_aux_TCC4.........................proved - complete [shostak]( 0.19 s)
RND_aux_TCC5.........................proved - complete [shostak]( 0.21 s)
RND_aux_TCC6.........................proved - incomplete [shostak]( 7.84 s)
RND_aux_alt_TCC1.....................proved - complete [shostak]( 0.09 s)
RND_aux_alt_TCC2.....................proved - incomplete [shostak]( 0.12 s)
RND_aux_alt_TCC3.....................proved - incomplete [shostak]( 0.25 s)
RND_aux_alt_def......................proved - incomplete [shostak]( 0.30 s)
RND_Min_TCC1.........................proved - complete [shostak]( 0.03 s)
RND_Min_TCC2.........................proved - complete [shostak]( 0.03 s)
RND_Min_TCC3.........................proved - incomplete [shostak]( 0.03 s)
RND_Min_TCC4.........................proved - incomplete [shostak]( 0.03 s)
RND_Max_TCC1.........................proved - incomplete [shostak]( 0.03 s)
Exp_incr_1_TCC1......................proved - complete [shostak]( 0.03 s)
Exp_incr_1...........................proved - complete [shostak]( 0.05 s)
Exp_incr_2...........................proved - complete [shostak]( 0.06 s)
Exp_increq_1_TCC1....................proved - complete [shostak]( 0.03 s)
Exp_increq_1.........................proved - complete [shostak]( 0.05 s)
Exp_increq_2.........................proved - complete [shostak]( 0.06 s)
Exp_1................................proved - complete [shostak]( 0.07 s)
EqExpEq..............................proved - complete [shostak]( 0.08 s)
expt_odd_TCC1........................proved - complete [shostak]( 0.03 s)
expt_odd.............................proved - complete [shostak]( 0.35 s)
expt_even............................proved - complete [shostak]( 0.77 s)
FoppCorrect..........................proved - complete [shostak]( 0.05 s)
FoppFopp.............................proved - complete [shostak]( 0.04 s)
Fopp_mult_left.......................proved - complete [shostak]( 0.07 s)
Fopp_mult_right......................proved - complete [shostak]( 0.05 s)
FabsCorrect..........................proved - complete [shostak]( 0.10 s)
FplusCorrect.........................proved - complete [shostak]( 0.20 s)
FplusAssociative.....................proved - complete [shostak]( 0.80 s)
FmultAssociative.....................proved - complete [shostak]( 0.07 s)
FminusCorrect........................proved - complete [shostak]( 0.20 s)
FmultCorrect.........................proved - complete [shostak]( 0.18 s)
Fmult_1_r............................proved - complete [shostak]( 0.06 s)
Fmult_1_l............................proved - complete [shostak]( 0.07 s)
Fmult_2_r............................proved - complete [shostak]( 0.03 s)
Fmult_2_l............................proved - complete [shostak]( 0.03 s)
FDivKexpt_TCC1.......................proved - complete [shostak]( 0.03 s)
FDivKexpt_TCC2.......................proved - complete [shostak]( 0.03 s)
FDivKexpt_TCC3.......................proved - complete [shostak]( 0.84 s)
FDivKexpt_def........................proved - complete [shostak]( 2.61 s)
FoppBounded..........................proved - complete [shostak]( 0.15 s)
FabsBounded..........................proved - complete [shostak]( 0.10 s)
FabsCanonic..........................proved - complete [shostak]( 0.39 s)
LeR0Fnum.............................proved - complete [shostak]( 0.11 s)
LeFnumZERO...........................proved - complete [shostak]( 0.11 s)
FleCorrect...........................proved - complete [shostak]( 0.31 s)
FltCorrect...........................proved - complete [shostak]( 0.40 s)
FminCorrect..........................proved - complete [shostak]( 0.08 s)
FmaxCorrect..........................proved - complete [shostak]( 0.09 s)
FsubnormalUnique.....................proved - complete [shostak]( 0.31 s)
FnormalUnique........................proved - complete [shostak]( 1.92 s)
NormalAndSubNormalNotEq..............proved - complete [shostak]( 0.62 s)
FcanonicUnique.......................proved - complete [shostak]( 1.06 s)
FnormalizeCorrect....................proved - complete [shostak]( 0.03 s)
FulpCanonic_TCC1.....................proved - complete [shostak]( 0.10 s)
FulpCanonic..........................proved - complete [shostak]( 0.04 s)
Lexico...............................proved - complete [shostak]( 2.43 s)
CanonicLeastExp......................proved - complete [shostak]( 0.04 s)
Fast_canonic.........................proved - complete [shostak]( 0.11 s)
FulpOpp_TCC1.........................proved - complete [shostak]( 0.03 s)
FulpOpp..............................proved - complete [shostak]( 0.10 s)
FulpAbs_TCC1.........................proved - complete [shostak]( 0.03 s)
FulpAbs..............................proved - complete [shostak]( 0.11 s)
FulpMonotone.........................proved - complete [shostak]( 0.06 s)
FulpMonotoneAbs......................proved - complete [shostak]( 0.09 s)
FloatPlusUlpBounded..................proved - complete [shostak]( 0.84 s)
FloatMinusUlpBounded.................proved - complete [shostak]( 0.11 s)
FpredFoppFsucc.......................proved - complete [shostak]( 0.28 s)
FsuccFoppFpred.......................proved - complete [shostak]( 0.27 s)
FsuccFpred...........................proved - complete [shostak]( 1.41 s)
FpredFsucc...........................proved - complete [shostak]( 0.09 s)
FpredBounded.........................proved - complete [shostak]( 0.82 s)
FsuccBounded.........................proved - complete [shostak]( 0.05 s)
FsuccCanonic.........................proved - complete [shostak]( 0.04 s)
FpredPos.............................proved - complete [shostak]( 0.37 s)
FsuccPos.............................proved - complete [shostak]( 0.42 s)
FpredDiff_TCC1.......................proved - complete [shostak]( 0.03 s)
FpredDiff............................proved - complete [shostak]( 0.40 s)
FsuccDiff............................proved - complete [shostak]( 0.07 s)
FpredLt..............................proved - complete [shostak]( 0.52 s)
FpredLe_aux..........................proved - complete [shostak](13.47 s)
FpredLe_aux2.........................proved - complete [shostak]( 0.13 s)
FpredLe..............................proved - complete [shostak]( 0.56 s)
FsuccLe..............................proved - complete [shostak]( 0.05 s)
FpredProp_aux........................proved - complete [shostak]( 2.76 s)
FpredProp............................proved - complete [shostak]( 0.18 s)
FsuccLt..............................proved - complete [shostak]( 0.12 s)
FsuccProp............................proved - complete [shostak]( 0.05 s)
FsuccZleEq_aux.......................proved - complete [shostak]( 0.03 s)
FsuccZleEq...........................proved - complete [shostak]( 0.42 s)
EvenFsuccOdd_aux_TCC1................proved - complete [shostak]( 0.03 s)
EvenFsuccOdd_aux.....................proved - complete [shostak]( 0.21 s)
EvenFsuccOdd.........................proved - complete [shostak]( 0.33 s)
OddFsuccEven_aux_TCC1................proved - complete [shostak]( 0.03 s)
OddFsuccEven_aux.....................proved - complete [shostak]( 0.16 s)
OddFsuccEven.........................proved - complete [shostak]( 0.36 s)
MinOppMax............................proved - complete [shostak]( 0.06 s)
MaxOppMin............................proved - complete [shostak]( 0.07 s)
ClosestFopp..........................proved - complete [shostak]( 0.34 s)
RleRoundedR0.........................proved - complete [shostak]( 0.17 s)
RleRoundedLessR0.....................proved - complete [shostak]( 0.17 s)
RND_aux_le...........................proved - incomplete [shostak]( 0.96 s)
RND_aux_ge...........................proved - incomplete [shostak]( 2.51 s)
RND_Min_isMin_TCC1...................proved - incomplete [shostak]( 0.03 s)
RND_Min_isMin........................proved - incomplete [shostak]( 0.32 s)
RND_Max_isMax_TCC1...................proved - incomplete [shostak]( 0.03 s)
RND_Max_isMax........................proved - incomplete [shostak]( 0.05 s)
RND_aux_float_TCC1...................proved - complete [shostak]( 0.04 s)
RND_aux_float_TCC2...................proved - complete [shostak]( 0.08 s)
RND_aux_float_TCC3...................proved - complete [shostak]( 0.89 s)
RND_aux_float_TCC4...................proved - complete [shostak]( 0.11 s)
RND_aux_float_TCC5...................proved - complete [shostak]( 0.23 s)
RND_aux_float_TCC6...................proved - complete [shostak]( 0.10 s)
RND_aux_float_TCC7...................proved - incomplete [shostak]( 1.67 s)
RND_aux_float_def_TCC1...............proved - complete [shostak]( 0.09 s)
RND_aux_float_def....................proved - incomplete [shostak]( 1.07 s)
RND_float_Min_TCC1...................proved - complete [shostak]( 0.03 s)
RND_float_Min_TCC2...................proved - complete [shostak]( 0.04 s)
RND_float_Min_TCC3...................proved - incomplete [shostak]( 0.04 s)
RND_float_Min_TCC4...................proved - incomplete [shostak]( 0.06 s)
RND_float_Min_def....................proved - incomplete [shostak]( 0.42 s)
RND_float_Max_TCC1...................proved - incomplete [shostak]( 0.03 s)
RND_float_Max_def....................proved - incomplete [shostak]( 0.12 s)
RND_float_Min_ge_canonic.............proved - incomplete [shostak]( 0.11 s)
RND_float_Max_le_canonic.............proved - incomplete [shostak]( 0.12 s)
RND_float_Min_canonic................proved - incomplete [shostak]( 0.06 s)
RND_float_Max_canonic................proved - incomplete [shostak]( 0.04 s)
RND_float_Min_ge.....................proved - incomplete [shostak]( 0.04 s)
RND_float_Min_le.....................proved - incomplete [shostak]( 0.05 s)
RND_float_Max_ge.....................proved - incomplete [shostak]( 0.49 s)
RND_float_Max_le.....................proved - incomplete [shostak]( 0.47 s)
RND_float_Min_lt_canonic.............proved - incomplete [shostak]( 0.13 s)
RND_float_Min_gt_canonic.............proved - incomplete [shostak]( 0.14 s)
RND_float_Min_ge_0...................proved - incomplete [shostak]( 0.35 s)
RND_float_Min_lt_0...................proved - incomplete [shostak]( 0.22 s)
RND_float_Max_le_0...................proved - incomplete [shostak]( 0.71 s)
RND_float_Max_gt_0...................proved - incomplete [shostak]( 0.22 s)
Fmult_canonic_id_Min_TCC1............proved - complete [shostak]( 0.10 s)
Fmult_canonic_id_Min.................proved - incomplete [shostak]( 0.08 s)
Fmult_canonic_id_Max.................proved - incomplete [shostak]( 0.08 s)
Fplus_canonic_id_Min_TCC1............proved - complete [shostak]( 0.15 s)
Fplus_canonic_id_Min.................proved - incomplete [shostak]( 0.09 s)
Fplus_canonic_id_Max.................proved - incomplete [shostak]( 0.10 s)
MaxSuccMin_TCC1......................proved - complete [shostak]( 0.03 s)
MaxSuccMin...........................proved - complete [shostak]( 0.13 s)
LeMinMaxClosest......................proved - complete [shostak]( 8.36 s)
isMin_Total..........................proved - incomplete [shostak]( 0.03 s)
isMin_Compatible.....................proved - complete [shostak]( 0.04 s)
isMin_Monotone.......................proved - complete [shostak]( 0.05 s)
isMin_RoundedMode....................proved - incomplete [shostak]( 0.03 s)
isMin_Unique.........................proved - complete [shostak]( 0.04 s)
isMax_Total..........................proved - incomplete [shostak]( 0.05 s)
isMax_Compatible.....................proved - complete [shostak]( 0.12 s)
isMax_Monotone.......................proved - complete [shostak]( 0.12 s)
isMax_RoundedMode....................proved - incomplete [shostak]( 0.03 s)
isMax_Unique.........................proved - complete [shostak]( 0.18 s)
ToZero_Total.........................proved - incomplete [shostak]( 0.45 s)
ToZero_Compatible....................proved - complete [shostak]( 0.12 s)
ToZero_MinOrMax......................proved - complete [shostak]( 0.03 s)
ToZero_Monotone......................proved - complete [shostak]( 0.55 s)
ToZero_RoundedMode...................proved - incomplete [shostak]( 0.03 s)
ToZero_Unique........................proved - complete [shostak]( 0.10 s)
Closest_Total........................proved - incomplete [shostak]( 0.90 s)
Closest_Compatible...................proved - complete [shostak]( 0.09 s)
Closest_MinOrMax.....................proved - complete [shostak]( 0.17 s)
Closest_Monotone.....................proved - complete [shostak]( 0.24 s)
Closest_RoundedMode..................proved - incomplete [shostak]( 0.03 s)
RND_EClosest_isEclosest_TCC1.........proved - incomplete [shostak]( 0.02 s)
RND_EClosest_isEclosest..............proved - incomplete [shostak]( 3.03 s)
EvenClosest_Total....................proved - incomplete [shostak]( 0.04 s)
EvenClosest_Compatible...............proved - complete [shostak]( 0.08 s)
EvenClosest_MinOrMax.................proved - complete [shostak]( 0.04 s)
EvenClosest_Monotone.................proved - complete [shostak]( 0.05 s)
EvenClosest_RoundedMode..............proved - incomplete [shostak]( 0.03 s)
EvenClosest_Unique...................proved - complete [shostak]( 0.23 s)
AFZClosest_Total.....................proved - incomplete [shostak](-0.98 s)
AFZClosest_Compatible................proved - complete [shostak]( 0.06 s)
AFZClosest_MinOrMax..................proved - complete [shostak]( 0.04 s)
AFZClosest_Monotone..................proved - complete [shostak]( 0.05 s)
AFZClosest_RoundedMode...............proved - incomplete [shostak]( 0.03 s)
AFZClosest_Unique....................proved - incomplete [shostak]( 0.88 s)
RoundedProjectorEq...................proved - complete [shostak]( 0.05 s)
RoundedProjector.....................proved - complete [shostak]( 0.04 s)
isMin_Rep............................proved - complete [shostak]( 0.28 s)
RoundedModeRep.......................proved - complete [shostak]( 0.10 s)
RoundedModeUlp.......................proved - complete [shostak]( 0.25 s)
ClosestUlp...........................proved - incomplete [shostak]( 0.69 s)
RoundedModeNonDecreasing.............proved - complete [shostak]( 0.05 s)
ClosestUlp2_TCC1.....................proved - complete [shostak]( 0.04 s)
ClosestUlp2..........................proved - incomplete [shostak]( 1.40 s)
ClosestFabs..........................proved - incomplete [shostak]( 0.36 s)
SterbenzAux..........................proved - complete [shostak]( 0.71 s)
Sterbenz.............................proved - complete [shostak]( 0.23 s)
errorBoundedPlus.....................proved - incomplete [shostak]( 1.07 s)
errorBoundedMult_aux.................proved - incomplete [shostak]( 3.22 s)
errorBoundedMult_aux2................proved - incomplete [shostak]( 3.47 s)
errorBoundedMult.....................proved - incomplete [shostak]( 1.11 s)
FulpLeN_TCC1.........................proved - complete [shostak]( 0.10 s)
FulpLeN..............................proved - complete [shostak]( 0.51 s)
FulpGe_TCC1..........................proved - complete [shostak]( 0.03 s)
FulpGe...............................proved - complete [shostak]( 1.09 s)
FulpLe_TCC1..........................proved - complete [shostak]( 0.06 s)
FulpLe...............................proved - complete [shostak]( 0.26 s)
FulpFpred1_TCC1......................proved - complete [shostak]( 0.04 s)
FulpFpred1...........................proved - complete [shostak]( 0.28 s)
FulpFpred2...........................proved - complete [shostak]( 0.26 s)
Theory totals: 250 formulas, 250 attempted, 250 succeeded (104.76 s)
Proof summary for theory axpy
FcanonicBounded2.....................proved - complete [shostak]( 0.02 s)
MinOrMax_Rlt.........................proved - incomplete [shostak]( 0.07 s)
MinOrMax_Fopp_TCC1...................proved - complete [shostak]( 0.03 s)
MinOrMax_Fopp........................proved - complete [shostak]( 0.03 s)
MinOrMax1_TCC1.......................proved - complete [shostak]( 0.03 s)
MinOrMax1_TCC2.......................proved - complete [shostak]( 0.03 s)
MinOrMax1............................proved - complete [shostak]( 0.48 s)
MinOrMax2_TCC1.......................proved - complete [shostak]( 0.02 s)
MinOrMax2............................proved - complete [shostak]( 0.13 s)
MinOrMax3_TCC1.......................proved - complete [shostak]( 0.03 s)
MinOrMax3............................proved - complete [shostak]( 1.15 s)
RoundLe_TCC1.........................proved - complete [shostak]( 0.02 s)
RoundLe_TCC2.........................proved - complete [shostak]( 0.16 s)
RoundLe_TCC3.........................proved - complete [shostak]( 0.66 s)
RoundLe..............................proved - incomplete [shostak]( 2.22 s)
RoundGe_TCC1.........................proved - complete [shostak]( 0.10 s)
RoundGe..............................proved - incomplete [shostak]( 1.46 s)
ExactSum_Near_TCC1...................proved - complete [shostak]( 0.29 s)
ExactSum_Near........................proved - incomplete [shostak]( 0.82 s)
Normal_iff_TCC1......................proved - complete [shostak]( 0.21 s)
Normal_iff...........................proved - complete [shostak]( 0.94 s)
Axpy_aux1_TCC1.......................proved - complete [shostak]( 0.06 s)
Axpy_aux1............................proved - incomplete [shostak]( 3.70 s)
Axpy_aux1_aux1.......................proved - incomplete [shostak]( 1.05 s)
Axpy_aux1_aux2.......................proved - incomplete [shostak]( 0.88 s)
Axpy_aux2............................proved - incomplete [shostak]( 1.45 s)
Axpy_aux3............................proved - incomplete [shostak]( 4.26 s)
AxpyPos..............................proved - incomplete [shostak]( 0.50 s)
Axpy_opt_aux1_aux1_TCC1..............proved - complete [shostak]( 0.34 s)
Axpy_opt_aux1_aux1_TCC2..............proved - complete [shostak]( 0.68 s)
Axpy_opt_aux1_aux1_TCC3..............proved - complete [shostak]( 0.34 s)
Axpy_opt_aux1_aux1_TCC4..............proved - complete [shostak]( 0.57 s)
Axpy_opt_aux1_aux1_TCC5..............proved - complete [shostak]( 0.36 s)
Axpy_opt_aux1_aux1...................proved - complete [shostak](17.90 s)
Axpy_opt_aux1_TCC1...................proved - complete [shostak]( 0.75 s)
Axpy_opt_aux1........................proved - incomplete [shostak]( 8.83 s)
Axpy_opt_aux2_TCC1...................proved - complete [shostak]( 0.74 s)
Axpy_opt_aux2_TCC2...................proved - complete [shostak]( 0.82 s)
Axpy_opt_aux2........................proved - incomplete [shostak](37.70 s)
Axpy_opt_aux3_TCC1...................proved - complete [shostak]( 0.78 s)
Axpy_opt_aux3_TCC2...................proved - complete [shostak]( 0.98 s)
Axpy_opt_aux3........................proved - incomplete [shostak](14.40 s)
Axpy_optPos_TCC1.....................proved - complete [shostak]( 0.70 s)
Axpy_optPos_TCC2.....................proved - complete [shostak]( 0.87 s)
Axpy_optPos..........................proved - incomplete [shostak]( 1.00 s)
Axpy_optZero_TCC1....................proved - complete [shostak]( 0.70 s)
Axpy_optZero_TCC2....................proved - complete [shostak]( 0.89 s)
Axpy_optZero.........................proved - incomplete [shostak]( 2.64 s)
Axpy_opt_TCC1........................proved - complete [shostak]( 0.69 s)
Axpy_opt_TCC2........................proved - complete [shostak]( 0.86 s)
Axpy_opt.............................proved - incomplete [shostak]( 2.09 s)
Axpy_simpl...........................proved - incomplete [shostak]( 0.51 s)
Theory totals: 52 formulas, 52 attempted, 52 succeeded (116.93 s)
Proof summary for theory IEEE_854
Significand_size_TCC1.................proved - complete [shostak](0.02 s)
Exponent_balance_TCC1.................proved - complete [shostak](0.02 s)
Exponent_balance_TCC2.................proved - complete [shostak](0.05 s)
Exponent_balance......................proved - complete [shostak](0.21 s)
E_max_gt_E_min........................proved - complete [shostak](0.11 s)
HUG_example...........................proved - complete [shostak](0.04 s)
ex754_2...............................proved - complete [shostak](0.04 s)
ex754_3...............................proved - complete [shostak](0.25 s)
E_min_neg.............................proved - complete [shostak](0.08 s)
E_max_pos.............................proved - complete [shostak](0.08 s)
IMP_IEEE_854_defs_TCC1................proved - complete [shostak](0.01 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.91 s)
Proof summary for theory IEEE_854_defs
fp_add_TCC1...........................proved - complete [shostak](0.05 s)
fp_add_TCC2...........................proved - complete [shostak](0.02 s)
fp_add_x_correct......................proved - complete [shostak](0.16 s)
fsub_alt_def..........................proved - complete [shostak](0.25 s)
fp_div_TCC1...........................proved - complete [shostak](0.02 s)
fp_div_TCC2...........................proved - complete [shostak](0.04 s)
fp_sqrt_TCC1..........................proved - complete [shostak](0.03 s)
fp_sqrt_TCC2..........................proved - complete [shostak](0.10 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.67 s)
Proof summary for theory IEEE_854_values
value_digit_TCC1......................proved - complete [shostak](0.03 s)
value_TCC1............................proved - complete [shostak](0.02 s)
shift_left_TCC1.......................proved - complete [shostak](0.06 s)
shift_left_TCC2.......................proved - complete [shostak](0.05 s)
normalize_TCC1........................proved - complete [shostak](0.03 s)
normalize_TCC2........................proved - complete [shostak](0.03 s)
normalize_TCC3........................proved - complete [shostak](0.03 s)
normalize_TCC4........................proved - complete [shostak](0.03 s)
normalize_idempotent..................proved - complete [shostak](0.20 s)
subnormal?_TCC1.......................proved - complete [shostak](0.11 s)
normal?_TCC1..........................proved - complete [shostak](0.03 s)
max_significand_TCC1..................proved - complete [shostak](0.03 s)
min_significand_TCC1..................proved - complete [shostak](0.03 s)
min_significand_TCC2..................proved - complete [shostak](0.03 s)
d_zero_TCC1...........................proved - complete [shostak](0.03 s)
Sum_value0............................proved - complete [shostak](0.15 s)
zero_finite_d_zero....................proved - complete [shostak](0.03 s)
max_fp_pos_TCC1.......................proved - complete [shostak](0.02 s)
min_fp_pos_TCC1.......................proved - complete [shostak](0.02 s)
pos_zero_TCC1.........................proved - complete [shostak](0.02 s)
neg_zero_TCC1.........................proved - complete [shostak](0.02 s)
max_pos_TCC1..........................proved - complete [shostak](0.02 s)
max_pos_TCC2..........................proved - complete [shostak](0.18 s)
min_pos_TCC1..........................proved - complete [shostak](0.02 s)
min_pos_TCC2..........................proved - complete [shostak](0.14 s)
max_neg_TCC1..........................proved - complete [shostak](0.02 s)
max_neg_TCC2..........................proved - complete [shostak](0.21 s)
min_neg_TCC1..........................proved - complete [shostak](0.02 s)
min_neg_TCC2..........................proved - complete [shostak](0.18 s)
max_fp_correct_TCC1...................proved - complete [shostak](0.01 s)
max_fp_correct_TCC2...................proved - complete [shostak](0.01 s)
max_fp_correct........................proved - complete [shostak](0.38 s)
min_fp_correct_TCC1...................proved - complete [shostak](0.02 s)
min_fp_correct........................proved - complete [shostak](0.20 s)
value0................................proved - complete [shostak](0.13 s)
value_of_zero.........................proved - complete [shostak](0.02 s)
normal_value..........................proved - complete [shostak](0.70 s)
value_positive........................proved - complete [shostak](0.15 s)
value_negative........................proved - complete [shostak](0.17 s)
finite_cover..........................proved - complete [shostak](0.27 s)
finite_disjoint1......................proved - complete [shostak](0.03 s)
finite_disjoint2......................proved - complete [shostak](0.02 s)
finite_disjoint3......................proved - complete [shostak](0.03 s)
toggle_sign_TCC1......................proved - complete [shostak](0.03 s)
toggle_sign_TCC2......................proved - complete [shostak](0.04 s)
toggle_finite.........................proved - complete [shostak](0.03 s)
toggle_infinite.......................proved - complete [shostak](0.03 s)
toggle_NaN............................proved - complete [shostak](0.03 s)
value_toggle_TCC1.....................proved - complete [shostak](0.02 s)
value_toggle..........................proved - complete [shostak](0.16 s)
toggle_d_normalize....................proved - complete [shostak](0.26 s)
toggle_Exp_normalize..................proved - complete [shostak](0.26 s)
toggle_zero?..........................proved - complete [shostak](0.03 s)
toggle_normal?........................proved - complete [shostak](0.03 s)
toggle_subnormal?.....................proved - complete [shostak](0.03 s)
value_digit_le_TCC1...................proved - complete [shostak](0.03 s)
value_digit_le........................proved - complete [shostak](0.07 s)
Sum_d_lt_b............................proved - complete [shostak](0.22 s)
Sum_d_lt1_TCC1........................proved - complete [shostak](0.02 s)
Sum_d_lt1.............................proved - complete [shostak](0.24 s)
Sum_d_ge1.............................proved - complete [shostak](0.18 s)
value_sig_lt_b........................proved - complete [shostak](0.04 s)
value_sig_lt1.........................proved - complete [shostak](0.04 s)
value_sig_ge1.........................proved - complete [shostak](0.03 s)
abs_value_fin.........................proved - complete [shostak](0.16 s)
min_significand_min...................proved - complete [shostak](0.32 s)
sign_normal...........................proved - complete [shostak](0.19 s)
value_normal_TCC1.....................proved - complete [shostak](0.03 s)
value_normal..........................proved - complete [shostak](0.22 s)
value_subnormal_TCC1..................proved - complete [shostak](0.17 s)
value_subnormal.......................proved - complete [shostak](0.19 s)
value_nonzero.........................proved - complete [shostak](0.16 s)
scale_value_TCC1......................proved - complete [shostak](0.02 s)
scaled_Sum_int........................proved - complete [shostak](0.31 s)
scale_value_p_TCC1....................proved - complete [shostak](0.02 s)
scale_value_p_TCC2....................proved - complete [shostak](0.21 s)
scaled_Sum_i_TCC1.....................proved - complete [shostak](0.02 s)
scaled_Sum_i..........................proved - complete [shostak](0.07 s)
scaled_Sum............................proved - complete [shostak](0.05 s)
floor_Sum.............................proved - complete [shostak](0.30 s)
mod_Sum_TCC1..........................proved - complete [shostak](0.05 s)
mod_Sum...............................proved - complete [shostak](0.79 s)
Theory totals: 82 formulas, 82 attempted, 82 succeeded (9.05 s)
Proof summary for theory sum_hack
Sum_TCC1..............................proved - complete [shostak](0.02 s)
Sum_TCC2..............................proved - complete [shostak](0.02 s)
Sum_nonneg............................proved - complete [shostak](0.09 s)
Sum_zero..............................proved - complete [shostak](0.14 s)
Sum_pos...............................proved - complete [shostak](0.12 s)
Sum_le................................proved - complete [shostak](0.10 s)
Sum_ge1...............................proved - complete [shostak](0.11 s)
Sum_ge................................proved - complete [shostak](0.11 s)
Sum_split_TCC1........................proved - complete [shostak](0.02 s)
Sum_split.............................proved - complete [shostak](0.17 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.90 s)
Proof summary for theory sum_lemmas
mant_digit_fun_TCC1...................proved - complete [shostak](0.03 s)
Sum_pos_less_1_TCC1...................proved - complete [shostak](0.06 s)
Sum_pos_less_1........................proved - complete [shostak](0.22 s)
floor_Sum_mant........................proved - complete [shostak](0.09 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.40 s)
Proof summary for theory enumerated_type_defs
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory IEEE_854_remainder
REM_TCC1..............................proved - complete [shostak](0.02 s)
REM_TCC2..............................proved - complete [shostak](0.05 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s)
Proof summary for theory real_to_fp
truncate_zero.........................proved - complete [shostak](0.08 s)
digits_of_finite......................proved - complete [shostak](0.31 s)
real_to_fp_TCC1.......................proved - complete [shostak](0.02 s)
real_to_fp_TCC2.......................proved - complete [shostak](0.07 s)
real_to_fp_TCC3.......................proved - complete [shostak](0.05 s)
real_to_fp_TCC4.......................proved - complete [shostak](0.05 s)
real_to_fp_TCC5.......................proved - complete [shostak](0.13 s)
real_to_fp_zero.......................proved - complete [shostak](0.08 s)
sign_of_value.........................proved - complete [shostak](0.04 s)
Exp_of_value_normal_TCC1..............proved - complete [shostak](0.03 s)
Exp_of_value_normal...................proved - complete [shostak](0.46 s)
real_to_fp_normal.....................proved - complete [shostak](0.16 s)
real_to_fp_subnormal..................proved - complete [shostak](0.19 s)
real_to_fp_inverts_value..............proved - complete [shostak](0.03 s)
round_exceptions_x_TCC1...............proved - complete [shostak](0.03 s)
round_exceptions_x_TCC2...............proved - complete [shostak](0.02 s)
fp_round_TCC1.........................proved - complete [shostak](0.07 s)
round_value...........................proved - complete [shostak](0.56 s)
round_value2..........................proved - complete [shostak](0.12 s)
round_0...............................proved - complete [shostak](0.02 s)
round_value3..........................proved - complete [shostak](0.03 s)
round_error_TCC1......................proved - complete [shostak](0.09 s)
round_error_TCC2......................proved - complete [shostak](0.09 s)
round_error...........................proved - complete [shostak](0.51 s)
round_near............................proved - complete [shostak](0.48 s)
round_pos.............................proved - complete [shostak](0.14 s)
round_neg.............................proved - complete [shostak](0.15 s)
round_zero............................proved - complete [shostak](0.50 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (4.52 s)
Proof summary for theory over_under
over_under?_TCC1......................proved - complete [shostak](0.07 s)
infinity_TCC1.........................proved - complete [shostak](0.02 s)
trap_over_TCC1........................proved - complete [shostak](0.02 s)
overflow_TCC1.........................proved - complete [shostak](0.15 s)
exact_underflow_TCC1..................proved - complete [shostak](0.02 s)
exact_underflow_TCC2..................proved - complete [shostak](0.04 s)
round_under_TCC1......................proved - complete [shostak](0.08 s)
round_under_TCC2......................proved - complete [shostak](0.09 s)
round_under_correct_TCC1..............proved - complete [shostak](0.13 s)
round_under_correct...................proved - complete [shostak](0.17 s)
round_under_value_TCC1................proved - complete [shostak](0.05 s)
round_under_value.....................proved - complete [shostak](0.53 s)
round_under_error_TCC1................proved - complete [shostak](0.07 s)
round_under_error.....................proved - complete [shostak](0.34 s)
round_under_near......................proved - complete [shostak](0.38 s)
round_under_pos.......................proved - complete [shostak](0.21 s)
round_under_neg.......................proved - complete [shostak](0.18 s)
round_under_zero......................proved - complete [shostak](0.48 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (3.03 s)
Proof summary for theory fp_round_aux
Exp_of_TCC1...........................proved - complete [shostak](0.02 s)
Exp_of_TCC2...........................proved - complete [shostak](0.06 s)
Exp_of_TCC3...........................proved - complete [shostak](0.09 s)
Exp_of_correct_TCC1...................proved - complete [shostak](0.02 s)
Exp_of_correct........................proved - complete [shostak](0.19 s)
significand_TCC1......................proved - complete [shostak](0.03 s)
significand_TCC2......................proved - complete [shostak](0.09 s)
real_components_TCC1..................proved - complete [shostak](0.03 s)
real_components.......................proved - complete [shostak](0.20 s)
abs_real_components...................proved - complete [shostak](0.15 s)
Exp_of_unique_TCC1....................proved - complete [shostak](0.07 s)
Exp_of_unique_TCC2....................proved - complete [shostak](0.07 s)
Exp_of_unique.........................proved - complete [shostak](0.11 s)
posreal_exponent......................proved - complete [shostak](0.17 s)
real_exponent.........................proved - complete [shostak](0.11 s)
scale_TCC1............................proved - complete [shostak](0.03 s)
scale_TCC2............................proved - complete [shostak](0.06 s)
scale_TCC3............................proved - complete [shostak](0.07 s)
scale_correct_TCC1....................proved - complete [shostak](0.02 s)
scale_correct_TCC2....................proved - complete [shostak](0.05 s)
scale_correct_TCC3....................proved - complete [shostak](0.05 s)
scale_correct.........................proved - complete [shostak](0.16 s)
round_scaled_TCC1.....................proved - complete [shostak](0.06 s)
round_scaled_TCC2.....................proved - complete [shostak](0.06 s)
truncate_TCC1.........................proved - complete [shostak](0.03 s)
truncate_shift........................proved - complete [shostak](0.15 s)
Exp_of_shift..........................proved - complete [shostak](0.21 s)
scale_shift...........................proved - complete [shostak](0.06 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (2.42 s)
Proof summary for theory round
round_to_even0........................proved - complete [shostak](0.08 s)
round_to_even1........................proved - complete [shostak](0.16 s)
round_to_even2........................proved - complete [shostak](0.24 s)
round1................................proved - complete [shostak](0.23 s)
round_int.............................proved - complete [shostak](0.12 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.83 s)
Proof summary for theory IEEE_854_fp_int
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory arithmetic_ops
apply_TCC1............................proved - complete [shostak](0.36 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.36 s)
Proof summary for theory comparison1
n_value_TCC1..........................proved - complete [shostak](0.03 s)
n_value_TCC2..........................proved - complete [shostak](0.02 s)
fp_compare_TCC1.......................proved - complete [shostak](0.03 s)
fp_compare_TCC2.......................proved - complete [shostak](0.03 s)
posinf_ge.............................proved - complete [shostak](0.25 s)
NaN_unordered.........................proved - complete [shostak](0.03 s)
eq_def................................proved - complete [shostak](0.09 s)
ne_def................................proved - complete [shostak](0.10 s)
gt_def................................proved - complete [shostak](0.07 s)
ge_def................................proved - complete [shostak](0.11 s)
lt_def................................proved - complete [shostak](0.08 s)
le_def................................proved - complete [shostak](0.11 s)
un_def................................proved - complete [shostak](0.03 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.98 s)
Proof summary for theory infinity_arithmetic
fp_sub_inf_def_TCC1...................proved - complete [shostak](0.03 s)
fp_sub_inf_def........................proved - complete [shostak](0.09 s)
mult_sign_TCC1........................proved - complete [shostak](0.02 s)
mult_sign_TCC2........................proved - complete [shostak](0.02 s)
mult_sign_TCC3........................proved - complete [shostak](0.02 s)
mult_sign_TCC4........................proved - complete [shostak](0.02 s)
fp_div_inf_TCC1.......................proved - complete [shostak](0.02 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.22 s)
Proof summary for theory NaN_ops
mk_quiet_correct......................proved - complete [shostak](0.06 s)
fp_quiet_TCC1.........................proved - complete [shostak](0.04 s)
fp_signal_TCC1........................proved - complete [shostak](0.03 s)
NaN_ops_correct_TCC1..................proved - complete [shostak](0.16 s)
NaN_ops_correct.......................proved - complete [shostak](0.21 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.50 s)
Proof summary for theory IEEE_link
Significand_size_TCC1................proved - complete [shostak]( 0.02 s)
IMP_IEEE_854_TCC1....................proved - complete [shostak]( 0.03 s)
IMP_IEEE_854_TCC2....................proved - complete [shostak]( 0.03 s)
IMP_IEEE_854_TCC3....................proved - complete [shostak]( 0.02 s)
IMP_IEEE_854_TCC4....................proved - complete [shostak]( 0.02 s)
IMP_IEEE_854_TCC5....................proved - complete [shostak]( 0.01 s)
b_TCC1...............................proved - complete [shostak]( 0.04 s)
IEEE_to_float_TCC1...................proved - complete [shostak]( 0.02 s)
IEEE_to_float_TCC2...................proved - complete [shostak]( 0.03 s)
IEEE_to_float_TCC3...................proved - complete [shostak]( 0.03 s)
IEEE_to_float_TCC4...................proved - complete [shostak]( 0.63 s)
IEEE_to_float_TCC5...................proved - complete [shostak]( 0.02 s)
float_to_IEEE_TCC1...................proved - complete [shostak]( 0.03 s)
float_to_IEEE_TCC2...................proved - complete [shostak]( 1.03 s)
float_to_IEEE_TCC3...................proved - complete [shostak]( 0.05 s)
float_to_IEEE_TCC4...................proved - complete [shostak]( 0.03 s)
float_to_IEEE_TCC5...................proved - complete [shostak]( 7.12 s)
value_nonzero_bis_TCC1...............proved - complete [shostak]( 0.08 s)
value_nonzero_bis_TCC2...............proved - complete [shostak]( 0.02 s)
value_nonzero_bis....................proved - complete [shostak]( 0.13 s)
Sterbenz_bis.........................proved - complete [shostak]( 0.38 s)
Roundings_eq_pos_TCC1................proved - complete [shostak]( 0.04 s)
Roundings_eq_pos_TCC2................proved - complete [shostak]( 0.02 s)
Roundings_eq_pos.....................proved - incomplete [shostak]( 6.71 s)
Roundings_eq_neg_TCC1................proved - complete [shostak]( 0.02 s)
Roundings_eq_neg.....................proved - incomplete [shostak]( 4.15 s)
fp_round_opp_aux_TCC1................proved - complete [shostak]( 0.03 s)
fp_round_opp_aux_TCC2................proved - complete [shostak]( 0.03 s)
fp_round_opp_aux.....................proved - complete [shostak]( 0.33 s)
fp_round_opp_TCC1....................proved - complete [shostak]( 0.02 s)
fp_round_opp.........................proved - complete [shostak]( 1.76 s)
RND_EClosest2_TCC1...................proved - incomplete [shostak]( 0.47 s)
RND_EClosest2........................proved - incomplete [shostak]( 9.94 s)
Roundings_eq_1_TCC1..................proved - complete [shostak]( 0.02 s)
Roundings_eq_1_TCC2..................proved - complete [shostak]( 0.02 s)
Roundings_eq_1.......................proved - incomplete [shostak]( 0.32 s)
Roundings_eq_2_TCC1..................proved - complete [shostak]( 0.02 s)
Roundings_eq_2.......................proved - incomplete [shostak]( 0.21 s)
Roundings_eq_3_TCC1..................proved - complete [shostak]( 0.03 s)
Roundings_eq_3_TCC2..................proved - complete [shostak]( 0.03 s)
Roundings_eq_3.......................proved - incomplete [shostak](21.38 s)
Roundings_eq_4_TCC1..................proved - complete [shostak]( 0.02 s)
Roundings_eq_4.......................proved - incomplete [shostak]( 2.03 s)
RoundedModeNonDecreasing_bis_TCC1....proved - complete [shostak]( 0.03 s)
RoundedModeNonDecreasing_bis.........proved - incomplete [shostak]( 0.80 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (58.19 s)
Grand Totals: 569 proofs, 569 attempted, 569 succeeded (304.74 s);;; GC:;;; Finished GC
[ Dauer der Verarbeitung: 0.217 Sekunden
]
|
|
|
|
|
|
