|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
context_tactic.ML
Sprache: SML
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[961] Hlasm[2465] Haskell[2783]}Entwicklung
***
*** 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)
[ Seitenstruktur0.309Drucken
]
|
|
|
|
|
|
