| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: majority_seq.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[961] Hlasm[2465] Haskell[2783]}zum Wurzelverzeichnis wechseln *** *** top (18:2:54 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 ln_exp conn_posreal..........................proved - complete [shostak](0.07 s) one_over_t_cont.......................proved - complete [shostak](0.30 s) ln_prep_TCC1..........................proved - complete [shostak](0.04 s) ln_prep_TCC2..........................proved - complete [shostak](0.04 s) ln_prep...............................proved - incomplete [shostak](0.07 s) ln_TCC1...............................proved - incomplete [shostak](0.03 s) ln_derivable_TCC1.....................proved - complete [shostak](0.02 s) ln_derivable..........................proved - incomplete [shostak](0.05 s) ln_continuous.........................proved - incomplete [shostak](0.28 s) ln_1..................................proved - incomplete [shostak](0.03 s) ln_mult...............................proved - incomplete [shostak](0.71 s) ln_div................................proved - incomplete [shostak](0.11 s) ln_expt_TCC1..........................proved - complete [shostak](0.02 s) ln_expt...............................proved - incomplete [shostak](0.27 s) ln_strict_increasing..................proved - incomplete [shostak](0.07 s) ln_increasing.........................proved - incomplete [shostak](0.03 s) ln_image_all..........................proved - incomplete [shostak](0.18 s) ln_bij................................proved - incomplete [shostak](0.04 s) large_ln..............................proved - incomplete [shostak](0.07 s) ln_eq_0...............................proved - incomplete [shostak](0.03 s) ln_ge_0...............................proved - incomplete [shostak](0.02 s) ln_gt_0...............................proved - incomplete [shostak](0.02 s) exp_TCC1..............................proved - incomplete [shostak](0.03 s) exp_def...............................proved - incomplete [shostak](0.04 s) exp_bij...............................proved - incomplete [shostak](0.02 s) ln_exp................................proved - incomplete [shostak](0.02 s) exp_ln................................proved - incomplete [shostak](0.03 s) ln_e..................................proved - incomplete [shostak](0.02 s) ln_2_bnds.............................proved - incomplete [shostak](0.16 s) exp_int_TCC1..........................proved - incomplete [shostak](0.02 s) exp_int...............................proved - incomplete [shostak](0.07 s) exp_sum...............................proved - incomplete [shostak](0.14 s) exp_diff..............................proved - incomplete [shostak](0.12 s) exp_scal_TCC1.........................proved - incomplete [shostak](0.02 s) exp_scal..............................proved - incomplete [shostak](0.10 s) exp_0.................................proved - incomplete [shostak](0.05 s) exp_1.................................proved - incomplete [shostak](0.02 s) exp_neg...............................proved - incomplete [shostak](0.11 s) expt_alt_def_TCC1.....................proved - complete [shostak](0.03 s) expt_alt_def_TCC2.....................proved - complete [shostak](0.02 s) expt_alt_def..........................proved - incomplete [shostak](0.05 s) exp_strict_increasing.................proved - incomplete [shostak](0.03 s) exp_increasing........................proved - incomplete [shostak](0.04 s) exp_continuous........................proved - incomplete [shostak](0.77 s) exp_deriv_TCC1........................proved - complete [shostak](0.02 s) exp_deriv_TCC2........................proved - complete [shostak](0.01 s) exp_deriv.............................proved - incomplete [shostak](0.15 s) e_bnds................................proved - incomplete [shostak](0.09 s) large_exp.............................proved - incomplete [shostak](0.15 s) small_exp.............................proved - incomplete [shostak](0.18 s) Theory totals: 50 formulas, 50 attempted, 50 succeeded (5.02 s) Proof summary for theory expt doublecaret_TCC1......................proved - complete [shostak](0.02 s) hathat_sum_TCC1.......................proved - complete [shostak](0.03 s) hathat_sum_TCC2.......................proved - complete [shostak](0.02 s) hathat_sum............................proved - incomplete [shostak](0.17 s) hathat_diff_TCC1......................proved - complete [shostak](0.03 s) hathat_diff_TCC2......................proved - incomplete [shostak](0.05 s) hathat_diff...........................proved - incomplete [shostak](0.14 s) hathat_to_0_TCC1......................proved - complete [shostak](0.02 s) hathat_to_0...........................proved - incomplete [shostak](0.02 s) hathat_to_1_TCC1......................proved - complete [shostak](0.02 s) hathat_to_1...........................proved - incomplete [shostak](0.05 s) hathat_0..............................proved - incomplete [shostak](0.03 s) hathat_1..............................proved - incomplete [shostak](0.03 s) hathat_nat_TCC1.......................proved - complete [shostak](0.02 s) hathat_nat............................proved - incomplete [shostak](0.10 s) hathat_lt_cross_TCC1..................proved - complete [shostak](0.02 s) hathat_lt_cross_TCC2..................proved - incomplete [shostak](0.04 s) hathat_lt_cross.......................proved - incomplete [shostak](0.14 s) hathat_gt_cross_TCC1..................proved - incomplete [shostak](0.05 s) hathat_gt_cross.......................proved - incomplete [shostak](0.14 s) hathat_eq_0_TCC1......................proved - complete [shostak](0.02 s) hathat_eq_0...........................proved - incomplete [shostak](0.05 s) hathat_eq_1_TCC1......................proved - complete [shostak](0.02 s) hathat_eq_1...........................proved - incomplete [shostak](0.11 s) hathat_cross_TCC1.....................proved - incomplete [shostak](0.09 s) hathat_cross..........................proved - incomplete [shostak](0.06 s) hathat_mult_TCC1......................proved - complete [shostak](0.02 s) hathat_mult_TCC2......................proved - incomplete [shostak](0.06 s) hathat_mult_TCC3......................proved - complete [shostak](0.02 s) hathat_mult...........................proved - incomplete [shostak](0.10 s) hathat_div_TCC1.......................proved - complete [shostak](0.04 s) hathat_div_TCC2.......................proved - incomplete [shostak](0.13 s) hathat_div............................proved - incomplete [shostak](0.14 s) hathat_abs_TCC1.......................proved - complete [shostak](0.04 s) hathat_abs............................proved - incomplete [shostak](0.06 s) hathat_sum_posreal_TCC1...............proved - complete [shostak](0.02 s) hathat_sum_posreal....................proved - incomplete [shostak](0.18 s) hathat_diff_posreal_TCC1..............proved - incomplete [shostak](0.12 s) hathat_diff_posreal_TCC2..............proved - complete [shostak](0.02 s) hathat_diff_posreal...................proved - incomplete [shostak](0.15 s) hathat_cont...........................proved - incomplete [shostak](0.32 s) Theory totals: 41 formulas, 41 attempted, 41 succeeded (2.92 s) Proof summary for theory hyperbolic noa_abs_lt1.........................proved - complete [shostak]( 0.09 s) noa_posreal_gt1.....................proved - complete [shostak]( 0.04 s) conn_abs_lt1........................proved - complete [shostak]( 0.03 s) conn_real...........................proved - complete [shostak]( 0.02 s) deriv_domain_abs_lt1................proved - complete [shostak]( 0.03 s) deriv_domain_posreal_gt1............proved - complete [shostak]( 0.10 s) cosh_TCC1...........................proved - incomplete [shostak]( 0.39 s) tanh_TCC1...........................proved - incomplete [shostak]( 0.02 s) tanh_TCC2...........................proved - incomplete [shostak]( 0.27 s) csch_TCC1...........................proved - incomplete [shostak]( 0.46 s) sech_TCC1...........................proved - incomplete [shostak]( 0.06 s) coth_TCC1...........................proved - incomplete [shostak]( 0.29 s) coth_TCC2...........................proved - incomplete [shostak]( 0.39 s) posreal_csch_TCC1...................proved - incomplete [shostak]( 0.29 s) posreal_coth_TCC1...................proved - incomplete [shostak]( 1.31 s) sinh_strict_increasing..............proved - incomplete [shostak]( 0.18 s) cosh_strict_increasing..............proved - incomplete [shostak]( 0.69 s) tanh_strict_increasing..............proved - incomplete [shostak]( 0.71 s) csch_strict_decreasing..............proved - incomplete [shostak]( 0.11 s) sech_strict_decreasing..............proved - incomplete [shostak]( 0.08 s) coth_strict_decreasing..............proved - incomplete [shostak]( 0.18 s) sinh_0..............................proved - incomplete [shostak]( 0.06 s) cosh_0..............................proved - incomplete [shostak]( 0.07 s) tanh_0..............................proved - incomplete [shostak]( 0.05 s) sech_0..............................proved - incomplete [shostak]( 0.02 s) cosh_sinh_one.......................proved - incomplete [shostak]( 0.26 s) tanh_sech_one.......................proved - incomplete [shostak]( 0.19 s) coth_csch_one.......................proved - incomplete [shostak]( 0.23 s) cosh_plus_sinh......................proved - incomplete [shostak]( 0.09 s) cosh_minus_sinh.....................proved - incomplete [shostak]( 0.09 s) sinh_neg............................proved - incomplete [shostak]( 0.05 s) cosh_neg............................proved - incomplete [shostak]( 0.09 s) tanh_neg............................proved - incomplete [shostak]( 0.06 s) csch_neg............................proved - incomplete [shostak]( 0.06 s) sech_neg............................proved - incomplete [shostak]( 0.03 s) coth_neg............................proved - incomplete [shostak]( 0.06 s) sinh_sum............................proved - incomplete [shostak]( 0.52 s) sinh_diff...........................proved - incomplete [shostak]( 0.12 s) cosh_sum............................proved - incomplete [shostak]( 0.56 s) cosh_diff...........................proved - incomplete [shostak]( 0.11 s) tanh_sum_TCC1.......................proved - incomplete [shostak]( 0.39 s) tanh_sum............................proved - incomplete [shostak]( 1.03 s) coth_sum_TCC1.......................proved - incomplete [shostak]( 0.14 s) coth_sum............................proved - incomplete [shostak]( 0.55 s) sinh_half_TCC1......................proved - incomplete [shostak]( 0.03 s) sinh_half...........................proved - incomplete [shostak]( 0.85 s) cosh_half_TCC1......................proved - incomplete [shostak]( 0.06 s) cosh_half...........................proved - incomplete [shostak]( 0.61 s) tanh_half1_TCC1.....................proved - incomplete [shostak]( 0.03 s) tanh_half1_TCC2.....................proved - incomplete [shostak]( 0.09 s) tanh_half1..........................proved - incomplete [shostak]( 0.45 s) tanh_half2..........................proved - incomplete [shostak]( 0.36 s) tanh_half3..........................proved - incomplete [shostak]( 0.36 s) sinh2x..............................proved - incomplete [shostak]( 0.30 s) sinh2x_B_TCC1.......................proved - incomplete [shostak]( 0.07 s) sinh2x_B............................proved - incomplete [shostak]( 1.00 s) cosh2x..............................proved - incomplete [shostak]( 0.33 s) cosh2x_B............................proved - incomplete [shostak]( 0.09 s) cosh2x_C............................proved - incomplete [shostak]( 0.10 s) tanh2x..............................proved - incomplete [shostak]( 0.55 s) sinh3x_TCC1.........................proved - incomplete [shostak]( 0.02 s) sinh3x..............................proved - incomplete [shostak]( 0.25 s) cosh3x..............................proved - incomplete [shostak]( 0.28 s) sinh4x..............................proved - incomplete [shostak]( 0.25 s) cosh4x_TCC1.........................proved - incomplete [shostak]( 0.02 s) cosh4x..............................proved - incomplete [shostak]( 0.29 s) sinh_times_sinh.....................proved - incomplete [shostak]( 0.12 s) cosh_times_cosh.....................proved - incomplete [shostak]( 0.14 s) sinh_times_cosh.....................proved - incomplete [shostak]( 0.13 s) sum_sinh............................proved - incomplete [shostak]( 0.16 s) diff_sinh...........................proved - incomplete [shostak]( 0.14 s) sum_cosh............................proved - incomplete [shostak]( 0.19 s) diff_cosh...........................proved - incomplete [shostak]( 0.15 s) sum_tanh_TCC1.......................proved - incomplete [shostak]( 0.06 s) sum_tanh............................proved - incomplete [shostak]( 0.11 s) sum_coth_TCC1.......................proved - incomplete [shostak]( 0.06 s) sum_coth............................proved - incomplete [shostak]( 0.28 s) diff_sinh_sq........................proved - incomplete [shostak]( 1.07 s) diff_cosh_sq........................proved - incomplete [shostak]( 0.08 s) sum_cosh_sinh_sq....................proved - incomplete [shostak]( 0.21 s) hyperbolic_deMoivre_TCC1............proved - incomplete [shostak]( 0.04 s) hyperbolic_deMoivre.................proved - incomplete [shostak]( 0.10 s) sinh_derivable2_TCC1................proved - complete [shostak]( 0.02 s) sinh_derivable2_TCC2................proved - complete [shostak]( 0.02 s) sinh_derivable2.....................proved - incomplete [shostak]( 0.19 s) cosh_derivable2.....................proved - incomplete [shostak]( 0.28 s) tanh_derivable2.....................proved - incomplete [shostak]( 0.05 s) deriv_sinh_TCC1.....................proved - incomplete [shostak]( 0.02 s) deriv_sinh..........................proved - incomplete [shostak]( 0.44 s) deriv_cosh_TCC1.....................proved - incomplete [shostak]( 0.02 s) deriv_cosh..........................proved - incomplete [shostak]( 0.48 s) deriv_tanh_TCC1.....................proved - incomplete [shostak]( 0.02 s) deriv_tanh..........................proved - incomplete [shostak]( 0.30 s) sinh_series_n_TCC1..................proved - complete [shostak]( 0.03 s) sinh_series_n_TCC2..................proved - complete [shostak]( 0.07 s) sinh_taylors_TCC1...................proved - complete [shostak]( 0.02 s) sinh_taylors_TCC2...................proved - complete [shostak]( 0.08 s) sinh_taylors........................proved - incomplete [shostak]( 1.46 s) asinh_TCC1..........................proved - complete [shostak]( 0.18 s) acosh_TCC1..........................proved - complete [shostak]( 0.05 s) acosh_TCC2..........................proved - complete [shostak]( 0.10 s) acosh_TCC3..........................proved - incomplete [shostak]( 0.31 s) atanh_TCC1..........................proved - complete [shostak]( 0.02 s) atanh_TCC2..........................proved - complete [shostak]( 0.09 s) sinh_bij............................proved - incomplete [shostak]( 0.43 s) cosh_bij............................proved - incomplete [shostak]( 0.46 s) tanh_bij............................proved - incomplete [shostak]( 0.69 s) csch_bij............................proved - incomplete [shostak]( 0.20 s) sech_bij............................proved - incomplete [shostak]( 0.19 s) coth_bij............................proved - incomplete [shostak]( 0.23 s) asinh_alt_def.......................proved - incomplete [shostak]( 0.39 s) asinh_sinh..........................proved - incomplete [shostak]( 0.03 s) sinh_asinh..........................proved - incomplete [shostak]( 1.01 s) asinh_strict_increasing.............proved - incomplete [shostak]( 0.04 s) asinh_bij...........................proved - incomplete [shostak]( 0.03 s) asinh_derivable2....................proved - incomplete [shostak]( 0.47 s) acosh_derivable2_TCC1...............proved - complete [shostak]( 0.02 s) acosh_derivable2_TCC2...............proved - complete [shostak]( 0.10 s) acosh_derivable2_TCC3...............proved - complete [shostak]( 0.02 s) acosh_derivable2....................proved - incomplete [shostak]( 0.57 s) atanh_derivable2_TCC1...............proved - complete [shostak]( 0.03 s) atanh_derivable2_TCC2...............proved - complete [shostak]( 0.02 s) atanh_derivable2....................proved - incomplete [shostak]( 0.20 s) deriv_asinh_TCC1....................proved - incomplete [shostak]( 0.03 s) deriv_asinh.........................proved - incomplete [shostak]( 1.54 s) deriv_acosh_TCC1....................proved - incomplete [shostak]( 0.02 s) deriv_acosh_TCC2....................proved - complete [shostak]( 0.03 s) deriv_acosh_TCC3....................proved - complete [shostak]( 0.05 s) deriv_acosh.........................proved - incomplete [shostak]( 2.63 s) deriv_atanh_TCC1....................proved - incomplete [shostak]( 0.02 s) deriv_atanh_TCC2....................proved - complete [shostak]( 0.07 s) deriv_atanh.........................proved - incomplete [shostak]( 1.20 s) atanhF_TCC1.........................proved - complete [shostak]( 0.12 s) atanhD_TCC1.........................proved - complete [shostak]( 0.08 s) atanh_taylors_prep1.................proved - complete [shostak]( 0.45 s) atanh_taylors_prep2_TCC1............proved - complete [shostak]( 0.03 s) atanh_taylors_prep2_TCC2............proved - complete [shostak]( 0.08 s) atanh_taylors_prep2.................proved - complete [shostak]( 0.11 s) atanh_taylors_prep3_TCC1............proved - complete [shostak]( 0.02 s) atanh_taylors_prep3_TCC2............proved - complete [shostak]( 0.04 s) atanh_taylors_prep3.................proved - complete [shostak]( 0.77 s) atanh_taylors_prep4_TCC1............proved - complete [shostak]( 0.03 s) atanh_taylors_prep4_TCC2............proved - complete [shostak]( 0.08 s) atanh_taylors_prep4.................proved - complete [shostak]( 0.34 s) atanh_taylors_prep5_TCC1............proved - complete [shostak]( 0.04 s) atanh_taylors_prep5_TCC2............proved - complete [shostak]( 0.07 s) atanh_taylors_prep5.................proved - complete [shostak]( 0.55 s) atanhND_TCC1........................proved - complete [shostak]( 0.13 s) atanh_taylors_prep6_TCC1............proved - complete [shostak]( -0.50 s) atanh_taylors_prep6_TCC2............proved - complete [shostak]( 0.13 s) atanh_taylors_prep6.................proved - complete [shostak](141.05 s) atanh_taylors_prep7.................proved - complete [shostak]( 0.93 s) atanh_taylors_prep8_TCC1............proved - complete [shostak]( 0.02 s) atanh_taylors_prep8.................proved - complete [shostak]( 0.27 s) atanh_nderiv_TCC1...................proved - incomplete [shostak]( 0.38 s) atanh_nderiv_TCC2...................proved - complete [shostak]( 0.12 s) atanh_nderiv_TCC3...................proved - complete [shostak]( 0.12 s) atanh_nderiv_TCC4...................proved - complete [shostak]( 0.11 s) atanh_nderiv........................proved - incomplete [shostak]( 0.50 s) atanh_nderiv_0_TCC1.................proved - complete [shostak]( 0.08 s) atanh_nderiv_0......................proved - incomplete [shostak]( 1.02 s) atanh_n_times_derivable.............proved - incomplete [shostak]( 0.28 s) atanh_series_term_TCC1..............proved - complete [shostak]( 0.09 s) atanh_series_eqv_TCC1...............proved - complete [shostak]( 0.08 s) atanh_series_eqv_TCC2...............proved - incomplete [shostak]( 0.09 s) atanh_series_eqv_TCC3...............proved - complete [shostak]( 0.07 s) atanh_series_eqv....................proved - incomplete [shostak]( 0.91 s) atanh_taylors_TCC1..................proved - complete [shostak]( 0.02 s) atanh_taylors_TCC2..................proved - incomplete [shostak]( 0.08 s) atanh_taylors_TCC3..................proved - complete [shostak]( 0.09 s) atanh_taylors.......................proved - incomplete [shostak]( 0.42 s) atanh_series_TCC1...................proved - complete [shostak]( 0.06 s) atanh_series_TCC2...................proved - complete [shostak]( 0.21 s) atanh_series........................proved - incomplete [shostak]( 5.62 s) Theory totals: 174 formulas, 174 attempted, 174 succeeded (190.21 s) Proof summary for theory exp_series IMP_taylor_series_TCC1................proved - complete [shostak](0.03 s) IMP_taylor_series_TCC2................proved - complete [shostak](0.01 s) IMP_taylor_series_TCC3................proved - complete [shostak](0.02 s) IMP_taylor_series_TCC4................proved - complete [shostak](0.02 s) nderiv_exp_TCC1.......................proved - complete [shostak](0.02 s) nderiv_exp............................proved - incomplete [shostak](0.04 s) exp_inf_deriv.........................proved - incomplete [shostak](0.04 s) exp_series_prep_TCC1..................proved - incomplete [shostak](0.05 s) exp_series_prep_TCC2..................proved - incomplete [shostak](0.02 s) exp_series_prep.......................proved - incomplete [shostak](1.22 s) conv_exp..............................proved - incomplete [shostak](0.16 s) exp_series_TCC1.......................proved - incomplete [shostak](0.02 s) exp_series............................proved - incomplete [shostak](0.51 s) exp_estimate_TCC1.....................proved - complete [shostak](0.02 s) exp_estimate_TCC2.....................proved - complete [shostak](0.03 s) exp_estimate_TCC3.....................proved - complete [shostak](0.02 s) exp_taylors_TCC1......................proved - complete [shostak](0.04 s) exp_taylors...........................proved - incomplete [shostak](0.56 s) exp_taylors_err_TCC1..................proved - complete [shostak](0.04 s) exp_taylors_err.......................proved - incomplete [shostak](0.99 s) exp_estimate_increasing...............proved - complete [shostak](1.72 s) exp_estimate_positive.................proved - complete [shostak](1.29 s) exp_estimate_0........................proved - complete [shostak](0.11 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (6.98 s) Proof summary for theory convergence_special conv_1_div_n..........................proved - complete [shostak](0.22 s) conv_x_to_1_div_n_TCC1................proved - complete [shostak](0.05 s) conv_x_to_1_div_n.....................proved - incomplete [shostak](0.19 s) conv_x_to_n_TCC1......................proved - complete [shostak](0.03 s) conv_x_to_n...........................proved - incomplete [shostak](0.34 s) expt_abs_gt_TCC1......................proved - complete [shostak](0.02 s) expt_abs_gt_TCC2......................proved - complete [shostak](0.03 s) expt_abs_gt...........................proved - complete [shostak](0.19 s) conv_x_to_n_div_fact..................proved - incomplete [shostak](1.83 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (2.89 s) Proof summary for theory ln_series noa_posreal..........................proved - complete [shostak]( 0.04 s) noa_gt_m1............................proved - complete [shostak]( 0.04 s) conn_gt_m1...........................proved - complete [shostak]( 0.03 s) conn_posreal.........................proved - complete [shostak]( 0.03 s) conn_abslt1..........................proved - complete [shostak]( 0.08 s) noa_abslt1...........................proved - complete [shostak]( 0.08 s) deriv_domain_gtm1....................proved - complete [shostak]( 0.12 s) nderiv_ln_TCC1.......................proved - complete [shostak]( 0.02 s) nderiv_ln_TCC2.......................proved - complete [shostak]( 0.02 s) nderiv_ln............................proved - incomplete [shostak]( 0.99 s) ln_nderiv_TCC1.......................proved - incomplete [shostak]( 0.03 s) ln_nderiv_TCC2.......................proved - complete [shostak]( 0.03 s) ln_nderiv_TCC3.......................proved - complete [shostak]( 0.03 s) ln_nderiv............................proved - incomplete [shostak]( 0.58 s) IMP_taylor_series_TCC1...............proved - complete [shostak]( 0.02 s) IMP_taylor_series_TCC2...............proved - complete [shostak]( 0.02 s) IMP_taylor_series_TCC3...............proved - complete [shostak]( 0.11 s) IMP_taylor_series_TCC4...............proved - complete [shostak]( 0.05 s) IMP_taylor_series_TCC5...............proved - complete [shostak]( 0.04 s) ln_estimate_TCC1.....................proved - complete [shostak]( 0.02 s) ln_estimate_TCC2.....................proved - complete [shostak]( 0.03 s) ln_estimate_TCC3.....................proved - complete [shostak]( 0.02 s) ln_estimate_TCC4.....................proved - complete [shostak]( 0.02 s) ln_taylors_TCC1......................proved - complete [shostak]( 0.03 s) ln_taylors_TCC2......................proved - complete [shostak]( 0.03 s) ln_taylors_TCC3......................proved - complete [shostak]( 0.04 s) ln_taylors_TCC4......................proved - complete [shostak]( 0.08 s) ln_taylors_TCC5......................proved - complete [shostak]( 0.03 s) ln_taylors...........................proved - incomplete [shostak]( 1.97 s) ln_estimate_error_bound_TCC1.........proved - complete [shostak]( 0.02 s) ln_estimate_error_bound..............proved - incomplete [shostak]( 0.94 s) lnp1_TCC1............................proved - complete [shostak]( 0.08 s) lnp1_TCC2............................proved - incomplete [shostak]( 0.11 s) lnp1_TCC3............................proved - complete [shostak]( 0.03 s) lnp1.................................proved - incomplete [shostak]( 0.02 s) ln_estimate_increasing_odd...........proved - complete [shostak]( 3.87 s) ln_estimate_increasing_even..........proved - complete [shostak](10.79 s) lnp1_prep_TCC1.......................proved - complete [shostak]( 0.05 s) lnp1_prep_TCC2.......................proved - complete [shostak]( 0.02 s) lnp1_prep............................proved - incomplete [shostak]( 0.34 s) geom_neg_TCC1........................proved - complete [shostak]( 0.02 s) geom_neg_TCC2........................proved - complete [shostak]( 0.13 s) geom_neg_TCC3........................proved - complete [shostak]( 0.03 s) geom_neg.............................proved - complete [shostak]( 0.10 s) lnp1_conv............................proved - complete [shostak]( 0.69 s) int_geo_prep_TCC1....................proved - complete [shostak]( 0.03 s) int_geo_prep_TCC2....................proved - complete [shostak]( 0.10 s) int_geo_prep.........................proved - incomplete [shostak]( 0.37 s) int_geo_neg_TCC1.....................proved - incomplete [shostak]( 0.03 s) int_geo_neg..........................proved - incomplete [shostak]( 6.65 s) Theory totals: 50 formulas, 50 attempted, 50 succeeded (29.06 s) Proof summary for theory exp_approx exp_neg_le1_bounds....................proved - incomplete [shostak](1.80 s) exp_neg_le1_ub_strict_decreasing_n....proved - complete [shostak](1.25 s) exp_neg_le1_lb_pos....................proved - incomplete [shostak](0.55 s) exp_neg_ub_TCC1.......................proved - complete [shostak](0.07 s) exp_neg_ub_TCC2.......................proved - complete [shostak](0.08 s) exp_neg_ub_TCC3.......................proved - incomplete [shostak](0.22 s) exp_neg_lb_TCC1.......................proved - complete [shostak](0.08 s) exp_neg_lb_TCC2.......................proved - incomplete [shostak](0.20 s) exp_neg_bounds........................proved - incomplete [shostak](0.24 s) exp_ub_n_TCC1.........................proved - complete [shostak](0.04 s) exp_ub_n_TCC2.........................proved - complete [shostak](0.04 s) exp_bounds............................proved - incomplete [shostak](1.07 s) exp_range_test_TCC1...................proved - complete [shostak](0.09 s) exp_range_test_TCC2...................proved - complete [shostak](0.08 s) exp_range_test........................proved - complete [shostak](5.06 s) exp_range_test_lb_TCC1................proved - complete [shostak](0.11 s) exp_range_test_lb_TCC2................proved - complete [shostak](0.10 s) exp_range_test_lb.....................proved - complete [shostak](7.68 s) exp_neg_ub_increasing.................proved - incomplete [shostak](1.69 s) exp_neg_lb_increasing.................proved - incomplete [shostak](2.17 s) test_TCC1.............................proved - complete [shostak](0.11 s) test_TCC2.............................proved - complete [shostak](0.11 s) test..................................proved - incomplete [shostak](0.29 s) exp_ub_increasing.....................proved - incomplete [shostak](1.72 s) exp_lb_increasing.....................proved - incomplete [shostak](1.82 s) e_bounds..............................proved - incomplete [shostak](0.03 s) e_bounds2.............................proved - incomplete [shostak](0.89 s) e_bound...............................proved - incomplete [shostak](0.05 s) Theory totals: 28 formulas, 28 attempted, 28 succeeded (27.64 s) Proof summary for theory ln_approx ln_le2_bounds_TCC1....................proved - complete [shostak](0.05 s) ln_le2_bounds.........................proved - incomplete [shostak](0.59 s) ln_gt1_lb_TCC1........................proved - complete [shostak](0.02 s) ln_gt1_ub_increasing..................proved - incomplete [shostak](1.58 s) ln_gt1_lb_increasing..................proved - incomplete [shostak](1.93 s) ln_gt1_bounds_TCC1....................proved - complete [shostak](0.03 s) ln_gt1_bounds_TCC2....................proved - complete [shostak](0.03 s) ln_gt1_bounds.........................proved - incomplete [shostak](0.47 s) ln_lb_TCC1............................proved - complete [shostak](0.07 s) ln_lb_TCC2............................proved - complete [shostak](0.03 s) ln_lb_increasing......................proved - incomplete [shostak](0.88 s) ln_ub_increasing......................proved - incomplete [shostak](0.89 s) ln_bounds.............................proved - incomplete [shostak](0.14 s) floor_eq_log_nat_ge_1_TCC1............proved - complete [shostak](0.03 s) floor_eq_log_nat_ge_1_TCC2............proved - incomplete [shostak](0.03 s) floor_eq_log_nat_ge_1.................proved - incomplete [shostak](0.48 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (7.26 s) Proof summary for theory ln_exp_series_alt noa_posreal...........................proved - complete [shostak](0.05 s) conn_posreal..........................proved - complete [shostak](0.02 s) noa_gt_m1.............................proved - complete [shostak](0.04 s) conn_gt_m1............................proved - complete [shostak](0.03 s) deriv_domain_gtm1.....................proved - complete [shostak](0.10 s) nderiv_ln_TCC1........................proved - complete [shostak](0.02 s) nderiv_ln_TCC2........................proved - complete [shostak](0.05 s) nderiv_ln.............................proved - incomplete [shostak](0.96 s) ln_nderiv_TCC1........................proved - incomplete [shostak](0.02 s) ln_nderiv_TCC2........................proved - complete [shostak](0.03 s) ln_nderiv_TCC3........................proved - complete [shostak](0.03 s) ln_nderiv.............................proved - incomplete [shostak](0.64 s) ln_estimate_TCC1......................proved - complete [shostak](0.03 s) ln_estimate_TCC2......................proved - complete [shostak](0.02 s) ln_estimate_TCC3......................proved - complete [shostak](0.03 s) ln_estimate_TCC4......................proved - complete [shostak](0.03 s) ln_estimate_scaf1_TCC1................proved - complete [shostak](0.03 s) ln_estimate_scaf1.....................proved - complete [shostak](0.31 s) ln_estimate_scaf2_TCC1................proved - complete [shostak](0.03 s) ln_estimate_scaf2.....................proved - incomplete [shostak](0.09 s) ln_estimate_scaf3_TCC1................proved - complete [shostak](0.03 s) ln_estimate_scaf3_TCC2................proved - incomplete [shostak](0.02 s) ln_estimate_scaf3.....................proved - incomplete [shostak](0.09 s) ln_estimate_scaf4_TCC1................proved - complete [shostak](0.03 s) ln_estimate_scaf4_TCC2................proved - complete [shostak](0.02 s) ln_estimate_scaf4_TCC3................proved - complete [shostak](0.03 s) ln_estimate_scaf4.....................proved - complete [shostak](0.43 s) ln_estimate_scaf5_TCC1................proved - complete [shostak](0.03 s) ln_estimate_scaf5_TCC2................proved - complete [shostak](0.04 s) ln_estimate_scaf5.....................proved - complete [shostak](0.11 s) ln_estimate_scaf6.....................proved - complete [shostak](0.40 s) ln_estimate_scaf7_TCC1................proved - complete [shostak](0.04 s) ln_estimate_scaf7.....................proved - complete [shostak](1.01 s) ln_estimate_scaf8_TCC1................proved - complete [shostak](0.04 s) ln_estimate_scaf8_TCC2................proved - incomplete [shostak](0.04 s) ln_estimate_scaf8.....................proved - incomplete [shostak](0.62 s) ln_estimate_scaf9_TCC1................proved - incomplete [shostak](0.02 s) ln_estimate_scaf9.....................proved - incomplete [shostak](0.20 s) ln_estimate_scaf10_TCC1...............proved - complete [shostak](0.04 s) ln_estimate_scaf10....................proved - incomplete [shostak](3.05 s) ln_estimate_scaf11....................proved - incomplete [shostak](1.47 s) ln_estimate_bnd_TCC1..................proved - complete [shostak](0.03 s) ln_estimate_bnd_TCC2..................proved - complete [shostak](0.02 s) ln_estimate_bnd_TCC3..................proved - complete [shostak](0.11 s) ln_estimate_bnd.......................proved - incomplete [shostak](0.33 s) lnT_TCC1..............................proved - complete [shostak](0.04 s) lnT_TCC2..............................proved - complete [shostak](0.28 s) lnT_convergence.......................proved - incomplete [shostak](0.76 s) lnT_convergent........................proved - incomplete [shostak](0.05 s) ln_series_def_TCC1....................proved - incomplete [shostak](0.05 s) ln_series_def.........................proved - incomplete [shostak](0.06 s) ln_taylors_TCC1.......................proved - complete [shostak](0.02 s) ln_taylors_TCC2.......................proved - complete [shostak](0.02 s) ln_taylors_TCC3.......................proved - complete [shostak](0.04 s) ln_taylors_TCC4.......................proved - complete [shostak](0.07 s) ln_taylors_TCC5.......................proved - complete [shostak](0.06 s) ln_taylors............................proved - incomplete [shostak](1.24 s) nderiv_exp_TCC1.......................proved - complete [shostak](0.02 s) nderiv_exp_TCC2.......................proved - complete [shostak](0.03 s) nderiv_exp............................proved - incomplete [shostak](0.04 s) expT_TCC1.............................proved - complete [shostak](0.02 s) exp_taylors_TCC1......................proved - complete [shostak](0.03 s) exp_taylors_TCC2......................proved - complete [shostak](0.04 s) exp_taylors...........................proved - incomplete [shostak](0.48 s) exp_estimate_bnd_TCC1.................proved - complete [shostak](0.03 s) exp_estimate_bnd......................proved - incomplete [shostak](1.02 s) exp_series_scaf2_TCC1.................proved - complete [shostak](0.07 s) exp_series_scaf2......................proved - complete [shostak](0.34 s) exp_series_scaf3_TCC1.................proved - complete [shostak](0.07 s) exp_series_scaf3......................proved - complete [shostak](0.32 s) expT_convergence......................proved - incomplete [shostak](2.70 s) expT_convergent.......................proved - incomplete [shostak](0.03 s) exp_series_TCC1.......................proved - incomplete [shostak](0.02 s) exp_series............................proved - incomplete [shostak](0.04 s) Theory totals: 74 formulas, 74 attempted, 74 succeeded (18.81 s) Proof summary for theory ln_exp_ineq noa_posreal...........................proved - complete [shostak](0.05 s) conn_posreal..........................proved - complete [shostak](0.03 s) ln_ineq1_TCC1.........................proved - complete [shostak](0.02 s) ln_ineq1_TCC2.........................proved - complete [shostak](0.02 s) ln_ineq1..............................proved - incomplete [shostak](1.14 s) ln_ineq2_TCC1.........................proved - complete [shostak](0.03 s) ln_ineq2_TCC2.........................proved - incomplete [shostak](0.03 s) ln_ineq2..............................proved - incomplete [shostak](0.09 s) ln_ineq3_TCC1.........................proved - complete [shostak](0.05 s) ln_ineq3..............................proved - incomplete [shostak](5.32 s) ln_ineq4..............................proved - incomplete [shostak](0.06 s) ln_ineq5..............................proved - incomplete [shostak](0.27 s) ln_ineq6_TCC1.........................proved - complete [shostak](0.03 s) ln_ineq6_TCC2.........................proved - complete [shostak](0.04 s) ln_ineq6..............................proved - incomplete [shostak](0.24 s) exp_ineq1_TCC1........................proved - complete [shostak](0.02 s) exp_ineq1.............................proved - incomplete [shostak](0.10 s) exp_ineq2.............................proved - incomplete [shostak](0.08 s) exp_ineq3.............................proved - incomplete [shostak](0.18 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (7.79 s) Grand Totals: 484 proofs, 484 attempted, 484 succeeded (298.59 s) [ zur Elbe Produktseite wechseln0.200Quellennavigators ] |