Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[784] Hlasm[2270] Haskell[2610]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (17:33:11 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
ln_div................................proved - complete [shostak](0.11 s)
ln_expt_TCC1..........................proved - complete [shostak](0.01 s)
ln_expt...............................proved - complete [shostak](0.24 s)
ln_increasing.........................proved - complete [shostak](0.02 s)
ln_bij................................proved - complete [shostak](0.02 s)
large_ln..............................proved - complete [shostak](0.05 s)
ln_eq_0...............................proved - complete [shostak](0.01 s)
ln_ge_0...............................proved - complete [shostak](0.01 s)
ln_gt_0...............................proved - complete [shostak](0.02 s)
exp_TCC1..............................proved - complete [shostak](0.02 s)
exp_def...............................proved - complete [shostak](0.03 s)
exp_bij...............................proved - complete [shostak](0.00 s)
ln_exp................................proved - complete [shostak](0.01 s)
exp_ln................................proved - complete [shostak](0.02 s)
ln_e..................................proved - complete [shostak](0.00 s)
exp_int_TCC1..........................proved - complete [shostak](0.01 s)
exp_int...............................proved - complete [shostak](0.05 s)
exp_sum...............................proved - complete [shostak](0.12 s)
exp_diff..............................proved - complete [shostak](0.10 s)
exp_scal_TCC1.........................proved - complete [shostak](0.00 s)
exp_scal..............................proved - complete [shostak](0.09 s)
exp_0.................................proved - complete [shostak](0.04 s)
exp_1.................................proved - complete [shostak](0.00 s)
exp_neg...............................proved - complete [shostak](0.08 s)
expt_alt_def_TCC1.....................proved - complete [shostak](0.00 s)
expt_alt_def_TCC2.....................proved - complete [shostak](0.00 s)
expt_alt_def..........................proved - complete [shostak](0.04 s)
exp_strict_increasing.................proved - complete [shostak](0.02 s)
exp_increasing........................proved - complete [shostak](0.02 s)
e_bnds................................proved - complete [shostak](0.07 s)
large_exp.............................proved - complete [shostak](0.13 s)
small_exp.............................proved - complete [shostak](0.16 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (1.50 s)
Proof summary for theory expt
doublecaret_TCC1......................proved - complete [shostak](0.01 s)
hathat_sum_TCC1.......................proved - complete [shostak](0.01 s)
hathat_sum_TCC2.......................proved - complete [shostak](0.00 s)
hathat_sum............................proved - complete [shostak](0.15 s)
hathat_diff_TCC1......................proved - complete [shostak](0.00 s)
hathat_diff_TCC2......................proved - complete [shostak](0.03 s)
hathat_diff...........................proved - complete [shostak](0.13 s)
hathat_to_0_TCC1......................proved - complete [shostak](0.00 s)
hathat_to_0...........................proved - complete [shostak](0.01 s)
hathat_to_1_TCC1......................proved - complete [shostak](0.00 s)
hathat_to_1...........................proved - complete [shostak](0.03 s)
hathat_0..............................proved - complete [shostak](0.01 s)
hathat_1..............................proved - complete [shostak](0.01 s)
hathat_nat_TCC1.......................proved - complete [shostak](-.00 s)
hathat_nat............................proved - complete [shostak](0.08 s)
hathat_lt_cross_TCC1..................proved - complete [shostak](0.00 s)
hathat_lt_cross_TCC2..................proved - complete [shostak](0.02 s)
hathat_lt_cross.......................proved - complete [shostak](0.12 s)
hathat_gt_cross_TCC1..................proved - complete [shostak](0.02 s)
hathat_gt_cross.......................proved - complete [shostak](0.12 s)
hathat_eq_0_TCC1......................proved - complete [shostak](0.00 s)
hathat_eq_0...........................proved - complete [shostak](0.03 s)
hathat_eq_1_TCC1......................proved - complete [shostak](0.00 s)
hathat_eq_1...........................proved - complete [shostak](0.10 s)
hathat_div_TCC1.......................proved - complete [shostak](0.02 s)
hathat_div_TCC2.......................proved - complete [shostak](0.03 s)
hathat_div............................proved - complete [shostak](0.13 s)
hathat_abs_TCC1.......................proved - complete [shostak](0.01 s)
hathat_abs............................proved - complete [shostak](0.04 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (1.11 s)
Proof summary for theory hyperbolic
cosh_TCC1.............................proved - complete [shostak](0.40 s)
tanh_TCC1.............................proved - complete [shostak](0.01 s)
tanh_TCC2.............................proved - complete [shostak](0.23 s)
csch_TCC1.............................proved - complete [shostak](0.44 s)
sech_TCC1.............................proved - complete [shostak](0.04 s)
coth_TCC1.............................proved - complete [shostak](0.28 s)
coth_TCC2.............................proved - complete [shostak](0.35 s)
posreal_csch_TCC1.....................proved - complete [shostak](0.27 s)
posreal_coth_TCC1.....................proved - complete [shostak](0.59 s)
sinh_strict_increasing................proved - complete [shostak](0.17 s)
cosh_strict_increasing................proved - complete [shostak](0.66 s)
tanh_strict_increasing................proved - complete [shostak](0.68 s)
csch_strict_decreasing................proved - complete [shostak](0.09 s)
sech_strict_decreasing................proved - complete [shostak](0.06 s)
coth_strict_decreasing................proved - complete [shostak](0.15 s)
sinh_0................................proved - complete [shostak](0.05 s)
cosh_0................................proved - complete [shostak](0.04 s)
tanh_0................................proved - complete [shostak](0.03 s)
sech_0................................proved - complete [shostak](0.00 s)
cosh_sinh_one.........................proved - complete [shostak](0.22 s)
tanh_sech_one.........................proved - complete [shostak](0.17 s)
coth_csch_one.........................proved - complete [shostak](0.21 s)
cosh_plus_sinh........................proved - complete [shostak](0.07 s)
cosh_minus_sinh.......................proved - complete [shostak](0.07 s)
sinh_neg..............................proved - complete [shostak](0.03 s)
cosh_neg..............................proved - complete [shostak](0.08 s)
tanh_neg..............................proved - complete [shostak](0.04 s)
csch_neg..............................proved - complete [shostak](0.04 s)
sech_neg..............................proved - complete [shostak](0.01 s)
coth_neg..............................proved - complete [shostak](0.04 s)
sinh_sum..............................proved - complete [shostak](0.48 s)
sinh_diff.............................proved - complete [shostak](0.10 s)
cosh_sum..............................proved - complete [shostak](0.51 s)
cosh_diff.............................proved - complete [shostak](0.10 s)
tanh_sum_TCC1.........................proved - complete [shostak](0.34 s)
tanh_sum..............................proved - complete [shostak](1.02 s)
coth_sum_TCC1.........................proved - complete [shostak](0.12 s)
coth_sum..............................proved - complete [shostak](0.50 s)
sinh_half_TCC1........................proved - complete [shostak](0.01 s)
sinh_half.............................proved - complete [shostak](0.76 s)
cosh_half_TCC1........................proved - complete [shostak](0.04 s)
cosh_half.............................proved - complete [shostak](0.55 s)
tanh_half1_TCC1.......................proved - complete [shostak](0.02 s)
tanh_half1_TCC2.......................proved - complete [shostak](0.07 s)
tanh_half1............................proved - complete [shostak](0.41 s)
tanh_half2............................proved - complete [shostak](0.34 s)
tanh_half3............................proved - complete [shostak](0.33 s)
sinh2x................................proved - complete [shostak](0.28 s)
sinh2x_B_TCC1.........................proved - complete [shostak](0.05 s)
sinh2x_B..............................proved - complete [shostak](0.99 s)
cosh2x................................proved - complete [shostak](0.30 s)
cosh2x_B..............................proved - complete [shostak](0.07 s)
cosh2x_C..............................proved - complete [shostak](0.08 s)
tanh2x................................proved - complete [shostak](0.52 s)
sinh3x_TCC1...........................proved - complete [shostak](0.00 s)
sinh3x................................proved - complete [shostak](0.24 s)
cosh3x................................proved - complete [shostak](0.26 s)
sinh4x................................proved - complete [shostak](0.24 s)
cosh4x_TCC1...........................proved - complete [shostak](0.01 s)
cosh4x................................proved - complete [shostak](0.28 s)
sinh_times_sinh.......................proved - complete [shostak](0.09 s)
cosh_times_cosh.......................proved - complete [shostak](0.12 s)
sinh_times_cosh.......................proved - complete [shostak](0.11 s)
sum_sinh..............................proved - complete [shostak](0.13 s)
diff_sinh.............................proved - complete [shostak](0.12 s)
sum_cosh..............................proved - complete [shostak](0.17 s)
diff_cosh.............................proved - complete [shostak](0.12 s)
sum_tanh_TCC1.........................proved - complete [shostak](0.03 s)
sum_tanh..............................proved - complete [shostak](0.10 s)
sum_coth_TCC1.........................proved - complete [shostak](0.04 s)
sum_coth..............................proved - complete [shostak](0.24 s)
diff_sinh_sq..........................proved - complete [shostak](1.05 s)
diff_cosh_sq..........................proved - complete [shostak](0.08 s)
sum_cosh_sinh_sq......................proved - complete [shostak](0.19 s)
hyperbolic_deMoivre_TCC1..............proved - complete [shostak](0.03 s)
hyperbolic_deMoivre...................proved - complete [shostak](0.07 s)
sinh_series_n_TCC1....................proved - complete [shostak](0.00 s)
sinh_series_n_TCC2....................proved - complete [shostak](0.05 s)
sinh_taylors_TCC1.....................proved - complete [shostak](0.06 s)
asinh_TCC1............................proved - complete [shostak](0.16 s)
acosh_TCC1............................proved - complete [shostak](0.03 s)
acosh_TCC2............................proved - complete [shostak](0.08 s)
acosh_TCC3............................proved - complete [shostak](0.29 s)
atanh_TCC1............................proved - complete [shostak](0.01 s)
atanh_TCC2............................proved - complete [shostak](0.06 s)
sinh_bij..............................proved - complete [shostak](0.39 s)
cosh_bij..............................proved - complete [shostak](0.45 s)
tanh_bij..............................proved - complete [shostak](0.64 s)
csch_bij..............................proved - complete [shostak](0.19 s)
sech_bij..............................proved - complete [shostak](0.17 s)
coth_bij..............................proved - complete [shostak](0.21 s)
asinh_alt_def.........................proved - complete [shostak](0.37 s)
asinh_sinh............................proved - complete [shostak](0.02 s)
sinh_asinh............................proved - complete [shostak](0.93 s)
asinh_strict_increasing...............proved - complete [shostak](0.03 s)
asinh_bij.............................proved - complete [shostak](0.01 s)
atanhF_TCC1...........................proved - complete [shostak](0.08 s)
atanhD_TCC1...........................proved - complete [shostak](0.07 s)
atanhND_TCC1..........................proved - complete [shostak](0.10 s)
atanh_series_term_TCC1................proved - complete [shostak](0.06 s)
atanh_series_TCC1.....................proved - complete [shostak](0.03 s)
atanh_series_TCC2.....................proved - complete [shostak](0.18 s)
atanh_series_TCC3.....................proved - complete [shostak](0.22 s)
Theory totals: 103 formulas, 103 attempted, 103 succeeded (22.06 s)
Proof summary for theory taylor_help
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory exp_series
exp_estimate_TCC1.....................proved - complete [shostak](0.00 s)
exp_estimate_TCC2.....................proved - complete [shostak](0.01 s)
exp_taylors_TCC1......................proved - complete [shostak](0.02 s)
exp_taylors_err_TCC1..................proved - complete [shostak](0.02 s)
exp_taylors_err.......................proved - complete [shostak](0.89 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.94 s)
Proof summary for theory ln_series
ln_estimate_TCC1......................proved - complete [shostak](0.01 s)
ln_estimate_TCC2......................proved - complete [shostak](0.00 s)
ln_estimate_TCC3......................proved - complete [shostak](0.01 s)
ln_taylors_TCC1.......................proved - complete [shostak](0.01 s)
ln_taylors_TCC2.......................proved - complete [shostak](0.06 s)
ln_taylors_TCC3.......................proved - complete [shostak](0.03 s)
lnp1_TCC1.............................proved - complete [shostak](0.07 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.19 s)
Proof summary for theory exp_approx
exp_neg_le1_bounds....................proved - complete [shostak](2.07 s)
exp_neg_le1_ub_strict_decreasing_n....proved - complete [shostak](1.14 s)
exp_neg_le1_lb_strict_increasing_n....proved - complete [shostak](1.07 s)
exp_neg_le1_lb_pos....................proved - complete [shostak](0.65 s)
exp_neg_ub_TCC1.......................proved - complete [shostak](0.04 s)
exp_neg_ub_TCC2.......................proved - complete [shostak](0.06 s)
exp_neg_ub_TCC3.......................proved - complete [shostak](0.19 s)
exp_neg_lb_TCC1.......................proved - complete [shostak](0.06 s)
exp_neg_lb_TCC2.......................proved - complete [shostak](0.17 s)
exp_neg_bounds........................proved - complete [shostak](0.20 s)
exp_ub_TCC1...........................proved - complete [shostak](0.01 s)
exp_ub_TCC2...........................proved - complete [shostak](0.00 s)
exp_bounds............................proved - complete [shostak](0.23 s)
e_bounds..............................proved - complete [shostak](0.01 s)
e_bounds2.............................proved - complete [shostak](0.80 s)
e_bound...............................proved - complete [shostak](0.02 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (6.71 s)
Proof summary for theory ln_approx
ln_le2_bounds_TCC1....................proved - complete [shostak](0.03 s)
ln_le2_bounds.........................proved - complete [shostak](0.47 s)
ln_gt1_lb_TCC1........................proved - complete [shostak](0.00 s)
ln_gt1_bounds_TCC1....................proved - complete [shostak](0.01 s)
ln_gt1_bounds_TCC2....................proved - complete [shostak](0.01 s)
ln_gt1_bounds.........................proved - complete [shostak](0.43 s)
ln_lb_TCC1............................proved - complete [shostak](0.04 s)
ln_lb_TCC2............................proved - complete [shostak](0.01 s)
ln_bounds.............................proved - complete [shostak](0.11 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.10 s)
Proof summary for theory ln_exp_series_alt
ln_estimate_TCC1......................proved - complete [shostak](0.01 s)
ln_estimate_TCC2......................proved - complete [shostak](0.01 s)
ln_estimate_TCC3......................proved - complete [shostak](0.01 s)
ln_estimate_scaf4_TCC1................proved - complete [shostak](0.01 s)
ln_estimate_scaf4_TCC2................proved - complete [shostak](0.00 s)
ln_estimate_scaf4_TCC3................proved - complete [shostak](0.02 s)
ln_estimate_scaf4.....................proved - complete [shostak](0.41 s)
ln_estimate_scaf5_TCC1................proved - complete [shostak](0.01 s)
ln_estimate_scaf5_TCC2................proved - complete [shostak](0.03 s)
ln_estimate_scaf5.....................proved - complete [shostak](0.09 s)
ln_estimate_bnd_TCC1..................proved - complete [shostak](0.00 s)
ln_estimate_bnd_TCC2..................proved - complete [shostak](0.01 s)
ln_estimate_bnd_TCC3..................proved - complete [shostak](0.10 s)
lnT_TCC1..............................proved - complete [shostak](0.02 s)
lnT_TCC2..............................proved - complete [shostak](0.26 s)
ln_taylors_TCC1.......................proved - complete [shostak](0.00 s)
ln_taylors_TCC2.......................proved - complete [shostak](0.06 s)
ln_taylors_TCC3.......................proved - complete [shostak](0.04 s)
expT_TCC1.............................proved - complete [shostak](0.01 s)
exp_taylors_TCC1......................proved - complete [shostak](0.00 s)
exp_estimate_bnd_TCC1.................proved - complete [shostak](0.01 s)
exp_estimate_bnd......................proved - complete [shostak](0.92 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (2.02 s)
Proof summary for theory ln_exp_ineq
ln_ineq1_TCC1.........................proved - complete [shostak](0.01 s)
ln_ineq1_TCC2.........................proved - complete [shostak](0.00 s)
ln_ineq2_TCC1.........................proved - complete [shostak](0.01 s)
ln_ineq2_TCC2.........................proved - complete [shostak](0.01 s)
ln_ineq2..............................proved - complete [shostak](0.08 s)
ln_ineq3_TCC1.........................proved - complete [shostak](0.03 s)
ln_ineq4..............................proved - complete [shostak](0.05 s)
ln_ineq5..............................proved - complete [shostak](0.21 s)
ln_ineq6_TCC1.........................proved - complete [shostak](0.01 s)
ln_ineq6_TCC2.........................proved - complete [shostak](0.02 s)
ln_ineq6..............................proved - complete [shostak](0.20 s)
exp_ineq1_TCC1........................proved - complete [shostak](0.00 s)
exp_ineq1.............................proved - complete [shostak](0.08 s)
exp_ineq2.............................proved - complete [shostak](0.06 s)
exp_ineq3.............................proved - complete [shostak](0.13 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.90 s)
Grand Totals: 238 proofs, 238 attempted, 238 succeeded (36.53 s)
[ Dauer der Verarbeitung: 0.188 Sekunden
]
