Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


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  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik