Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
scott_continuity.pvs
Sprache: Lisp
Untersuchungsergebnis.summary Download desMT940 {MT940[541] Hlasm[2025] Haskell[2367]}zum Wurzelverzeichnis wechseln
***
*** top (16:31:35 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 top_limits
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory lim_of_functions
convergence_def.......................proved - complete [shostak](0.07 s)
adherence_fullset.....................proved - complete [shostak](0.02 s)
cv_unique.............................proved - complete [shostak](0.03 s)
cv_in_domain..........................proved - complete [shostak](0.02 s)
cv_sum................................proved - complete [shostak](0.04 s)
cv_diff...............................proved - complete [shostak](0.02 s)
cv_prod...............................proved - complete [shostak](0.04 s)
cv_const..............................proved - complete [shostak](0.01 s)
cv_scal...............................proved - complete [shostak](0.03 s)
cv_neg................................proved - complete [shostak](0.02 s)
cv_div................................proved - complete [shostak](0.03 s)
cv_inv................................proved - complete [shostak](0.04 s)
cv_identity...........................proved - complete [shostak](0.01 s)
cv_abs................................proved - complete [shostak](0.28 s)
conv_0_0_abs..........................proved - complete [shostak](0.21 s)
lim_TCC1..............................proved - complete [shostak](0.03 s)
lim_fun_lemma.........................proved - complete [shostak](0.01 s)
lim_fun_def...........................proved - complete [shostak](0.02 s)
lim_e_del.............................proved - complete [shostak](0.13 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.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.02 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)
convergent_identity...................proved - complete [shostak](0.02 s)
lim_sum_fun_TCC1......................proved - complete [shostak](0.01 s)
lim_sum_fun...........................proved - complete [shostak](0.04 s)
lim_neg_fun_TCC1......................proved - complete [shostak](0.00 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.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.02 s)
lim_inv_fun...........................proved - complete [shostak](0.02 s)
lim_div_fun_TCC1......................proved - complete [shostak](0.01 s)
lim_div_fun...........................proved - complete [shostak](0.03 s)
lim_identity_TCC1.....................proved - complete [shostak](0.01 s)
lim_identity..........................proved - complete [shostak](0.01 s)
lim_le1...............................proved - complete [shostak](0.05 s)
lim_ge1...............................proved - complete [shostak](0.04 s)
lim_order1............................proved - complete [shostak](0.06 s)
lim_le2...............................proved - complete [shostak](0.07 s)
lim_ge2...............................proved - complete [shostak](0.04 s)
lim_order2............................proved - complete [shostak](0.05 s)
Theory totals: 55 formulas, 55 attempted, 55 succeeded (1.95 s)
Proof summary for theory convergence_functions
member_adherent.......................proved - complete [shostak](0.04 s)
adherence_subset1.....................proved - complete [shostak](0.09 s)
adherence_subset2.....................proved - complete [shostak](0.01 s)
adherence_prop1.......................proved - complete [shostak](0.03 s)
adherence_prop2.......................proved - complete [shostak](0.08 s)
convergence_unicity...................proved - complete [shostak](0.29 s)
subset_convergence....................proved - complete [shostak](0.14 s)
subset_convergence2...................proved - complete [shostak](0.01 s)
convergence_in_domain.................proved - complete [shostak](0.19 s)
convergence_sum.......................proved - complete [shostak](0.36 s)
convergence_neg.......................proved - complete [shostak](0.17 s)
convergence_diff......................proved - complete [shostak](0.03 s)
convergence_prod......................proved - complete [shostak](0.46 s)
convergence_const.....................proved - complete [shostak](0.04 s)
convergence_scal......................proved - complete [shostak](0.04 s)
convergence_inv.......................proved - complete [shostak](0.36 s)
convergence_div.......................proved - complete [shostak](0.06 s)
convergence_identity..................proved - complete [shostak](0.07 s)
convergence_order.....................proved - complete [shostak](0.25 s)
convergence_lower_bound...............proved - complete [shostak](0.09 s)
convergence_upper_bound...............proved - complete [shostak](0.09 s)
convergence_locally_constant..........proved - complete [shostak](0.09 s)
convergence_squeezing.................proved - complete [shostak](0.38 s)
Theory totals: 23 formulas, 23 attempted, 23 succeeded (3.37 s)
Proof summary for theory epsilon_lemmas
prod_bound............................proved - complete [shostak](0.50 s)
prod_epsilon..........................proved - complete [shostak](0.36 s)
inv_bound_TCC1........................proved - complete [shostak](0.04 s)
inv_bound.............................proved - complete [shostak](0.45 s)
inv_epsilon1..........................proved - complete [shostak](0.25 s)
inv_epsilon_TCC1......................proved - complete [shostak](0.03 s)
inv_epsilon...........................proved - complete [shostak](0.29 s)
varying_epsilon.......................proved - complete [shostak](0.03 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.94 s)
Proof summary for theory lim_of_composition
adherence_lemma.......................proved - complete [shostak](0.21 s)
adherence_lemma2......................proved - complete [shostak](0.03 s)
convergence_composition...............proved - complete [shostak](0.29 s)
convergent_composition................proved - complete [shostak](0.22 s)
lim_composition_TCC1..................proved - complete [shostak](0.01 s)
lim_composition.......................proved - complete [shostak](0.08 s)
convergence_comp_continuous...........proved - complete [shostak](0.02 s)
convergent_comp_continuous............proved - complete [shostak](0.06 s)
lim_comp_continuous_TCC1..............proved - complete [shostak](0.01 s)
lim_comp_continuous...................proved - complete [shostak](0.04 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.98 s)
Proof summary for theory continuous_functions
continuity_def........................proved - complete [shostak](0.07 s)
continuity_def2.......................proved - complete [shostak](0.01 s)
continuous_on_def.....................proved - complete [shostak](0.21 s)
sum_continuous........................proved - complete [shostak](0.02 s)
diff_continuous.......................proved - complete [shostak](0.02 s)
prod_continuous.......................proved - complete [shostak](0.02 s)
const_continuous......................proved - complete [shostak](0.01 s)
scal_continuous.......................proved - complete [shostak](0.01 s)
neg_continuous........................proved - complete [shostak](0.01 s)
div_continuous........................proved - complete [shostak](0.04 s)
inv_continuous........................proved - complete [shostak](0.03 s)
identity_continuous...................proved - complete [shostak](0.01 s)
expt_continuous.......................proved - complete [shostak](0.06 s)
sum_set_continuous....................proved - complete [shostak](0.08 s)
diff_set_continuous...................proved - complete [shostak](0.07 s)
prod_set_continuous...................proved - complete [shostak](0.08 s)
const_set_continuous..................proved - complete [shostak](0.03 s)
scal_set_continuous...................proved - complete [shostak](0.04 s)
neg_set_continuous....................proved - complete [shostak](0.04 s)
div_set_continuous....................proved - complete [shostak](0.08 s)
inv_set_continuous....................proved - complete [shostak](0.05 s)
identity_set_continuous...............proved - complete [shostak](0.06 s)
continuous_def2.......................proved - complete [shostak](0.17 s)
continuity_subset2....................proved - complete [shostak](0.09 s)
continuous_fun_TCC1...................proved - complete [shostak](0.02 s)
sum_fun_continuous....................proved - complete [shostak](0.02 s)
diff_fun_continuous...................proved - complete [shostak](0.01 s)
prod_fun_continuous...................proved - complete [shostak](0.02 s)
const_fun_continuous..................proved - complete [shostak](0.01 s)
scal_fun_continuous...................proved - complete [shostak](0.02 s)
neg_fun_continuous....................proved - complete [shostak](0.01 s)
div_fun_continuous....................proved - complete [shostak](0.02 s)
id_fun_continuous.....................proved - complete [shostak](0.01 s)
inv_fun_continuous....................proved - complete [shostak](0.02 s)
linear_fun_cont.......................proved - complete [shostak](0.09 s)
one_over_x_cont_TCC1..................proved - complete [shostak](0.01 s)
one_over_x_cont.......................proved - complete [shostak](0.05 s)
x_to_n_continuous_TCC1................proved - complete [shostak](0.01 s)
x_to_n_continuous.....................proved - complete [shostak](0.17 s)
expt_fun_continuous...................proved - complete [shostak](0.01 s)
sum_cont_fun..........................proved - complete [shostak](0.06 s)
diff_cont_fun.........................proved - complete [shostak](0.05 s)
prod_cont_fun.........................proved - complete [shostak](0.06 s)
const_cont_fun........................proved - complete [shostak](0.01 s)
scal_cont_fun.........................proved - complete [shostak](0.01 s)
neg_cont_fun..........................proved - complete [shostak](0.03 s)
div_cont_fun..........................proved - complete [shostak](0.05 s)
inv_cont_fun..........................proved - complete [shostak](0.02 s)
identity_cont_fun.....................proved - complete [shostak](0.01 s)
expt_cont_fun.........................proved - complete [shostak](0.01 s)
Theory totals: 50 formulas, 50 attempted, 50 succeeded (2.14 s)
Proof summary for theory top_sequences
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory convergence_ops
cnv_seq_sum...........................proved - complete [shostak](0.20 s)
cnv_seq_neg...........................proved - complete [shostak](0.10 s)
cnv_seq_diff..........................proved - complete [shostak](0.02 s)
cnv_seq_prod..........................proved - complete [shostak](0.27 s)
cnv_seq_const.........................proved - complete [shostak](0.02 s)
cnv_seq_scal..........................proved - complete [shostak](0.03 s)
cnv_seq_inv...........................proved - complete [shostak](0.24 s)
cnv_seq_div...........................proved - complete [shostak](0.07 s)
cnv_seq_abs...........................proved - complete [shostak](0.17 s)
cnv_seq_order.........................proved - complete [shostak](0.12 s)
convergence_shift.....................proved - complete [shostak](0.10 s)
squeezing_variant.....................proved - complete [shostak](0.13 s)
squeezing_const1......................proved - complete [shostak](0.02 s)
squeezing_const2......................proved - complete [shostak](0.01 s)
squeezing.............................proved - complete [shostak](0.04 s)
squeezing_gen.........................proved - complete [shostak](0.05 s)
abs_convergence.......................proved - complete [shostak](0.05 s)
convergent_sum........................proved - complete [shostak](0.04 s)
convergent_neg........................proved - complete [shostak](0.03 s)
convergent_diff.......................proved - complete [shostak](0.13 s)
convergent_prod.......................proved - complete [shostak](0.14 s)
convergent_const......................proved - complete [shostak](0.05 s)
convergent_scal.......................proved - complete [shostak](0.11 s)
convergent_inv........................proved - complete [shostak](0.03 s)
convergent_div........................proved - complete [shostak](-1.70 s)
convergent_abs........................proved - complete [shostak](0.03 s)
squeezing_abs_0.......................proved - complete [shostak](0.06 s)
squeezing_abs_0_gen...................proved - complete [shostak](0.06 s)
constant_seq1.........................proved - complete [shostak](0.01 s)
constant_seq2.........................proved - complete [shostak](0.05 s)
conv_seq_plus.........................proved - complete [shostak](0.01 s)
conv_seq_minus........................proved - complete [shostak](0.00 s)
conv_seq_times........................proved - complete [shostak](0.01 s)
conv_seq_scal.........................proved - complete [shostak](0.00 s)
conv_seq_neg..........................proved - complete [shostak](0.00 s)
conv_seq_abs..........................proved - complete [shostak](0.01 s)
conv_seq_div1.........................proved - complete [shostak](0.02 s)
conv_seq_div2.........................proved - complete [shostak](0.01 s)
limit_sum.............................proved - complete [shostak](0.03 s)
limit_neg.............................proved - complete [shostak](0.01 s)
limit_diff............................proved - complete [shostak](0.01 s)
limit_prod............................proved - complete [shostak](0.02 s)
limit_inv_TCC1........................proved - complete [shostak](0.02 s)
limit_inv.............................proved - complete [shostak](0.03 s)
limit_div.............................proved - complete [shostak](0.03 s)
limit_const...........................proved - complete [shostak](0.01 s)
limit_scal............................proved - complete [shostak](0.02 s)
limit_abs.............................proved - complete [shostak](0.02 s)
limit_equiv...........................proved - complete [shostak](0.02 s)
limit_order...........................proved - complete [shostak](0.18 s)
Theory totals: 50 formulas, 50 attempted, 50 succeeded (1.14 s)
Proof summary for theory convergence_sequences
unique_limit..........................proved - complete [shostak](0.13 s)
limit_lemma...........................proved - complete [shostak](0.02 s)
limit_def.............................proved - complete [shostak](0.05 s)
convergence_subsequence...............proved - complete [shostak](0.11 s)
limit_accumulation....................proved - complete [shostak](0.12 s)
g_TCC1................................proved - complete [shostak](0.01 s)
g_TCC2................................proved - complete [shostak](0.01 s)
g_TCC3................................proved - complete [shostak](0.01 s)
g_prop................................proved - complete [shostak](0.14 s)
g_increasing..........................proved - complete [shostak](0.07 s)
g_convergence.........................proved - complete [shostak](0.03 s)
accumulation_subsequence..............proved - complete [shostak](0.25 s)
cauchy_accumulation...................proved - complete [shostak](0.19 s)
cauchy_subsequence....................proved - complete [shostak](0.01 s)
increasing_bounded_convergence........proved - complete [shostak](0.19 s)
decreasing_bounded_convergence........proved - complete [shostak](0.19 s)
bolzano_weierstrass1..................proved - complete [shostak](0.25 s)
bolzano_weierstrass2..................proved - complete [shostak](0.04 s)
bolzano_weierstrass3..................proved - complete [shostak](0.04 s)
bolzano_weierstrass4..................proved - complete [shostak](0.10 s)
prefix_bounded1.......................proved - complete [shostak](0.05 s)
prefix_bounded2.......................proved - complete [shostak](0.04 s)
cauchy_bounded........................proved - complete [shostak](0.12 s)
convergence_cauchy1...................proved - complete [shostak](0.23 s)
convergence_cauchy2...................proved - complete [shostak](0.06 s)
convergence_cauchy....................proved - complete [shostak](0.01 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (2.47 s)
Proof summary for theory sequence_props
incr_condition........................proved - complete [shostak](0.05 s)
decr_condition........................proved - complete [shostak](0.06 s)
strict_incr_condition.................proved - complete [shostak](0.06 s)
strict_decr_condition.................proved - complete [shostak](0.05 s)
extract_incr1.........................proved - complete [shostak](0.05 s)
extract_incr2.........................proved - complete [shostak](0.03 s)
extract_incr3.........................proved - complete [shostak](0.04 s)
unbounded_extract1....................proved - complete [shostak](0.01 s)
unbounded_extract2....................proved - complete [shostak](0.05 s)
extract_composition...................proved - complete [shostak](0.06 s)
subseq_def............................proved - complete [shostak](0.00 s)
reflexive_subseq......................proved - complete [shostak](0.03 s)
transitive_subseq.....................proved - complete [shostak](0.08 s)
extract_bij_TCC1......................proved - complete [shostak](0.04 s)
extract_bij...........................proved - complete [shostak](0.04 s)
incr_subseq...........................proved - complete [shostak](0.06 s)
decr_subseq...........................proved - complete [shostak](0.06 s)
strict_incr_subseq....................proved - complete [shostak](0.06 s)
strict_decr_subseq....................proved - complete [shostak](0.05 s)
bounded_above_subseq..................proved - complete [shostak](0.06 s)
bounded_below_subseq..................proved - complete [shostak](0.05 s)
bounded_subseq........................proved - complete [shostak](0.02 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.03 s)
Proof summary for theory real_fun_supinf
nonempty_image........................proved - complete [shostak](0.04 s)
bounded_above_image...................proved - complete [shostak](0.05 s)
bounded_below_image...................proved - complete [shostak](0.04 s)
supfun_is_bound.......................proved - complete [shostak](0.03 s)
supfun_is_sup.........................proved - complete [shostak](0.04 s)
supfun_is_sup2........................proved - complete [shostak](0.05 s)
inffun_is_bound.......................proved - complete [shostak](0.03 s)
inffun_is_inf.........................proved - complete [shostak](0.05 s)
inffun_is_inf2........................proved - complete [shostak](0.05 s)
supfun_neg_TCC1.......................proved - complete [shostak](0.01 s)
supfun_neg............................proved - complete [shostak](0.09 s)
inffun_neg_TCC1.......................proved - complete [shostak](0.01 s)
inffun_neg............................proved - complete [shostak](0.09 s)
max_upper_bound.......................proved - complete [shostak](0.03 s)
min_lower_bound.......................proved - complete [shostak](0.04 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.66 s)
Proof summary for theory monotone_subsequence
minimum_prefix........................proved - complete [shostak](0.08 s)
minimum_suffix........................proved - complete [shostak](0.07 s)
min_prop..............................proved - complete [shostak](0.05 s)
min_prop1.............................proved - complete [shostak](0.01 s)
min_prop2.............................proved - complete [shostak](0.03 s)
h_TCC1................................proved - complete [shostak](0.01 s)
h_TCC2................................proved - complete [shostak](0.01 s)
h_increasing..........................proved - complete [shostak](0.03 s)
hseq_extraction.......................proved - complete [shostak](0.01 s)
hseq_increasing.......................proved - complete [shostak](0.10 s)
no_minimum............................proved - complete [shostak](0.01 s)
pick_prop.............................proved - complete [shostak](0.05 s)
pick_prop1............................proved - complete [shostak](0.02 s)
pick_prop2............................proved - complete [shostak](0.01 s)
g_TCC1................................proved - complete [shostak](0.01 s)
g_TCC2................................proved - complete [shostak](0.01 s)
g_increasing..........................proved - complete [shostak](0.01 s)
gseq_extraction.......................proved - complete [shostak](0.01 s)
gseq_decreasing.......................proved - complete [shostak](0.01 s)
suffix_subseq.........................proved - complete [shostak](0.07 s)
suffix_hasmin.........................proved - complete [shostak](0.11 s)
monotone_subsequence..................proved - complete [shostak](0.05 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (0.76 s)
Proof summary for theory top_continuity
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory composition_continuous
composition_cont......................proved - complete [shostak](0.16 s)
composition_cont_set..................proved - complete [shostak](0.33 s)
composition_cont_fun..................proved - complete [shostak](0.04 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.54 s)
Proof summary for theory restriction_continuous
restrict_continuous...................proved - complete [shostak](0.16 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.16 s)
Proof summary for theory restriction_cont_fun
sub_dom...............................proved - complete [shostak](0.06 s)
restrict2_TCC1........................proved - complete [shostak](0.00 s)
restrict_cont_fun.....................proved - complete [shostak](0.15 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.21 s)
Proof summary for theory restriction_continuous2
sub_dom...............................proved - complete [shostak](0.06 s)
restrict2_TCC1........................proved - complete [shostak](0.01 s)
restrict_continuous2..................proved - complete [shostak](0.15 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.22 s)
Proof summary for theory continuous_functions_props
sub_interval..........................proved - complete [shostak](0.02 s)
R_TCC1................................proved - complete [shostak](0.13 s)
continuous_in_subintervals............proved - complete [shostak](0.14 s)
intermediate1.........................proved - complete [shostak](0.03 s)
intermediate2.........................proved - complete [shostak](0.03 s)
max_in_interval.......................proved - complete [shostak](0.08 s)
min_in_interval.......................proved - complete [shostak](0.06 s)
inj_continuous........................proved - complete [shostak](0.07 s)
inj_monotone..........................proved - complete [shostak](0.11 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.68 s)
Proof summary for theory continuity_interval
J_TCC1................................proved - complete [shostak](0.00 s)
bolz_weier............................proved - complete [shostak](0.03 s)
unbounded_sequence....................proved - complete [shostak](0.11 s)
bounded_from_above....................proved - complete [shostak](0.23 s)
bounded_from_below....................proved - complete [shostak](0.03 s)
max_extraction_TCC1...................proved - complete [shostak](0.01 s)
max_extraction........................proved - complete [shostak](0.09 s)
sup_is_reached........................proved - complete [shostak](0.22 s)
maximum_exists........................proved - complete [shostak](0.06 s)
max_pt_TCC1...........................proved - complete [shostak](0.10 s)
inf_is_reached_TCC1...................proved - complete [shostak](0.00 s)
inf_is_reached........................proved - complete [shostak](0.03 s)
minimum_exists........................proved - complete [shostak](0.02 s)
min_pt_TCC1...........................proved - complete [shostak](0.10 s)
intermediate_value1_TCC1..............proved - complete [shostak](0.00 s)
intermediate_value1_TCC2..............proved - complete [shostak](0.01 s)
intermediate_value1...................proved - complete [shostak](0.46 s)
intermediate_value2_TCC1..............proved - complete [shostak](0.01 s)
intermediate_value2...................proved - complete [shostak](0.02 s)
intermediate_value3_TCC1..............proved - complete [shostak](0.01 s)
intermediate_value3...................proved - complete [shostak](0.03 s)
intermediate_value4...................proved - complete [shostak](0.01 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.57 s)
Proof summary for theory continuity_props
continuity_limit......................proved - complete [shostak](0.12 s)
continuity_accumulation...............proved - complete [shostak](0.11 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.23 s)
Proof summary for theory interm_value_thm
interm_value1_TCC1....................proved - complete [shostak](0.12 s)
interm_value1_TCC2....................proved - complete [shostak](0.13 s)
interm_value1.........................proved - complete [shostak](0.02 s)
interm_value2_TCC1....................proved - complete [shostak](0.13 s)
interm_value2.........................proved - complete [shostak](0.02 s)
interm_value3_TCC1....................proved - complete [shostak](0.12 s)
interm_value3.........................proved - complete [shostak](0.02 s)
interm_value4.........................proved - complete [shostak](0.03 s)
interm_value5.........................proved - complete [shostak](0.35 s)
cont_intv.............................proved - complete [shostak](0.13 s)
cont_intv1............................proved - complete [shostak](0.02 s)
interm_val1...........................proved - complete [shostak](0.02 s)
interm_val2...........................proved - complete [shostak](0.03 s)
interm_val3...........................proved - complete [shostak](0.02 s)
interm_val4...........................proved - complete [shostak](0.02 s)
zeros_interm..........................proved - complete [shostak](0.09 s)
IntermediateValue.....................proved - complete [shostak](0.19 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (1.48 s)
Proof summary for theory continuous_functions_more
convergence_fun_of....................proved - complete [shostak](0.11 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.11 s)
Proof summary for theory unif_cont_fun
getem_scaf4...........................proved - complete [shostak](0.02 s)
unif_cont_interval....................proved - complete [shostak](2.60 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (2.63 s)
Proof summary for theory deriv_domain_def
connected_deriv_domain................proved - complete [shostak](0.15 s)
del_neigh_all_lem.....................proved - complete [shostak](0.16 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.31 s)
Proof summary for theory inverse_continuous_functions
inverse_incr..........................proved - complete [shostak](0.38 s)
inverse_decr..........................proved - complete [shostak](0.40 s)
inverse_continuous....................proved - complete [shostak](0.07 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.85 s)
Proof summary for theory continuous_linear
linear_cont_TCC1......................proved - complete [shostak](0.01 s)
linear_cont_TCC2......................proved - complete [shostak](0.01 s)
linear_cont...........................proved - complete [shostak](0.07 s)
cont_in_linear........................proved - complete [shostak](2.04 s)
unary_minus_dist......................proved - complete [shostak](0.02 s)
piecewise.............................proved - complete [shostak](7.01 s)
cont_piece............................proved - complete [shostak](0.44 s)
top_TCC1..............................proved - complete [shostak](0.05 s)
top_lem...............................proved - complete [shostak](0.03 s)
top_least.............................proved - complete [shostak](0.03 s)
bot_lem...............................proved - complete [shostak](0.03 s)
bot_least.............................proved - complete [shostak](0.03 s)
cont_upto_lub.........................proved - complete [shostak](0.89 s)
cont_downto_glb.......................proved - complete [shostak](0.64 s)
on_linear_top?_TCC1...................proved - complete [shostak](0.01 s)
cont_piecewise_linear.................proved - complete [shostak](0.43 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (11.74 s)
Proof summary for theory linear_functions
linear_add............................proved - complete [shostak](0.15 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.15 s)
Proof summary for theory cont_if_fun
discont_pts_lem.......................proved - complete [shostak](0.17 s)
if_fun_cont...........................proved - complete [shostak](0.62 s)
discont_pts_simple....................proved - complete [shostak](0.76 s)
prod_fun_lem..........................proved - complete [shostak](0.07 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.62 s)
Proof summary for theory continuous_lambda
id_cont...............................proved - complete [shostak](0.01 s)
const_cont............................proved - complete [shostak](0.01 s)
add_cont..............................proved - complete [shostak](0.02 s)
sub_cont..............................proved - complete [shostak](0.02 s)
neg_cont..............................proved - complete [shostak](0.01 s)
mult_cont.............................proved - complete [shostak](0.02 s)
div_cont..............................proved - complete [shostak](0.02 s)
scal_mult_cont........................proved - complete [shostak](0.02 s)
scal_div1_cont........................proved - complete [shostak](0.03 s)
scal_div2_cont........................proved - complete [shostak](0.02 s)
pow_cont_TCC1.........................proved - complete [shostak](0.01 s)
pow_cont..............................proved - complete [shostak](0.03 s)
sq_cont...............................proved - complete [shostak](0.02 s)
sqrt_cont_TCC1........................proved - complete [shostak](0.04 s)
sqrt_cont.............................proved - complete [shostak](0.04 s)
abs_cont..............................proved - complete [shostak](0.31 s)
max_cont..............................proved - complete [shostak](0.40 s)
min_cont..............................proved - complete [shostak](0.17 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (1.22 s)
Proof summary for theory sqrt_derivative
sqrt_derivable_fun_TCC1...............proved - complete [shostak](0.08 s)
sqrt_derivable_fun_TCC2...............proved - complete [shostak](0.02 s)
sqrt_derivable_fun....................proved - complete [shostak](0.21 s)
deriv_sqrt_fun_TCC1...................proved - complete [shostak](0.01 s)
deriv_sqrt_fun........................proved - complete [shostak](0.20 s)
deriv_sqrt............................proved - complete [shostak](0.04 s)
sqrt_continuous.......................proved - complete [shostak](0.01 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.57 s)
Proof summary for theory derivative_inverse
deriv_domain1.........................proved - complete [shostak](0.01 s)
deriv_domain2.........................proved - complete [shostak](0.00 s)
inverse_derivable_TCC1................proved - complete [shostak](0.01 s)
inverse_derivable_TCC2................proved - complete [shostak](0.01 s)
inverse_derivable_TCC3................proved - complete [shostak](0.00 s)
inverse_derivable_TCC4................proved - complete [shostak](0.00 s)
inverse_derivable.....................proved - complete [shostak](0.60 s)
inverse_derivable_fun.................proved - complete [shostak](0.02 s)
deriv_inverse_fun_TCC1................proved - complete [shostak](0.02 s)
deriv_inverse_fun.....................proved - complete [shostak](0.11 s)
deriv_inverse.........................proved - complete [shostak](0.02 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.80 s)
Proof summary for theory derivatives
IMP_derivatives_def_TCC1..............proved - complete [shostak](0.00 s)
IMP_derivatives_def_TCC2..............proved - complete [shostak](0.01 s)
deriv_TCC1............................proved - complete [shostak](0.01 s)
derivable_cont_fun....................proved - complete [shostak](0.04 s)
sum_derivable_fun.....................proved - complete [shostak](0.08 s)
neg_derivable_fun.....................proved - complete [shostak](0.05 s)
diff_derivable_fun....................proved - complete [shostak](0.08 s)
prod_derivable_fun....................proved - complete [shostak](0.08 s)
scal_derivable_fun....................proved - complete [shostak](0.05 s)
const_derivable_fun...................proved - complete [shostak](0.01 s)
inv_derivable_fun.....................proved - complete [shostak](0.05 s)
div_derivable_fun.....................proved - complete [shostak](0.08 s)
identity_derivable_fun................proved - complete [shostak](0.01 s)
id_derivable_fun......................proved - complete [shostak](0.00 s)
derivable_cont........................proved - complete [shostak](0.00 s)
nz_derivable_cont.....................proved - complete [shostak](0.01 s)
derivable_sum.........................proved - complete [shostak](0.01 s)
derivable_diff........................proved - complete [shostak](0.01 s)
derivable_prod........................proved - complete [shostak](0.01 s)
derivable_scal........................proved - complete [shostak](0.01 s)
derivable_neg.........................proved - complete [shostak](0.01 s)
derivable_div.........................proved - complete [shostak](0.01 s)
derivable_inv.........................proved - complete [shostak](0.08 s)
derivable_const.......................proved - complete [shostak](0.01 s)
derivable_id..........................proved - complete [shostak](0.01 s)
deriv_fun_def.........................proved - complete [shostak](0.08 s)
deriv_sum_fun.........................proved - complete [shostak](0.04 s)
deriv_neg_fun.........................proved - complete [shostak](0.02 s)
deriv_diff_fun........................proved - complete [shostak](0.04 s)
deriv_prod_fun........................proved - complete [shostak](0.07 s)
deriv_scal_fun........................proved - complete [shostak](0.03 s)
deriv_inv_fun_TCC1....................proved - complete [shostak](0.01 s)
deriv_inv_fun.........................proved - complete [shostak](0.06 s)
deriv_scaldiv_fun.....................proved - complete [shostak](0.26 s)
deriv_div_fun.........................proved - complete [shostak](0.12 s)
deriv_const_fun_TCC1..................proved - complete [shostak](0.01 s)
deriv_const_fun.......................proved - complete [shostak](0.03 s)
deriv_const_func......................proved - complete [shostak](0.01 s)
deriv_id_fun_TCC1.....................proved - complete [shostak](0.01 s)
deriv_id_fun..........................proved - complete [shostak](0.05 s)
deriv_I_fun...........................proved - complete [shostak](0.01 s)
deriv_linear_fun......................proved - complete [shostak](0.20 s)
deriv_exp_fun_TCC1....................proved - complete [shostak](0.23 s)
deriv_exp_fun.........................proved - complete [shostak](0.48 s)
deriv_x_n_TCC1........................proved - complete [shostak](0.01 s)
deriv_x_n_TCC2........................proved - complete [shostak](0.22 s)
deriv_x_n.............................proved - complete [shostak](0.15 s)
deriv_x_to_n_TCC1.....................proved - complete [shostak](0.01 s)
deriv_x_to_n_TCC2.....................proved - complete [shostak](0.14 s)
deriv_x_to_n..........................proved - complete [shostak](0.19 s)
Theory totals: 50 formulas, 50 attempted, 50 succeeded (3.24 s)
Proof summary for theory derivatives_def
NQ_TCC1...............................proved - complete [shostak](0.09 s)
deriv_TCC.............................proved - complete [shostak](0.11 s)
adh_A_lem.............................proved - complete [shostak](0.14 s)
continuous_lim........................proved - complete [shostak](0.39 s)
deriv_continuous......................proved - complete [shostak](0.56 s)
derivable_continuous..................proved - complete [shostak](0.01 s)
sum_NQ................................proved - complete [shostak](0.09 s)
neg_NQ................................proved - complete [shostak](0.06 s)
diff_NQ...............................proved - complete [shostak](0.08 s)
scal_NQ...............................proved - complete [shostak](0.09 s)
const_NQ..............................proved - complete [shostak](0.05 s)
identity_NQ...........................proved - complete [shostak](0.05 s)
prod_NQ...............................proved - complete [shostak](0.05 s)
cnv_seq_prod_NQ.......................proved - complete [shostak](0.70 s)
inv_NQ................................proved - complete [shostak](0.05 s)
cnv_seq_inv_NQ........................proved - complete [shostak](0.43 s)
sum_derivable.........................proved - complete [shostak](0.02 s)
neg_derivable.........................proved - complete [shostak](0.01 s)
diff_derivable........................proved - complete [shostak](0.02 s)
prod_derivable........................proved - complete [shostak](0.20 s)
scal_derivable........................proved - complete [shostak](0.02 s)
const_derivable.......................proved - complete [shostak](0.02 s)
inv_derivable.........................proved - complete [shostak](0.06 s)
div_derivable.........................proved - complete [shostak](0.01 s)
identity_derivable....................proved - complete [shostak](0.02 s)
deriv_TCC1............................proved - complete [shostak](0.01 s)
deriv_def.............................proved - complete [shostak](0.02 s)
deriv_sum_TCC1........................proved - complete [shostak](0.01 s)
deriv_sum.............................proved - complete [shostak](0.06 s)
deriv_neg_TCC1........................proved - complete [shostak](0.01 s)
deriv_neg.............................proved - complete [shostak](0.04 s)
deriv_diff_TCC1.......................proved - complete [shostak](0.01 s)
deriv_diff............................proved - complete [shostak](0.04 s)
deriv_prod_TCC1.......................proved - complete [shostak](0.01 s)
deriv_prod............................proved - complete [shostak](0.23 s)
deriv_const_TCC1......................proved - complete [shostak](0.01 s)
deriv_const...........................proved - complete [shostak](0.04 s)
deriv_scal_TCC1.......................proved - complete [shostak](0.00 s)
deriv_scal............................proved - complete [shostak](0.05 s)
deriv_inv_TCC1........................proved - complete [shostak](0.01 s)
deriv_inv.............................proved - complete [shostak](0.12 s)
deriv_div_TCC1........................proved - complete [shostak](0.01 s)
deriv_div.............................proved - complete [shostak](0.15 s)
deriv_identity_TCC1...................proved - complete [shostak](0.01 s)
deriv_identity........................proved - complete [shostak](0.03 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (4.22 s)
Proof summary for theory derivative_props
IMP_derivatives_alt_TCC1..............proved - complete [shostak](0.00 s)
IMP_derivatives_alt_TCC2..............proved - complete [shostak](0.01 s)
deriv_domain..........................proved - complete [shostak](0.01 s)
deriv_maximum.........................proved - complete [shostak](0.98 s)
deriv_minimum.........................proved - complete [shostak](0.11 s)
mean_value_aux_TCC1...................proved - complete [shostak](0.02 s)
mean_value_aux........................proved - complete [shostak](0.48 s)
mean_value_TCC1.......................proved - complete [shostak](0.01 s)
mean_value............................proved - complete [shostak](0.42 s)
mean_value_abs_TCC1...................proved - complete [shostak](0.02 s)
mean_value_abs........................proved - complete [shostak](0.49 s)
nonneg_derivative_TCC1................proved - complete [shostak](0.01 s)
nonneg_derivative.....................proved - complete [shostak](0.37 s)
nonpos_derivative.....................proved - complete [shostak](0.37 s)
positive_derivative...................proved - complete [shostak](0.11 s)
negative_derivative...................proved - complete [shostak](0.11 s)
null_derivative.......................proved - complete [shostak](0.13 s)
minimum_derivative....................proved - complete [shostak](0.37 s)
maximum_derivative....................proved - complete [shostak](0.16 s)
strict_minimum_derivative.............proved - complete [shostak](0.08 s)
strict_maximum_derivative.............proved - complete [shostak](0.13 s)
monotonic_antideriv...................proved - complete [shostak](0.07 s)
derivative_alt_TCC1...................proved - complete [shostak](0.01 s)
derivative_alt........................proved - complete [shostak](0.42 s)
derivative_fun_alt....................proved - complete [shostak](0.13 s)
epsi_lt_le............................proved - complete [shostak](0.03 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (5.07 s)
Proof summary for theory derivatives_alt
derivative_equivalence1_TCC1..........proved - complete [shostak](0.01 s)
derivative_equivalence1_TCC2..........proved - complete [shostak](0.01 s)
derivative_equivalence1...............proved - complete [shostak](0.08 s)
derivative_equivalence2...............proved - complete [shostak](0.90 s)
derivative_equivalence3...............proved - complete [shostak](0.16 s)
epsi_eq_0.............................proved - complete [shostak](0.04 s)
derivative_squeeze....................proved - complete [shostak](0.11 s)
derivative_squeeze_delta..............proved - complete [shostak](0.23 s)
deriv_constant1.......................proved - complete [shostak](0.54 s)
deriv_constant2.......................proved - complete [shostak](0.01 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.09 s)
Proof summary for theory chain_rule
chain_rule_cnvg_TCC1..................proved - complete [shostak](0.00 s)
chain_rule_cnvg_TCC2..................proved - complete [shostak](0.01 s)
chain_rule_cnvg_TCC3..................proved - complete [shostak](0.01 s)
chain_rule_cnvg_TCC4..................proved - complete [shostak](0.01 s)
chain_rule_cnvg.......................proved - complete [shostak](0.65 s)
composition_derivable_TCC1............proved - complete [shostak](0.01 s)
composition_derivable_TCC2............proved - complete [shostak](0.01 s)
composition_derivable.................proved - complete [shostak](0.04 s)
composition_derivable_fun_TCC1........proved - complete [shostak](0.01 s)
composition_derivable_fun_TCC2........proved - complete [shostak](0.01 s)
composition_derivable_fun.............proved - complete [shostak](0.02 s)
deriv_composition_TCC1................proved - complete [shostak](0.01 s)
deriv_composition.....................proved - complete [shostak](-1.25 s)
gg_TCC1...............................proved - complete [shostak](0.00 s)
gg_TCC2...............................proved - complete [shostak](0.01 s)
deriv_comp_fun_TCC1...................proved - complete [shostak](0.01 s)
deriv_comp_fun........................proved - complete [shostak](0.05 s)
comp_derivable_fun....................proved - complete [shostak](0.01 s)
chain_rule_TCC1.......................proved - complete [shostak](0.01 s)
chain_rule............................proved - complete [shostak](0.02 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (-0.34 s)
Proof summary for theory real_fun_continuity_equiv
real_fun_continuity_equiv_TCC1........proved - complete [shostak](0.00 s)
real_fun_continuity_equiv.............proved - complete [shostak](0.50 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.50 s)
Proof summary for theory real_metric_space
real_metric_space.....................proved - complete [shostak](0.18 s)
IMP_compactness_TCC1..................proved - complete [shostak](0.01 s)
compact_induction.....................proved - complete [shostak](0.23 s)
seq_intv_scaf_TCC1....................proved - complete [shostak](0.06 s)
seq_intv_scaf_TCC2....................proved - complete [shostak](0.03 s)
seq_intv_scaf_TCC3....................proved - complete [shostak](0.10 s)
seq_intv_scaf_TCC4....................proved - complete [shostak](0.07 s)
seq_intv_scaf_TCC5....................proved - complete [shostak](0.11 s)
seq_intv_scaf_TCC6....................proved - complete [shostak](0.07 s)
seq_inv_scaf_decreasing...............proved - complete [shostak](0.65 s)
compact_seq_induction.................proved - complete [shostak](0.27 s)
closed_intervals_compact..............proved - complete [shostak](5.63 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (7.42 s)
Proof summary for theory metric_spaces_def
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory open_sets
open_ball?_lem........................proved - complete [shostak](0.05 s)
open?_lem.............................proved - complete [shostak](0.01 s)
open_intv_open........................proved - complete [shostak](0.10 s)
above_intv_open.......................proved - complete [shostak](0.04 s)
below_intv_open.......................proved - complete [shostak](0.05 s)
union_open............................proved - complete [shostak](0.08 s)
closed_intv_closed....................proved - complete [shostak](0.07 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.40 s)
Proof summary for theory compactness
IMP_metric_spaces_TCC1................proved - complete [shostak](0.01 s)
nBalls_open_cover.....................proved - complete [shostak](0.05 s)
reverse_ball_TCC1.....................proved - complete [shostak](0.03 s)
set_compact...........................proved - complete [shostak](0.21 s)
idxCover_TCC1.........................proved - complete [shostak](0.04 s)
idxCover_def..........................proved - complete [shostak](0.07 s)
set_compact_alt.......................proved - complete [shostak](0.02 s)
max_min_finite_scaf...................proved - incomplete [shostak](1.83 s)
compact_sequence_limit................proved - incomplete [shostak](0.45 s)
compact_open_increasing_seq...........proved - incomplete [shostak](0.59 s)
closed_subset_of_compact..............proved - complete [shostak](0.17 s)
compact_closed........................proved - incomplete [shostak](0.52 s)
compact_bounded.......................proved - incomplete [shostak](0.26 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (4.24 s)
Proof summary for theory metric_spaces
open_emptyset.........................proved - complete [shostak](0.01 s)
closed_emptyset.......................proved - complete [shostak](0.03 s)
complement_open.......................proved - complete [shostak](0.01 s)
complement_closed.....................proved - complete [shostak](0.01 s)
open_fullset..........................proved - complete [shostak](0.01 s)
closed_fullset........................proved - complete [shostak](0.01 s)
open_in_fullset.......................proved - complete [shostak](0.14 s)
closed_in_fullset.....................proved - complete [shostak](0.01 s)
ball_open.............................proved - complete [shostak](0.08 s)
Complement_open.......................proved - complete [shostak](0.02 s)
Complement_closed.....................proved - complete [shostak](0.03 s)
subset_is_metric_space................proved - complete [shostak](0.30 s)
open_Union_open.......................proved - complete [shostak](0.07 s)
open_Intersection_open................proved - complete [shostak](0.14 s)
closed_Union_closed...................proved - complete [shostak](0.22 s)
closed_Intersection_closed............proved - complete [shostak](0.12 s)
open_closed_difference................proved - complete [shostak](0.10 s)
closed_open_difference................proved - complete [shostak](0.08 s)
open_def..............................proved - complete [shostak](0.06 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (1.45 s)
Proof summary for theory prelude_sets_aux
complement_difference.................proved - complete [shostak](0.02 s)
Intersection_member...................proved - complete [shostak](0.01 s)
Intersection_split....................proved - complete [shostak](0.06 s)
Intersection_finite...................proved - complete [shostak](0.16 s)
Union_member..........................proved - complete [shostak](0.01 s)
Union_split...........................proved - complete [shostak](0.06 s)
Union_finite..........................proved - complete [shostak](0.09 s)
finite_Complement.....................proved - complete [shostak](0.07 s)
epsilon_to_sequence...................proved - complete [shostak](0.06 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.56 s)
Proof summary for theory continuity_ms_def
continuous_at?_TCC1...................proved - complete [shostak](0.01 s)
continuous_at?_TCC2...................proved - complete [shostak](0.01 s)
continuous_at?_TCC3...................proved - complete [shostak](0.01 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.03 s)
Proof summary for theory weierstrass_approximation
IMP_real_fun_on_compact_sets_TCC1....proved - complete [shostak]( 0.01 s)
Weierstrass_approx_combin1_TCC1......proved - complete [shostak]( 0.01 s)
Weierstrass_approx_combin1_TCC2......proved - complete [shostak]( 0.01 s)
Weierstrass_approx_combin1_TCC3......proved - complete [shostak]( 0.03 s)
Weierstrass_approx_combin1...........proved - complete [shostak]( 4.00 s)
Weierstrass_approximation_0_1........proved - incomplete [shostak](11.99 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (16.05 s)
Proof summary for theory real_fun_on_compact_sets
IMP_continuity_ms_def_TCC1............proved - complete [shostak](0.01 s)
IMP_continuity_ms_def_TCC2............proved - complete [shostak](0.00 s)
cont_on_compact_max...................proved - incomplete [shostak](7.90 s)
cont_on_compact_min...................proved - incomplete [shostak](0.92 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (8.83 s)
Proof summary for theory uniform_continuity
ds_eq_0...............................proved - complete [shostak](0.06 s)
ds_sym................................proved - complete [shostak](0.05 s)
ds_triangle...........................proved - complete [shostak](0.09 s)
dt_eq_0...............................proved - complete [shostak](0.05 s)
dt_sym................................proved - complete [shostak](0.06 s)
dt_triangle...........................proved - complete [shostak](0.08 s)
IMP_continuity_ms_TCC1................proved - complete [shostak](0.01 s)
IMP_continuity_ms_TCC2................proved - complete [shostak](0.00 s)
unif_cont_implies_cont................proved - complete [shostak](0.10 s)
Hset_def..............................proved - complete [shostak](0.09 s)
ball_cover_lem........................proved - complete [shostak](0.15 s)
compact_ball_all......................proved - complete [shostak](0.16 s)
rset_prep.............................proved - complete [shostak](0.14 s)
rset_TCC1.............................proved - complete [shostak](0.01 s)
rset_lem_TCC1.........................proved - complete [shostak](0.02 s)
rset_lem..............................proved - complete [shostak](0.03 s)
rset_finite...........................proved - complete [shostak](0.04 s)
rset_not_empty........................proved - complete [shostak](0.16 s)
Heine.................................proved - incomplete [shostak](0.58 s)
uniform_continuity_sequence...........proved - complete [shostak](0.24 s)
continuous_image_of_compact...........proved - complete [shostak](0.29 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (2.42 s)
Proof summary for theory continuity_ms
IMP_continuity_ms_def_TCC1............proved - complete [shostak](0.01 s)
IMP_continuity_ms_def_TCC2............proved - complete [shostak](0.01 s)
image_inverse_image...................proved - complete [shostak](0.03 s)
inverse_image_image...................proved - complete [shostak](0.06 s)
continuous_open_sets..................proved - complete [shostak](0.18 s)
continuous_closed_sets................proved - complete [shostak](1.20 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.49 s)
Proof summary for theory finite_sets_aux
is_finite_exists_N....................proved - complete [shostak](0.03 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.03 s)
Proof summary for theory top_metric_spaces
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory cross_metric_spaces
product_is_metric.....................proved - complete [shostak](1.07 s)
product_is_metric_square..............proved - complete [shostak](2.98 s)
euclic_linear_lemma...................proved - complete [shostak](0.37 s)
metric_equivalence_TCC1...............proved - complete [shostak](0.01 s)
metric_equivalence_TCC2...............proved - complete [shostak](0.01 s)
metric_equivalence....................proved - complete [shostak](0.96 s)
metric_equivalence2...................proved - complete [shostak](0.02 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (5.41 s)
Proof summary for theory cross_metric_cont
IMP_cross_metric_spaces_TCC1..........proved - complete [shostak](0.00 s)
IMP_cross_metric_spaces_TCC2..........proved - complete [shostak](0.01 s)
IMP_continuity_ms_def_TCC1............proved - complete [shostak](0.00 s)
IMP_continuity_ms_def_TCC2............proved - complete [shostak](0.01 s)
product_cont_equiv....................proved - complete [shostak](0.24 s)
product_cont_product_subset...........proved - complete [shostak](0.24 s)
one_variable_unif_cont_sequence.......proved - complete [shostak](0.35 s)
curried_is_uniform....................proved - complete [shostak](0.05 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.89 s)
Proof summary for theory cross_metric_uniform_continuity
IMP_cross_metric_spaces_TCC1..........proved - complete [shostak](0.00 s)
IMP_cross_metric_spaces_TCC2..........proved - complete [shostak](0.00 s)
IMP_continuity_ms_def_TCC1............proved - complete [shostak](0.01 s)
IMP_continuity_ms_def_TCC2............proved - complete [shostak](0.01 s)
multiary_Heine........................proved - incomplete [shostak](3.83 s)
multi_Heine_Corollary1................proved - incomplete [shostak](0.06 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (3.91 s)
Proof summary for theory cross_metric_real_fun
IMP_cross_metric_uniform_continuity_TCC1...proved - complete [shostak](0.00 s)
IMP_cross_metric_uniform_continuity_TCC2...proved - complete [shostak](0.01 s)
IMP_cross_metric_uniform_continuity_TCC3...proved - complete [shostak](0.18 s)
curried_min_exists....................proved - incomplete [shostak](0.19 s)
curried_min_is_cont_TCC1..............proved - incomplete [shostak](0.17 s)
curried_min_is_cont...................proved - incomplete [shostak](1.06 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.62 s)
Proof summary for theory continuity_of_max_min
IMP_continuity_ms_def_TCC1............proved - complete [shostak](0.00 s)
IMP_continuity_ms_def_TCC2............proved - complete [shostak](0.00 s)
max_min_fun_convert...................proved - complete [shostak](0.14 s)
max_fun_continuous....................proved - complete [shostak](0.72 s)
min_fun_continuous....................proved - complete [shostak](0.68 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.54 s)
Proof summary for theory ms_composition_cont
IMP_continuity_ms_TCC1................proved - complete [shostak](0.00 s)
IMP_continuity_ms_TCC2................proved - complete [shostak](0.01 s)
IMP_continuity_ms_TCC3................proved - complete [shostak](0.00 s)
composition_continuous................proved - complete [shostak](0.14 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.16 s)
Proof summary for theory metric_space_real_fun
IMP_continuity_ms_def_TCC1...........proved - complete [shostak]( 0.01 s)
IMP_continuity_ms_def_TCC2...........proved - complete [shostak]( 0.00 s)
scal_continuous......................proved - complete [shostak]( 0.34 s)
neg_continuous.......................proved - complete [shostak]( 0.13 s)
sum_continuous.......................proved - complete [shostak]( 0.18 s)
diff_continuous......................proved - complete [shostak]( 0.79 s)
prod_continuous......................proved - complete [shostak](11.05 s)
abs_comp_cont........................proved - complete [shostak]( 0.25 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (12.74 s)
Proof summary for theory inverse_fun_ms_continuous
IMP_uniform_continuity_TCC1...........proved - complete [shostak](0.01 s)
IMP_uniform_continuity_TCC2...........proved - complete [shostak](0.01 s)
image_function_continuous.............proved - incomplete [shostak](0.11 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.13 s)
Proof summary for theory convex_function_props
convex_functions_locally_bounded......proved - complete [shostak](5.94 s)
convex_diff_quot_left_lt_TCC1.........proved - complete [shostak](0.12 s)
convex_diff_quot_left_lt_TCC2.........proved - complete [shostak](0.13 s)
convex_diff_quot_left_lt..............proved - complete [shostak](2.97 s)
convex_diff_quot_right_lt_TCC1........proved - complete [shostak](0.12 s)
convex_diff_quot_right_lt.............proved - complete [shostak](3.13 s)
convex_diff_quot_increasing...........proved - complete [shostak](0.11 s)
convex_diff_quot_bounded..............proved - complete [shostak](0.86 s)
convex_functions_continuous_TCC1......proved - complete [shostak](0.01 s)
convex_functions_continuous...........proved - complete [shostak](0.56 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (13.95 s)
Proof summary for theory top_derivative
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory derivatives_lam
IMP_derivatives_TCC1..................proved - complete [shostak](0.00 s)
IMP_derivatives_TCC2..................proved - complete [shostak](0.00 s)
derivable_id_lam......................proved - complete [shostak](0.01 s)
derivable_const_lam...................proved - complete [shostak](0.01 s)
derivable_add_lam.....................proved - complete [shostak](0.02 s)
derivable_mult_lam....................proved - complete [shostak](0.02 s)
derivable_pow_lam_TCC1................proved - complete [shostak](0.01 s)
derivable_pow_lam.....................proved - complete [shostak](0.11 s)
derivable_scal1_lam...................proved - complete [shostak](0.03 s)
derivable_scal2_lam...................proved - complete [shostak](0.05 s)
derivable_neg_lam.....................proved - complete [shostak](0.01 s)
derivable_sub_lam.....................proved - complete [shostak](0.02 s)
derivable_sq_lam......................proved - complete [shostak](0.03 s)
derivable_div_lam.....................proved - complete [shostak](0.03 s)
derivable_scald1_lam..................proved - complete [shostak](0.02 s)
--> --------------------
--> maximum size reached
--> --------------------
[ Verzeichnis aufwärts0.259unsichere Verbindung
]
|
|
