|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
integral_cont_scaf.pvs
Sprache: Lisp
Haftungsausschluß.summary KontaktMT940 {MT940[607] Hlasm[2111] Haskell[2429]}diese Dinge liegen außhalb unserer Verantwortung
***
*** 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)
[ Seitenstruktur0.196Drucken
]
|
|
|
|
|
|
