| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: ln_exp_series_alt.pvs Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[607] Hlasm[2111] Haskell[2429]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (17:45:6 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 limit_vect_real cv_unique.............................proved - complete [shostak](0.93 s) cv_in_domain..........................proved - complete [shostak](0.16 s) cv_sum................................proved - complete [shostak](0.34 s) cv_neg................................proved - complete [shostak](0.19 s) cv_diff...............................proved - complete [shostak](0.06 s) cv_prod...............................proved - complete [shostak](0.50 s) cv_const..............................proved - complete [shostak](0.05 s) cv_scal...............................proved - complete [shostak](0.06 s) cv_inv................................proved - complete [shostak](0.45 s) cv_div................................proved - complete [shostak](0.13 s) lim_fun_lemma.........................proved - complete [shostak](0.04 s) lim_fun_def...........................proved - complete [shostak](0.05 s) convergence_equiv.....................proved - complete [shostak](0.05 s) convergent_in_domain..................proved - complete [shostak](0.08 s) lim_in_domain.........................proved - complete [shostak](0.04 s) sum_fun_convergent....................proved - complete [shostak](0.05 s) neg_fun_convergent....................proved - complete [shostak](0.04 s) diff_fun_convergent...................proved - complete [shostak](0.04 s) prod_fun_convergent...................proved - complete [shostak](0.05 s) const_fun_convergent..................proved - complete [shostak](0.08 s) scal_fun_convergent...................proved - complete [shostak](0.05 s) inv_fun_convergent....................proved - complete [shostak](0.06 s) div_fun_convergent....................proved - complete [shostak](0.06 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.03 s) lim_sum_fun...........................proved - complete [shostak](0.05 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.03 s) lim_neg_fun...........................proved - complete [shostak](0.03 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.03 s) lim_diff_fun..........................proved - complete [shostak](0.04 s) lim_prod_fun_TCC1.....................proved - complete [shostak](0.04 s) lim_prod_fun..........................proved - complete [shostak](0.06 s) lim_const_fun_TCC1....................proved - complete [shostak](0.03 s) lim_const_fun.........................proved - complete [shostak](0.04 s) lim_scal_fun_TCC1.....................proved - complete [shostak](0.04 s) lim_scal_fun..........................proved - complete [shostak](0.05 s) lim_inv_fun_TCC1......................proved - complete [shostak](0.04 s) lim_inv_fun...........................proved - complete [shostak](0.06 s) lim_div_fun_TCC1......................proved - complete [shostak](0.03 s) lim_div_fun...........................proved - complete [shostak](0.05 s) convergence_order.....................proved - complete [shostak](0.28 s) convergence_lower_bound...............proved - complete [shostak](0.09 s) convergence_upper_bound...............proved - complete [shostak](0.09 s) lim_le1...............................proved - complete [shostak](0.09 s) lim_ge1...............................proved - complete [shostak](0.05 s) lim_order1............................proved - complete [shostak](0.10 s) Theory totals: 45 formulas, 45 attempted, 45 succeeded (4.91 s) Proof summary for theory limit_vect cv_unique.............................proved - complete [shostak](0.09 s) cv_in_domain..........................proved - complete [shostak](0.04 s) cv_sum................................proved - complete [shostak](0.18 s) cv_neg................................proved - complete [shostak](0.07 s) cv_diff...............................proved - complete [shostak](0.04 s) cv_const..............................proved - complete [shostak](0.01 s) cv_scal...............................proved - complete [shostak](0.22 s) lim_TCC1..............................proved - complete [shostak](0.02 s) lim_fun_lemma.........................proved - complete [shostak](0.02 s) lim_fun_def...........................proved - complete [shostak](0.02 s) convergence_equiv.....................proved - complete [shostak](0.02 s) convergent_in_domain..................proved - complete [shostak](0.03 s) lim_in_domain.........................proved - complete [shostak](0.01 s) sum_fun_convergent....................proved - complete [shostak](0.01 s) neg_fun_convergent....................proved - complete [shostak](0.42 s) diff_fun_convergent...................proved - complete [shostak](0.02 s) const_fun_convergent..................proved - complete [shostak](0.05 s) scal_fun_convergent...................proved - complete [shostak](0.01 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s) lim_sum_fun...........................proved - complete [shostak](0.02 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.01 s) lim_neg_fun...........................proved - complete [shostak](0.01 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_diff_fun..........................proved - complete [shostak](0.01 s) lim_const_fun_TCC1....................proved - complete [shostak](0.01 s) lim_const_fun.........................proved - complete [shostak](0.01 s) lim_scal_fun_TCC1.....................proved - complete [shostak](0.00 s) lim_scal_fun..........................proved - complete [shostak](0.02 s) Theory totals: 28 formulas, 28 attempted, 28 succeeded (1.37 s) Proof summary for theory cont_vect continuity_def........................proved - complete [shostak](0.02 s) continuity_def2.......................proved - complete [shostak](0.02 s) sum_continuous_vv.....................proved - complete [shostak](0.03 s) diff_continuous_vv....................proved - complete [shostak](0.02 s) const_continuous_vv...................proved - complete [shostak](0.02 s) neg_continuous_vv.....................proved - complete [shostak](0.06 s) continuous_vv_fun_TCC1................proved - complete [shostak](0.01 s) sum_fun_continuous_vv.................proved - complete [shostak](0.09 s) diff_fun_continuous_vv................proved - complete [shostak](0.10 s) const_fun_continuous_vv...............proved - complete [shostak](0.01 s) neg_fun_continuous_vv.................proved - complete [shostak](0.05 s) sum_cont_fun..........................proved - complete [shostak](0.10 s) diff_cont_fun.........................proved - complete [shostak](0.09 s) const_cont_fun........................proved - complete [shostak](0.01 s) neg_cont_fun..........................proved - complete [shostak](0.05 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.68 s) Proof summary for theory metric_vect Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory deriv_sigma IMP_derivatives_TCC1..................proved - complete [shostak](-.00 s) IMP_derivatives_TCC2..................proved - complete [shostak](0.00 s) sigma_derivable_TCC1..................proved - complete [shostak](0.14 s) sigma_derivable_TCC2..................proved - complete [shostak](0.14 s) sigma_derivable_TCC3..................proved - complete [shostak](0.20 s) sigma_derivable.......................proved - complete [shostak](0.77 s) deriv_sigma_TCC1......................proved - complete [shostak](0.19 s) deriv_sigma_TCC2......................proved - complete [shostak](0.19 s) deriv_sigma_TCC3......................proved - complete [shostak](0.21 s) deriv_sigma_TCC4......................proved - complete [shostak](0.04 s) deriv_sigma_TCC5......................proved - complete [shostak](0.18 s) deriv_sigma_TCC6......................proved - complete [shostak](0.19 s) deriv_sigma_TCC7......................proved - complete [shostak](0.26 s) deriv_sigma_TCC8......................proved - complete [shostak](0.01 s) deriv_sigma...........................proved - complete [shostak](1.98 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (4.51 s) Proof summary for theory deriv_real_vect_def IMP_derivatives_TCC1..................proved - complete [shostak](0.00 s) IMP_derivatives_TCC2..................proved - complete [shostak](0.00 s) deriv_TCC1............................proved - complete [shostak](0.05 s) sum_derivable.........................proved - complete [shostak](0.07 s) diff_derivable........................proved - complete [shostak](0.06 s) neg_derivable.........................proved - complete [shostak](0.05 s) scal_derivable........................proved - complete [shostak](0.07 s) const_derivable.......................proved - complete [shostak](0.10 s) deriv_sum_TCC1........................proved - complete [shostak](0.04 s) deriv_sum.............................proved - complete [shostak](0.17 s) deriv_neg_TCC1........................proved - complete [shostak](0.03 s) deriv_neg.............................proved - complete [shostak](0.11 s) deriv_diff_TCC1.......................proved - complete [shostak](0.04 s) deriv_diff............................proved - complete [shostak](0.15 s) deriv_const_TCC1......................proved - complete [shostak](0.03 s) deriv_const...........................proved - complete [shostak](0.12 s) deriv_scal_TCC1.......................proved - complete [shostak](0.04 s) deriv_scal............................proved - complete [shostak](0.16 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (1.31 s) Proof summary for theory vect_fun_ops diff_function.........................proved - complete [shostak](0.07 s) negneg_function.......................proved - complete [shostak](0.04 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s) Proof summary for theory deriv_dot_prod IMP_derivatives_TCC1..................proved - complete [shostak](0.00 s) IMP_derivatives_TCC2..................proved - complete [shostak](0.00 s) dot_prod_derivable....................proved - complete [shostak](0.16 s) deriv_dot_prod_TCC1...................proved - complete [shostak](0.04 s) deriv_dot_prod........................proved - complete [shostak](0.72 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.92 s) Proof summary for theory deriv_real_vect IMP_deriv_real_vect_def_TCC1..........proved - complete [shostak](0.00 s) IMP_deriv_real_vect_def_TCC2..........proved - complete [shostak](0.00 s) deriv_TCC1............................proved - complete [shostak](0.04 s) sum_derivable_vfun....................proved - complete [shostak](0.17 s) neg_derivable_vfun....................proved - complete [shostak](0.11 s) diff_derivable_vfun...................proved - complete [shostak](0.17 s) dot_derivable_vfun....................proved - complete [shostak](0.05 s) scal_derivable_vfun...................proved - complete [shostak](0.12 s) const_derivable_vfun..................proved - complete [shostak](0.04 s) inv_derivable_vfun....................proved - complete [shostak](0.11 s) derivable_sum.........................proved - complete [shostak](0.04 s) derivable_diff........................proved - complete [shostak](0.04 s) derivable_scal........................proved - complete [shostak](0.04 s) derivable_neg.........................proved - complete [shostak](0.04 s) derivable_const.......................proved - complete [shostak](0.03 s) deriv_sum_vfun........................proved - complete [shostak](0.09 s) deriv_neg_vfun........................proved - complete [shostak](0.06 s) deriv_diff_vfun.......................proved - complete [shostak](0.07 s) deriv_dot_vfun_TCC1...................proved - complete [shostak](0.04 s) deriv_dot_vfun........................proved - complete [shostak](0.11 s) deriv_scal_vfun.......................proved - complete [shostak](0.07 s) deriv_const_vfun......................proved - complete [shostak](0.07 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.50 s) Proof summary for theory deriv_real_vect2 IMP_derivatives_TCC1..................proved - complete [shostak](0.00 s) IMP_derivatives_TCC2..................proved - complete [shostak](0.00 s) deriv_rv_TCC1.........................proved - complete [shostak](0.04 s) deriv_rv_TCC2.........................proved - complete [shostak](0.02 s) sum_derivable_rv......................proved - complete [shostak](0.07 s) diff_derivable_rv.....................proved - complete [shostak](0.06 s) neg_derivable_rv......................proved - complete [shostak](0.04 s) prod_derivable_rv.....................proved - complete [shostak](0.23 s) dot_derivable_rv......................proved - complete [shostak](0.09 s) sqv_derivable_rv......................proved - complete [shostak](0.01 s) const_derivable_rv....................proved - complete [shostak](0.01 s) scal_derivable_rv.....................proved - complete [shostak](0.06 s) prod_id_derivable_rv..................proved - complete [shostak](0.01 s) deriv_sum_vfun_TCC1...................proved - complete [shostak](0.01 s) deriv_sum_vfun........................proved - complete [shostak](0.13 s) deriv_diff_vfun_TCC1..................proved - complete [shostak](0.01 s) deriv_diff_vfun.......................proved - complete [shostak](0.11 s) deriv_neg_vfun_TCC1...................proved - complete [shostak](0.00 s) deriv_neg_vfun........................proved - complete [shostak](0.09 s) deriv_prod_vfun_TCC1..................proved - complete [shostak](0.01 s) deriv_prod_vfun.......................proved - complete [shostak](0.34 s) deriv_dot_vfun_TCC1...................proved - complete [shostak](0.01 s) deriv_dot_vfun........................proved - complete [shostak](0.44 s) deriv_sqv_vfun_TCC1...................proved - complete [shostak](0.01 s) deriv_sqv_vfun........................proved - complete [shostak](0.07 s) deriv_const_vfun_TCC1.................proved - complete [shostak](0.01 s) deriv_const_vfun......................proved - complete [shostak](0.03 s) deriv_scal_vfun_TCC1..................proved - complete [shostak](0.01 s) deriv_scal_vfun.......................proved - complete [shostak](0.20 s) deriv_prod_id_vfun_TCC1...............proved - complete [shostak](0.01 s) deriv_prod_id_vfun....................proved - complete [shostak](0.05 s) d_sum_vfun............................proved - complete [shostak](0.02 s) d_diff_vfun...........................proved - complete [shostak](0.01 s) d_neg_vfun............................proved - complete [shostak](0.01 s) d_prod_vfun...........................proved - complete [shostak](0.02 s) d_dot_vfun............................proved - complete [shostak](0.01 s) d_const_vfun..........................proved - complete [shostak](0.02 s) d_scal_vfun...........................proved - complete [shostak](0.01 s) Theory totals: 38 formulas, 38 attempted, 38 succeeded (2.25 s) Proof summary for theory vect_fun_ops_rv diff_function.........................proved - complete [shostak](0.03 s) negneg_function.......................proved - complete [shostak](0.03 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.06 s) Proof summary for theory deriv_cont_2D derivable_rv_cont_rv_TCC1.............proved - complete [shostak](0.01 s) derivable_rv_cont_rv_TCC2.............proved - complete [shostak](0.00 s) derivable_rv_cont_rv..................proved - complete [shostak](0.03 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.04 s) Proof summary for theory cont_real_vect2 continuity_def........................proved - complete [shostak](0.05 s) continuity_def2.......................proved - complete [shostak](0.01 s) continuous_iff_comps..................proved - complete [shostak](0.88 s) cont_rv_iff_comps.....................proved - complete [shostak](0.90 s) sum_continuous_rv.....................proved - complete [shostak](0.02 s) diff_continuous_rv....................proved - complete [shostak](0.02 s) const_continuous_rv...................proved - complete [shostak](0.01 s) scal_continuous_rv....................proved - complete [shostak](0.44 s) prod_continuous_rv....................proved - complete [shostak](0.09 s) neg_continuous_rv.....................proved - complete [shostak](0.02 s) sum_cont_rv_fun.......................proved - complete [shostak](0.11 s) diff_cont_rv_fun......................proved - complete [shostak](0.11 s) const_cont_rv_fun.....................proved - complete [shostak](0.02 s) const_vfun_cont_rv....................proved - complete [shostak](0.06 s) scal_cont_rv_fun......................proved - complete [shostak](0.01 s) prod_cont_rv_fun......................proved - complete [shostak](0.08 s) neg_cont_rv_fun.......................proved - complete [shostak](0.06 s) continuous_rv_fun_TCC1................proved - complete [shostak](0.03 s) sum_fun_continuous_rv.................proved - complete [shostak](0.12 s) diff_fun_continuous_rv................proved - complete [shostak](0.11 s) const_fun_continuous_rv...............proved - complete [shostak](0.00 s) neg_fun_continuous_rv.................proved - complete [shostak](0.07 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (3.22 s) Proof summary for theory limit_real_vect2 cv_unique.............................proved - complete [shostak](0.31 s) cv_in_domain..........................proved - complete [shostak](0.09 s) cv_sum................................proved - complete [shostak](0.26 s) cv_neg................................proved - complete [shostak](0.12 s) cv_diff...............................proved - complete [shostak](0.05 s) cv_const..............................proved - complete [shostak](0.03 s) cv_scal...............................proved - complete [shostak](0.22 s) lim_TCC1..............................proved - complete [shostak](0.01 s) lim_fun_lemma.........................proved - complete [shostak](0.02 s) lim_fun_def...........................proved - complete [shostak](0.02 s) convergence_equiv.....................proved - complete [shostak](0.01 s) convergent_in_domain..................proved - complete [shostak](0.02 s) lim_in_domain.........................proved - complete [shostak](0.02 s) sum_fun_convergent....................proved - complete [shostak](0.02 s) neg_fun_convergent....................proved - complete [shostak](0.01 s) diff_fun_convergent...................proved - complete [shostak](0.02 s) const_fun_convergent..................proved - complete [shostak](0.04 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s) lim_sum_fun...........................proved - complete [shostak](0.01 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.01 s) lim_neg_fun...........................proved - complete [shostak](0.01 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_diff_fun..........................proved - complete [shostak](0.02 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (1.33 s) Proof summary for theory vect_metric_space IMP_metric_spaces_TCC1................proved - complete [shostak](0.07 s) vectors_metric_space..................proved - complete [shostak](0.03 s) vect_subset_metric_space..............proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.10 s) Proof summary for theory vect3_metric_space IMP_metric_spaces_TCC1................proved - complete [shostak](0.06 s) vect3_subset_metric_space.............proved - complete [shostak](0.04 s) vect3_metric_space....................proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.10 s) Proof summary for theory vect3_Heine IMP_cross_metric_real_fun_TCC1........proved - complete [shostak](0.01 s) IMP_cross_metric_real_fun_TCC2........proved - complete [shostak](0.00 s) curried_min_exists_3D_TCC1............proved - complete [shostak](0.00 s) curried_min_exists_3D.................proved - incomplete [shostak](0.39 s) curried_min_is_cont_3D_TCC1...........proved - incomplete [shostak](0.32 s) curried_min_is_cont_3D................proved - incomplete [shostak](0.31 s) curried_min_is_cont_3D_ed_TCC1........proved - incomplete [shostak](0.31 s) curried_min_is_cont_3D_ed.............proved - incomplete [shostak](0.52 s) multiary_Heine_3D.....................proved - incomplete [shostak](0.11 s) multiary_Heine_3D_ed..................proved - incomplete [shostak](0.16 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.13 s) Proof summary for theory limit_vect2_real cv_unique.............................proved - complete [shostak](0.31 s) cv_in_domain..........................proved - complete [shostak](0.09 s) cv_sum................................proved - complete [shostak](0.28 s) cv_neg................................proved - complete [shostak](0.14 s) cv_diff...............................proved - complete [shostak](0.02 s) cv_prod...............................proved - complete [shostak](0.40 s) cv_const..............................proved - complete [shostak](0.03 s) cv_scal...............................proved - complete [shostak](0.03 s) cv_inv................................proved - complete [shostak](0.34 s) cv_div................................proved - complete [shostak](0.08 s) lim_TCC1..............................proved - complete [shostak](0.02 s) lim_fun_lemma.........................proved - complete [shostak](0.01 s) lim_fun_def...........................proved - complete [shostak](0.02 s) convergence_equiv.....................proved - complete [shostak](0.02 s) convergent_in_domain..................proved - complete [shostak](0.02 s) lim_in_domain.........................proved - complete [shostak](0.01 s) sum_fun_convergent....................proved - complete [shostak](0.03 s) neg_fun_convergent....................proved - complete [shostak](0.01 s) diff_fun_convergent...................proved - complete [shostak](0.02 s) prod_fun_convergent...................proved - complete [shostak](0.03 s) const_fun_convergent..................proved - complete [shostak](0.04 s) scal_fun_convergent...................proved - complete [shostak](0.03 s) inv_fun_convergent....................proved - complete [shostak](0.03 s) div_fun_convergent....................proved - complete [shostak](0.03 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s) lim_sum_fun...........................proved - complete [shostak](0.02 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.01 s) lim_neg_fun...........................proved - complete [shostak](0.01 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_diff_fun..........................proved - complete [shostak](0.02 s) lim_prod_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_prod_fun..........................proved - complete [shostak](0.03 s) lim_const_fun_TCC1....................proved - complete [shostak](0.00 s) lim_const_fun.........................proved - complete [shostak](0.02 s) lim_scal_fun_TCC1.....................proved - complete [shostak](0.00 s) lim_scal_fun..........................proved - complete [shostak](0.03 s) lim_inv_fun_TCC1......................proved - complete [shostak](0.01 s) lim_inv_fun...........................proved - complete [shostak](0.03 s) lim_div_fun_TCC1......................proved - complete [shostak](0.01 s) lim_div_fun...........................proved - complete [shostak](0.03 s) convergence_order.....................proved - complete [shostak](0.21 s) convergence_lower_bound...............proved - complete [shostak](0.05 s) convergence_upper_bound...............proved - complete [shostak](0.06 s) lim_le1...............................proved - complete [shostak](0.05 s) lim_ge1...............................proved - complete [shostak](0.02 s) lim_order1............................proved - complete [shostak](0.06 s) Theory totals: 46 formulas, 46 attempted, 46 succeeded (2.73 s) Proof summary for theory limit_vect3_real cv_unique.............................proved - complete [shostak](0.34 s) cv_in_domain..........................proved - complete [shostak](0.10 s) cv_sum................................proved - complete [shostak](0.29 s) cv_neg................................proved - complete [shostak](0.14 s) cv_diff...............................proved - complete [shostak](0.02 s) cv_prod...............................proved - complete [shostak](0.41 s) cv_const..............................proved - complete [shostak](0.02 s) cv_scal...............................proved - complete [shostak](0.03 s) cv_inv................................proved - complete [shostak](0.33 s) cv_div................................proved - complete [shostak](0.07 s) lim_fun_lemma.........................proved - complete [shostak](0.01 s) lim_fun_def...........................proved - complete [shostak](0.02 s) convergence_equiv.....................proved - complete [shostak](0.01 s) convergent_in_domain..................proved - complete [shostak](0.03 s) lim_in_domain.........................proved - complete [shostak](0.01 s) sum_fun_convergent....................proved - complete [shostak](0.03 s) neg_fun_convergent....................proved - complete [shostak](0.01 s) diff_fun_convergent...................proved - complete [shostak](0.01 s) prod_fun_convergent...................proved - complete [shostak](0.03 s) const_fun_convergent..................proved - complete [shostak](0.04 s) scal_fun_convergent...................proved - complete [shostak](0.02 s) inv_fun_convergent....................proved - complete [shostak](0.04 s) div_fun_convergent....................proved - complete [shostak](0.03 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s) lim_sum_fun...........................proved - complete [shostak](0.02 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.01 s) lim_neg_fun...........................proved - complete [shostak](0.02 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_diff_fun..........................proved - complete [shostak](0.01 s) lim_prod_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_prod_fun..........................proved - complete [shostak](0.03 s) lim_const_fun_TCC1....................proved - complete [shostak](0.01 s) lim_const_fun.........................proved - complete [shostak](0.01 s) lim_scal_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_scal_fun..........................proved - complete [shostak](0.02 s) lim_inv_fun_TCC1......................proved - complete [shostak](0.01 s) lim_inv_fun...........................proved - complete [shostak](0.03 s) lim_div_fun_TCC1......................proved - complete [shostak](0.01 s) lim_div_fun...........................proved - complete [shostak](0.03 s) convergence_order.....................proved - complete [shostak](0.22 s) convergence_lower_bound...............proved - complete [shostak](0.05 s) convergence_upper_bound...............proved - complete [shostak](0.05 s) lim_le1...............................proved - complete [shostak](0.06 s) lim_ge1...............................proved - complete [shostak](0.02 s) lim_order1............................proved - complete [shostak](0.07 s) Theory totals: 45 formulas, 45 attempted, 45 succeeded (2.74 s) Proof summary for theory limit_vect2_vect2 cv_unique.............................proved - complete [shostak](0.18 s) cv_in_domain..........................proved - complete [shostak](0.06 s) cv_sum................................proved - complete [shostak](0.22 s) cv_neg................................proved - complete [shostak](0.09 s) cv_diff...............................proved - complete [shostak](0.05 s) cv_const..............................proved - complete [shostak](0.01 s) lim_TCC1..............................proved - complete [shostak](0.01 s) lim_fun_lemma.........................proved - complete [shostak](0.02 s) lim_fun_def...........................proved - complete [shostak](0.02 s) convergence_equiv.....................proved - complete [shostak](0.02 s) convergent_in_domain..................proved - complete [shostak](0.02 s) lim_in_domain.........................proved - complete [shostak](0.02 s) sum_fun_convergent....................proved - complete [shostak](0.01 s) neg_fun_convergent....................proved - complete [shostak](0.01 s) diff_fun_convergent...................proved - complete [shostak](0.01 s) const_fun_convergent..................proved - complete [shostak](0.04 s) lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s) lim_sum_fun...........................proved - complete [shostak](0.01 s) lim_neg_fun_TCC1......................proved - complete [shostak](0.01 s) lim_neg_fun...........................proved - complete [shostak](0.01 s) lim_diff_fun_TCC1.....................proved - complete [shostak](0.01 s) lim_diff_fun..........................proved - complete [shostak](0.01 s) lim_const_fun_TCC1....................proved - complete [shostak](0.01 s) lim_const_fun.........................proved - complete [shostak](0.01 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (0.85 s) Proof summary for theory cont_vect2_real continuity_def........................proved - complete [shostak](0.03 s) continuity_def2.......................proved - complete [shostak](0.01 s) sum_continuous_vr.....................proved - complete [shostak](0.02 s) diff_continuous_vr....................proved - complete [shostak](0.01 s) prod_continuous_vr....................proved - complete [shostak](0.02 s) const_continuous_vr...................proved - complete [shostak](0.01 s) scal_continuous_vr....................proved - complete [shostak](0.01 s) neg_continuous_vr.....................proved - complete [shostak](0.01 s) div_continuous_vr.....................proved - complete [shostak](0.03 s) inv_continuous_vr.....................proved - complete [shostak](0.04 s) expt_continuous_vr....................proved - complete [shostak](0.07 s) sum_cont_vr_fun.......................proved - complete [shostak](0.08 s) diff_cont_vr_fun......................proved - complete [shostak](0.08 s) prod_cont_vr_fun......................proved - complete [shostak](0.08 s) const_cont_vr_fun.....................proved - complete [shostak](0.00 s) scal_cont_vr_fun......................proved - complete [shostak](0.01 s) neg_cont_vr_fun.......................proved - complete [shostak](0.04 s) div_cont_vr_fun.......................proved - complete [shostak](0.08 s) inv_cont_vr_fun.......................proved - complete [shostak](0.01 s) expt_cont_vr_fun......................proved - complete [shostak](0.02 s) continuous_vr_fun_TCC1................proved - complete [shostak](0.02 s) sum_fun_continuous_vr.................proved - complete [shostak](0.09 s) diff_fun_continuous_vr................proved - complete [shostak](0.08 s) prod_fun_continuous_vr................proved - complete [shostak](0.09 s) const_fun_continuous_vr...............proved - complete [shostak](0.01 s) scal_fun_continuous_vr................proved - complete [shostak](0.05 s) neg_fun_continuous_vr.................proved - complete [shostak](0.05 s) div_fun_continuous_vr.................proved - complete [shostak](0.08 s) inv_fun_continuous_vr.................proved - complete [shostak](0.05 s) expt_fun_continuous_vr................proved - complete [shostak](0.01 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (1.18 s) Proof summary for theory cont_vect3_real continuity_def........................proved - complete [shostak](0.02 s) continuity_def2.......................proved - complete [shostak](0.01 s) sum_continuous_vr.....................proved - complete [shostak](0.02 s) diff_continuous_vr....................proved - complete [shostak](0.02 s) prod_continuous_vr....................proved - complete [shostak](0.01 s) const_continuous_vr...................proved - complete [shostak](0.01 s) scal_continuous_vr....................proved - complete [shostak](0.02 s) neg_continuous_vr.....................proved - complete [shostak](0.01 s) div_continuous_vr.....................proved - complete [shostak](0.04 s) inv_continuous_vr.....................proved - complete [shostak](0.03 s) expt_continuous_vr....................proved - complete [shostak](0.07 s) sum_cont_vr_fun.......................proved - complete [shostak](0.09 s) diff_cont_vr_fun......................proved - complete [shostak](0.08 s) prod_cont_vr_fun......................proved - complete [shostak](0.08 s) const_cont_vr_fun.....................proved - complete [shostak](0.01 s) scal_cont_vr_fun......................proved - complete [shostak](0.02 s) neg_cont_vr_fun.......................proved - complete [shostak](0.04 s) div_cont_vr_fun.......................proved - complete [shostak](0.08 s) inv_cont_vr_fun.......................proved - complete [shostak](0.01 s) expt_cont_vr_fun......................proved - complete [shostak](0.01 s) continuous_vr_fun_TCC1................proved - complete [shostak](0.02 s) sum_fun_continuous_vr.................proved - complete [shostak](0.08 s) diff_fun_continuous_vr................proved - complete [shostak](0.08 s) prod_fun_continuous_vr................proved - complete [shostak](0.08 s) const_fun_continuous_vr...............proved - complete [shostak](0.00 s) scal_fun_continuous_vr................proved - complete [shostak](0.04 s) neg_fun_continuous_vr.................proved - complete [shostak](0.04 s) div_fun_continuous_vr.................proved - complete [shostak](0.09 s) inv_fun_continuous_vr.................proved - complete [shostak](0.05 s) expt_fun_continuous_vr................proved - complete [shostak](0.01 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (1.16 s) Proof summary for theory cont_vect2_vect2 continuity_def........................proved - complete [shostak](0.01 s) continuity_def2.......................proved - complete [shostak](0.01 s) sum_continuous_vv.....................proved - complete [shostak](0.02 s) diff_continuous_vv....................proved - complete [shostak](0.01 s) const_continuous_vv...................proved - complete [shostak](0.00 s) identity_continuous_vv................proved - complete [shostak](0.01 s) neg_continuous_vv.....................proved - complete [shostak](0.01 s) sum_cont_vv_fun.......................proved - complete [shostak](0.08 s) diff_cont_vv_fun......................proved - complete [shostak](0.08 s) const_cont_vv_fun.....................proved - complete [shostak](0.01 s) neg_cont_vv_fun.......................proved - complete [shostak](0.04 s) id_cont_vv_fun........................proved - complete [shostak](0.01 s) continuous_vv_fun_TCC1................proved - complete [shostak](0.01 s) sum_fun_continuous_vv.................proved - complete [shostak](0.08 s) diff_fun_continuous_vv................proved - complete [shostak](0.07 s) const_fun_continuous_vv...............proved - complete [shostak](0.00 s) neg_fun_continuous_vv.................proved - complete [shostak](0.04 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (0.49 s) Proof summary for theory vect2_cont_comp comp_vv_vv_cont.......................proved - complete [shostak](0.05 s) comp_rv_vr_cont.......................proved - complete [shostak](0.10 s) comp_vr_vv_cont.......................proved - complete [shostak](0.07 s) comp_rr_vr_cont.......................proved - complete [shostak](0.12 s) comp_vv_rv_cont.......................proved - complete [shostak](0.08 s) comp_rv_rr_cont.......................proved - complete [shostak](0.16 s) comp_vr_rv_cont.......................proved - complete [shostak](0.15 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.71 s) Proof summary for theory vect2_cont_comp2 comp_tt_vt_cont.......................proved - complete [shostak](0.12 s) comp_rv_tt_cont.......................proved - complete [shostak](0.18 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.29 s) Proof summary for theory vect2_cont_dot dot_cont_vr...........................proved - complete [shostak](1.05 s) dot_cont_rr...........................proved - complete [shostak](0.40 s) scal_cont_rv..........................proved - complete [shostak](1.49 s) scal_cont_vv..........................proved - complete [shostak](1.33 s) scal_scal_cont_rv.....................proved - complete [shostak](0.01 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (4.29 s) Proof summary for theory vect_cont_2D const_cont_vv.........................proved - complete [shostak](0.01 s) const_cont_rv.........................proved - complete [shostak](0.01 s) const_cont_vr.........................proved - complete [shostak](0.11 s) pair_cont_rv..........................proved - complete [shostak](0.63 s) pair_cont_vv..........................proved - complete [shostak](0.37 s) x_cont_vr.............................proved - complete [shostak](0.14 s) y_cont_vr.............................proved - complete [shostak](0.12 s) id_cont_vv............................proved - complete [shostak](0.01 s) mult_cont_vr..........................proved - complete [shostak](0.02 s) scal_mult_cont_vr.....................proved - complete [shostak](0.02 s) div_cont_vr...........................proved - complete [shostak](0.02 s) scal_div1_cont_vr.....................proved - complete [shostak](0.03 s) scal_div2_cont_vr.....................proved - complete [shostak](0.02 s) add_cont_vv...........................proved - complete [shostak](0.02 s) add_cont_vr...........................proved - complete [shostak](0.02 s) add_cont_rv...........................proved - complete [shostak](0.02 s) sub_cont_vv...........................proved - complete [shostak](0.02 s) sub_cont_vr...........................proved - complete [shostak](0.02 s) sub_cont_rv...........................proved - complete [shostak](0.02 s) neg_cont_vr...........................proved - complete [shostak](0.02 s) neg_cont_vv...........................proved - complete [shostak](0.01 s) neg_cont_rv...........................proved - complete [shostak](0.02 s) scal_scal_cont_vv.....................proved - complete [shostak](0.01 s) sqv_cont..............................proved - complete [shostak](0.01 s) neg_cont..............................proved - complete [shostak](0.02 s) abs_cont_vr...........................proved - complete [shostak](0.04 s) max_cont_vr...........................proved - complete [shostak](0.33 s) min_cont_vr...........................proved - complete [shostak](0.12 s) sq_cont_vr............................proved - complete [shostak](0.04 s) sqv_cont_vr...........................proved - complete [shostak](0.01 s) sqv_cont_rr...........................proved - complete [shostak](0.01 s) Theory totals: 31 formulas, 31 attempted, 31 succeeded (2.25 s) Proof summary for theory vect_deriv_2D IMP_deriv_real_vect2_TCC1.............proved - complete [shostak](0.00 s) IMP_deriv_real_vect2_TCC2.............proved - complete [shostak](0.00 s) detsv_diff............................proved - complete [shostak](0.11 s) detsvp_deriv_TCC1.....................proved - complete [shostak](0.01 s) detsvp_deriv..........................proved - complete [shostak](0.59 s) sqvdot_diff...........................proved - complete [shostak](0.09 s) sqvdot_deriv_TCC1.....................proved - complete [shostak](0.01 s) sqvdot_deriv..........................proved - complete [shostak](0.40 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.20 s) Proof summary for theory vect_chain_rule composition_derivable_vfun_TCC1.......proved - complete [shostak](0.01 s) composition_derivable_vfun_TCC2.......proved - complete [shostak](0.00 s) composition_derivable_vfun_TCC3.......proved - complete [shostak](0.01 s) composition_derivable_vfun_TCC4.......proved - complete [shostak](0.01 s) composition_derivable_vfun............proved - complete [shostak](0.06 s) gg_TCC1...............................proved - complete [shostak](0.01 s) gg_TCC2...............................proved - complete [shostak](0.00 s) deriv_comp_vfun_TCC1..................proved - complete [shostak](0.01 s) deriv_comp_vfun.......................proved - complete [shostak](0.19 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.30 s) Proof summary for theory four_vects_2D_continuity div_vvr_TCC1..........................proved - complete [shostak](0.02 s) sum_vvv_cont..........................proved - complete [shostak](0.29 s) sum_vvr_cont..........................proved - complete [shostak](0.46 s) diff_vvv_cont.........................proved - complete [shostak](0.33 s) scal_vvv_cont.........................proved - complete [shostak](0.42 s) dot_vvv_cont..........................proved - complete [shostak](1.65 s) prod_vvr_cont.........................proved - complete [shostak](0.54 s) const_vvr_cont........................proved - complete [shostak](0.03 s) scal_vvr_vvv_cont.....................proved - complete [shostak](1.38 s) scal_vvr_cont.........................proved - complete [shostak](0.48 s) div_vvr_cont_TCC1.....................proved - complete [shostak](0.92 s) div_vvr_cont..........................proved - complete [shostak](0.86 s) input1_vvv_cont.......................proved - complete [shostak](0.01 s) input2_vvv_cont.......................proved - complete [shostak](0.03 s) input3_vvv_cont.......................proved - complete [shostak](0.01 s) input4_vvv_cont.......................proved - complete [shostak](0.02 s) max_vvr_cont..........................proved - complete [shostak](0.45 s) norm_vvv_cont.........................proved - complete [shostak](0.19 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (8.11 s) Proof summary for theory vect2_metric_space IMP_metric_spaces_TCC1................proved - complete [shostak](0.04 s) vect2_subset_metric_space.............proved - complete [shostak](0.04 s) vect2_metric_space....................proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.09 s) Proof summary for theory vect2_Heine IMP_cross_metric_real_fun_TCC1........proved - complete [shostak](0.00 s) IMP_cross_metric_real_fun_TCC2........proved - complete [shostak](0.00 s) curried_min_exists_2D_TCC1............proved - complete [shostak](0.01 s) curried_min_exists_2D.................proved - incomplete [shostak](0.40 s) curried_min_is_cont_2D_TCC1...........proved - incomplete [shostak](0.33 s) curried_min_is_cont_2D................proved - incomplete [shostak](0.30 s) curried_min_is_cont_2D_ed_TCC1........proved - incomplete [shostak](0.30 s) curried_min_is_cont_2D_ed.............proved - incomplete [shostak](0.50 s) multiary_Heine_2D.....................proved - incomplete [shostak](0.11 s) multiary_Heine_2D_ed..................proved - incomplete [shostak](0.17 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.11 s) Proof summary for theory vect_vect_2D_continuity div_vvr_TCC1..........................proved - complete [shostak](0.02 s) sum_vvv_cont..........................proved - complete [shostak](0.23 s) sum_vvr_cont..........................proved - complete [shostak](0.21 s) diff_vvv_cont.........................proved - complete [shostak](0.23 s) scal_vvv_cont.........................proved - complete [shostak](0.27 s) dot_vvv_cont..........................proved - complete [shostak](1.45 s) prod_vvr_cont.........................proved - complete [shostak](0.48 s) const_vvr_cont........................proved - complete [shostak](0.04 s) scal_vvr_vvv_cont.....................proved - complete [shostak](1.08 s) scal_vvr_cont.........................proved - complete [shostak](0.27 s) div_vvr_cont_TCC1.....................proved - complete [shostak](0.52 s) div_vvr_cont..........................proved - complete [shostak](0.82 s) nzv_vvv_cont..........................proved - complete [shostak](0.02 s) s_vvv_cont............................proved - complete [shostak](0.02 s) max_vvr_cont..........................proved - complete [shostak](0.38 s) norm_vvv_cont.........................proved - complete [shostak](0.18 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (6.20 s) Proof summary for theory deriv_sincos_ax sin_derivable_TCC1....................proved - complete [shostak](0.00 s) sin_derivable_TCC2....................proved - complete [shostak](0.00 s) deriv_sin_TCC1........................proved - complete [shostak](0.00 s) deriv_cos_TCC1........................proved - complete [shostak](0.01 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.01 s) Grand Totals: 559 proofs, 559 attempted, 559 succeeded (59.26 s) [ Dauer der Verarbeitung: 0.230 Sekunden ] |