|
|
|
|
Quelle analysis.summary
Sprache: unbekannt
|
|
Spracherkennung für: .summary vermutete Sprache: Unknown {[0] [0] [0]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** 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)
derivable_scald2_lam..................proved - complete [shostak](0.04 s)
deriv_id_lam_TCC1.....................proved - complete [shostak](0.00 s)
deriv_id_lam..........................proved - complete [shostak](0.01 s)
deriv_const_lam_TCC1..................proved - complete [shostak](0.01 s)
deriv_const_lam.......................proved - complete [shostak](0.01 s)
deriv_add_lam_TCC1....................proved - complete [shostak](0.01 s)
deriv_add_lam.........................proved - complete [shostak](0.02 s)
deriv_mult_lam_TCC1...................proved - complete [shostak](0.01 s)
deriv_mult_lam........................proved - complete [shostak](0.01 s)
deriv_pow_lam_TCC1....................proved - complete [shostak](0.01 s)
deriv_pow_lam_TCC2....................proved - complete [shostak](0.01 s)
deriv_pow_lam_TCC3....................proved - complete [shostak](0.00 s)
deriv_pow_lam.........................proved - complete [shostak](0.09 s)
deriv_scal1_lam_TCC1..................proved - complete [shostak](0.01 s)
deriv_scal1_lam.......................proved - complete [shostak](0.01 s)
deriv_scal2_lam_TCC1..................proved - complete [shostak](0.01 s)
deriv_scal2_lam.......................proved - complete [shostak](0.04 s)
deriv_neg_lam_TCC1....................proved - complete [shostak](0.01 s)
deriv_neg_lam.........................proved - complete [shostak](0.01 s)
deriv_sub_lam_TCC1....................proved - complete [shostak](0.01 s)
deriv_sub_lam.........................proved - complete [shostak](0.01 s)
deriv_sq_lam_TCC1.....................proved - complete [shostak](0.01 s)
deriv_sq_lam..........................proved - complete [shostak](0.08 s)
deriv_div_lam_TCC1....................proved - complete [shostak](0.01 s)
deriv_div_lam.........................proved - complete [shostak](0.12 s)
deriv_scald1_lam_TCC1.................proved - complete [shostak](0.01 s)
deriv_scald1_lam......................proved - complete [shostak](0.09 s)
deriv_scald2_lam_TCC1.................proved - complete [shostak](0.01 s)
deriv_scald2_lam......................proved - complete [shostak](0.06 s)
Theory totals: 44 formulas, 44 attempted, 44 succeeded (1.12 s)
Proof summary for theory deriv_domain
deriv_domain_real.....................proved - complete [shostak](0.05 s)
deriv_domain_nzreal...................proved - complete [shostak](0.09 s)
deriv_domain_posreal..................proved - complete [shostak](0.07 s)
deriv_domain_nnreal...................proved - complete [shostak](0.07 s)
deriv_domain_negreal..................proved - complete [shostak](0.06 s)
deriv_domain_open.....................proved - complete [shostak](0.16 s)
deriv_domain_closed...................proved - complete [shostak](0.28 s)
deriv_domain_oc.......................proved - complete [shostak](0.14 s)
deriv_domain_co.......................proved - complete [shostak](0.16 s)
deriv_domain_posreal_le...............proved - complete [shostak](0.28 s)
deriv_domain_posreal_lt...............proved - complete [shostak](0.18 s)
deriv_domain_nnreal_lt................proved - complete [shostak](0.17 s)
not_one_element_real..................proved - complete [shostak](0.01 s)
not_one_element_nzreal................proved - complete [shostak](0.01 s)
not_one_element_posreal...............proved - complete [shostak](0.02 s)
not_one_element_nnreal................proved - complete [shostak](0.02 s)
not_one_element_negreal...............proved - complete [shostak](0.02 s)
connected_real........................proved - complete [shostak](0.01 s)
connected_posreal.....................proved - complete [shostak](0.01 s)
connected_nnreal......................proved - complete [shostak](0.01 s)
connected_negreal.....................proved - complete [shostak](0.01 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (1.84 s)
Proof summary for theory deriv_domains
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory deriv_sign
IMP_derivatives_TCC1..................proved - complete [shostak](0.00 s)
IMP_derivatives_TCC2..................proved - complete [shostak](0.02 s)
sign_derivable........................proved - complete [shostak](0.44 s)
sign_derivable_fun....................proved - complete [shostak](0.01 s)
deriv_sign_TCC1.......................proved - complete [shostak](0.00 s)
deriv_sign............................proved - complete [shostak](0.61 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.08 s)
Proof summary for theory derivatives_subtype
derivable_subtype_TCC1................proved - complete [shostak](0.01 s)
derivable_subtype_TCC2................proved - complete [shostak](0.01 s)
derivable_subtype_TCC3................proved - complete [shostak](0.21 s)
derivable_subtype_TCC4................proved - complete [shostak](0.01 s)
derivable_subtype.....................proved - complete [shostak](0.35 s)
deriv_subtype_TCC1....................proved - complete [shostak](0.01 s)
deriv_subtype_TCC2....................proved - complete [shostak](0.01 s)
deriv_subtype_TCC3....................proved - complete [shostak](0.17 s)
deriv_subtype.........................proved - complete [shostak](0.55 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.33 s)
Proof summary for theory restrict2_deriv
f_TCC1................................proved - complete [shostak](0.00 s)
f_TCC2................................proved - complete [shostak](0.01 s)
sub_dom...............................proved - complete [shostak](0.12 s)
restrict2_derivable_TCC1..............proved - complete [shostak](0.01 s)
restrict2_derivable_TCC2..............proved - complete [shostak](0.00 s)
restrict2_derivable...................proved - complete [shostak](0.32 s)
restrict2_deriv_TCC1..................proved - complete [shostak](0.00 s)
restrict2_deriv.......................proved - complete [shostak](0.05 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.51 s)
Proof summary for theory polynomial_deriv
derivable_polynomial_TCC1.............proved - complete [shostak](0.05 s)
derivable_polynomial_TCC2.............proved - complete [shostak](0.01 s)
derivable_polynomial..................proved - complete [shostak](0.27 s)
deriv_polynomial_TCC1.................proved - complete [shostak](0.01 s)
deriv_polynomial_TCC2.................proved - complete [shostak](0.01 s)
deriv_polynomial......................proved - complete [shostak](0.72 s)
derivable_n_times_polynomial..........proved - complete [shostak](0.16 s)
nderiv_polynomial_TCC1................proved - complete [shostak](0.02 s)
nderiv_polynomial_TCC2................proved - complete [shostak](0.01 s)
nderiv_polynomial_TCC3................proved - complete [shostak](0.02 s)
nderiv_polynomial.....................proved - complete [shostak](1.19 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.47 s)
Proof summary for theory nth_derivatives
derivable_n_times?_TCC1...............proved - complete [shostak](0.01 s)
derivable_n_times?_TCC2...............proved - complete [shostak](0.01 s)
derivable_n_times?_TCC3...............proved - complete [shostak](0.16 s)
derivable_n_times?_TCC4...............proved - complete [shostak](0.13 s)
derivable_n_times_lem.................proved - complete [shostak](0.08 s)
derivable_n_times_def_TCC1............proved - complete [shostak](0.03 s)
derivable_n_times_def_TCC2............proved - complete [shostak](0.00 s)
derivable_n_times_def_TCC3............proved - complete [shostak](0.00 s)
derivable_n_times_def.................proved - complete [shostak](0.01 s)
nderiv_TCC1...........................proved - complete [shostak](0.02 s)
nderiv_TCC2...........................proved - complete [shostak](0.01 s)
nderiv_TCC3...........................proved - complete [shostak](0.01 s)
nderiv_TCC4...........................proved - complete [shostak](0.01 s)
nderiv_derivable_TCC1.................proved - complete [shostak](0.03 s)
nderiv_derivable_TCC2.................proved - complete [shostak](0.01 s)
nderiv_derivable_TCC3.................proved - complete [shostak](0.01 s)
nderiv_derivable......................proved - complete [shostak](0.11 s)
nderiv_derivable_aux_TCC1.............proved - complete [shostak](0.03 s)
nderiv_derivable_aux_TCC2.............proved - complete [shostak](0.02 s)
nderiv_derivable_aux_TCC3.............proved - complete [shostak](0.04 s)
nderiv_derivable_aux..................proved - complete [shostak](0.10 s)
nderiv_derivable_eqv_TCC1.............proved - complete [shostak](0.00 s)
nderiv_derivable_eqv_TCC2.............proved - complete [shostak](0.00 s)
nderiv_derivable_eqv..................proved - complete [shostak](0.09 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (0.92 s)
Proof summary for theory taylors
deriv_domain..........................proved - complete [shostak](0.00 s)
sigma_derivable_TCC1..................proved - complete [shostak](0.01 s)
sigma_derivable_TCC2..................proved - complete [shostak](0.01 s)
sigma_derivable_TCC3..................proved - complete [shostak](0.14 s)
sigma_derivable.......................proved - complete [shostak](0.22 s)
tay1_TCC1.............................proved - complete [shostak](0.01 s)
tay1..................................proved - complete [shostak](0.14 s)
tay2..................................proved - complete [shostak](0.05 s)
tay3_TCC1.............................proved - complete [shostak](0.04 s)
tay3..................................proved - complete [shostak](0.40 s)
deriv_sigma_TCC1......................proved - complete [shostak](0.01 s)
deriv_sigma_TCC2......................proved - complete [shostak](0.02 s)
deriv_sigma...........................proved - complete [shostak](0.34 s)
nderiv_term_derivable_TCC1............proved - complete [shostak](0.03 s)
nderiv_term_derivable.................proved - complete [shostak](0.15 s)
taylor_derivable_TCC1.................proved - complete [shostak](0.02 s)
taylor_derivable_TCC2.................proved - complete [shostak](0.03 s)
taylor_derivable_TCC3.................proved - complete [shostak](0.04 s)
taylor_derivable......................proved - complete [shostak](0.32 s)
deriv_nderiv_TCC1.....................proved - complete [shostak](0.03 s)
deriv_nderiv_TCC2.....................proved - complete [shostak](0.05 s)
deriv_nderiv_TCC3.....................proved - complete [shostak](0.04 s)
deriv_nderiv..........................proved - complete [shostak](0.04 s)
term_by_term_deriv_TCC1...............proved - complete [shostak](0.03 s)
term_by_term_deriv_TCC2...............proved - complete [shostak](0.04 s)
term_by_term_deriv_TCC3...............proved - complete [shostak](0.05 s)
term_by_term_deriv_TCC4...............proved - complete [shostak](0.37 s)
term_by_term_deriv....................proved - complete [shostak](1.50 s)
taylor_lemma_TCC1.....................proved - complete [shostak](0.07 s)
taylor_lemma..........................proved - complete [shostak](0.66 s)
Taylors...............................proved - complete [shostak](2.60 s)
Taylor_term_TCC1......................proved - complete [shostak](0.02 s)
Taylors_inf_TCC1......................proved - complete [shostak](0.02 s)
Taylors_inf_TCC2......................proved - complete [shostak](0.07 s)
Taylors_inf...........................proved - complete [shostak](0.39 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (7.99 s)
Proof summary for theory top_riesz_representation
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory bounded_variation
IMP_rs_partition_TCC1.................proved - complete [shostak](0.01 s)
IMP_rs_partition_TCC2.................proved - complete [shostak](0.00 s)
variation_on_TCC1.....................proved - complete [shostak](0.05 s)
variation_on_TCC2.....................proved - complete [shostak](0.03 s)
variation_on_TCC3.....................proved - complete [shostak](0.10 s)
variation_on_strictly_sort_TCC1.......proved - incomplete [shostak](0.25 s)
variation_on_strictly_sort............proved - incomplete [shostak](2.48 s)
monotonic_BV_TCC1.....................proved - complete [shostak](0.02 s)
monotonic_BV..........................proved - complete [shostak](1.24 s)
BV_bounded............................proved - complete [shostak](0.69 s)
BV_bound..............................proved - complete [shostak](0.63 s)
BV_add................................proved - complete [shostak](1.12 s)
BV_scal...............................proved - complete [shostak](1.00 s)
BV_sub................................proved - complete [shostak](0.06 s)
BV_mult...............................proved - complete [shostak](3.19 s)
variation_on_subset_TCC1..............proved - complete [shostak](0.12 s)
variation_on_subset...................proved - complete [shostak](1.45 s)
BV_subset_TCC1........................proved - complete [shostak](0.04 s)
BV_subset.............................proved - complete [shostak](0.07 s)
total_variation_TCC1..................proved - complete [shostak](0.09 s)
total_variation_TCC2..................proved - complete [shostak](0.23 s)
total_variation_TCC3..................proved - complete [shostak](0.73 s)
total_variation_approx_TCC1...........proved - complete [shostak](0.17 s)
total_variation_approx................proved - incomplete [shostak](0.21 s)
BV_decomposition......................proved - incomplete [shostak](2.88 s)
Theory totals: 25 formulas, 25 attempted, 25 succeeded (16.86 s)
Proof summary for theory rs_partition
partition_pred?_TCC1..................proved - complete [shostak](0.06 s)
partition_strictly_sort...............proved - incomplete [shostak](0.49 s)
width_TCC1............................proved - complete [shostak](0.20 s)
width_TCC2............................proved - incomplete [shostak](0.34 s)
width_lem.............................proved - incomplete [shostak](0.18 s)
width_lem_exists......................proved - incomplete [shostak](0.12 s)
parts_order...........................proved - complete [shostak](0.05 s)
parts_disjoint........................proved - complete [shostak](0.18 s)
in_sect?_TCC1.........................proved - complete [shostak](0.03 s)
part_in...............................proved - incomplete [shostak](0.20 s)
part_in_strict_left...................proved - incomplete [shostak](0.19 s)
part_not_in...........................proved - complete [shostak](0.08 s)
part_induction........................proved - complete [shostak](0.17 s)
eq_partition_TCC1.....................proved - complete [shostak](0.02 s)
eq_partition_TCC2.....................proved - complete [shostak](0.26 s)
eq_partition_TCC3.....................proved - complete [shostak](0.36 s)
eq_partition_TCC4.....................proved - complete [shostak](1.05 s)
len_eq_part...........................proved - complete [shostak](0.08 s)
eq_part_lem_a.........................proved - complete [shostak](0.09 s)
eq_part_lem_b_TCC1....................proved - complete [shostak](0.02 s)
eq_part_lem_b.........................proved - complete [shostak](0.24 s)
width_eq_part_TCC1....................proved - complete [shostak](0.03 s)
width_eq_part.........................proved - incomplete [shostak](0.43 s)
N_from_delta_TCC1.....................proved - complete [shostak](0.10 s)
N_from_delta..........................proved - incomplete [shostak](0.25 s)
partition_exists......................proved - incomplete [shostak](0.08 s)
partjoin_TCC1.........................proved - complete [shostak](0.02 s)
partjoin_TCC2.........................proved - complete [shostak](0.04 s)
partjoin_TCC3.........................proved - complete [shostak](0.44 s)
partjoin_def_TCC1.....................proved - complete [shostak](0.40 s)
partjoin_def..........................proved - complete [shostak](0.42 s)
partjoin_width_TCC1...................proved - complete [shostak](0.11 s)
partjoin_width........................proved - incomplete [shostak](1.40 s)
partition_union_TCC1..................proved - complete [shostak](0.03 s)
partition_union_TCC2..................proved - incomplete [shostak](1.47 s)
partition_union_sym...................proved - incomplete [shostak](-1.05 s)
partition_union_unique................proved - incomplete [shostak](4.54 s)
partition_union_width.................proved - incomplete [shostak](0.90 s)
partition_strictly_sort_union_TCC1....proved - incomplete [shostak](0.06 s)
partition_strictly_sort_union.........proved - incomplete [shostak](0.79 s)
partition_union_is_strictly_sort......proved - incomplete [shostak](0.27 s)
partition_union_map_TCC1..............proved - incomplete [shostak](0.74 s)
partition_union_map_unique............proved - incomplete [shostak](0.38 s)
partition_union_map_increasing........proved - incomplete [shostak](0.28 s)
partition_union_strictly_sort_map_inv...proved - incomplete [shostak](0.48 s)
partition_union_map_inv_TCC1..........proved - incomplete [shostak](2.00 s)
partition_union_map_inv_def_TCC1......proved - incomplete [shostak](0.66 s)
partition_union_map_inv_def_TCC2......proved - incomplete [shostak](0.56 s)
partition_union_map_inv_def...........proved - incomplete [shostak](1.35 s)
partition_sort_inv_map_TCC1...........proved - incomplete [shostak](0.36 s)
partition_sort_inv_map................proved - incomplete [shostak](0.79 s)
Theory totals: 51 formulas, 51 attempted, 51 succeeded (22.75 s)
Proof summary for theory riesz_bounded_functionals
IMP_riesz_linear_functionals_TCC1.....proved - complete [shostak](0.07 s)
IMP_riesz_linear_functionals_TCC2.....proved - complete [shostak](0.03 s)
IMP_riesz_linear_functionals_TCC3.....proved - complete [shostak](0.03 s)
bounded_op?_TCC1......................proved - complete [shostak](0.03 s)
op_norm_TCC1..........................proved - complete [shostak](0.94 s)
op_norm_bound.........................proved - complete [shostak](0.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.12 s)
Proof summary for theory riesz_function_sets
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory riesz_interval_funs
Intab_TCC1............................proved - complete [shostak](0.00 s)
IMP_metric_space_real_fun_TCC1........proved - complete [shostak](0.28 s)
IMP_metric_space_real_fun_TCC2........proved - complete [shostak](0.01 s)
bounded_on_int_sum_closed.............proved - complete [shostak](0.13 s)
bounded_on_int_const_closed...........proved - complete [shostak](0.14 s)
fun_norm_TCC1.........................proved - complete [shostak](0.19 s)
fun_norm_dist_TCC1....................proved - complete [shostak](0.04 s)
fun_norm_dist_TCC2....................proved - complete [shostak](0.23 s)
fun_norm_bound........................proved - complete [shostak](0.02 s)
fun_norm_zero.........................proved - complete [shostak](0.04 s)
fun_norm_scal_TCC1....................proved - complete [shostak](0.16 s)
fun_norm_scal.........................proved - complete [shostak](0.95 s)
fun_norm_triangle_TCC1................proved - complete [shostak](0.12 s)
fun_norm_triangle.....................proved - complete [shostak](0.38 s)
bounded_funs_metric_space_TCC1........proved - complete [shostak](0.01 s)
bounded_funs_metric_space.............proved - complete [shostak](0.66 s)
int_compact...........................proved - complete [shostak](0.01 s)
continuous_implies_bounded............proved - incomplete [shostak](0.40 s)
continuous_function_bounded...........proved - incomplete [shostak](0.01 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (3.80 s)
Proof summary for theory riesz_linear_functionals
additive_op?_TCC1.....................proved - complete [shostak](0.01 s)
const_inv_op?_TCC1....................proved - complete [shostak](0.01 s)
linear_op_zero_TCC1...................proved - complete [shostak](0.00 s)
linear_op_zero........................proved - complete [shostak](0.04 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.05 s)
Proof summary for theory riesz_hahn_banach
C_Bounded_Linear_Operator_TCC1........proved - incomplete [shostak](0.21 s)
B_Bounded_Linear_Operator_TCC1........proved - incomplete [shostak](0.43 s)
lesseqp_TCC1..........................proved - incomplete [shostak](0.10 s)
lesseqp_TCC2..........................proved - incomplete [shostak](0.04 s)
lesseqp_TCC3..........................proved - incomplete [shostak](0.03 s)
lesseqp_TCC4..........................proved - incomplete [shostak](0.02 s)
lesseqp_TCC5..........................proved - incomplete [shostak](0.03 s)
Hahn_Banach_partial_order.............proved - incomplete [shostak](0.31 s)
Hahn_Banach_partial_order_sub.........proved - incomplete [shostak](0.05 s)
Op_Extension_exists...................proved - incomplete [shostak](7.05 s)
Hahn_Banach_TCC1......................proved - incomplete [shostak](0.16 s)
Hahn_Banach_TCC2......................proved - incomplete [shostak](0.20 s)
Hahn_Banach...........................proved - incomplete [shostak](5.96 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (14.61 s)
Proof summary for theory riesz_representation
IMP_rs_integral_cont_TCC1............proved - complete [shostak]( 0.01 s)
IMP_rs_integral_cont_TCC2............proved - complete [shostak]( 0.01 s)
integral_norm_bounded_TCC1...........proved - complete [shostak]( 0.03 s)
integral_norm_bounded_TCC2...........proved - complete [shostak]( 0.02 s)
integral_norm_bounded_TCC3...........proved - incomplete [shostak]( 0.02 s)
integral_norm_bounded................proved - incomplete [shostak](15.87 s)
fun_to_op_TCC1.......................proved - incomplete [shostak]( 0.07 s)
fun_to_op_TCC2.......................proved - incomplete [shostak]( 0.64 s)
fun_to_op_bound_TCC1.................proved - complete [shostak]( 0.02 s)
fun_to_op_bound......................proved - incomplete [shostak]( 0.12 s)
char_fun_minus.......................proved - complete [shostak]( 0.20 s)
step_approx_TCC1.....................proved - complete [shostak]( 0.05 s)
step_approx_TCC2.....................proved - complete [shostak]( 0.05 s)
step_approx_TCC3.....................proved - complete [shostak]( 0.15 s)
step_approx_TCC4.....................proved - complete [shostak]( 2.46 s)
step_approx_def......................proved - incomplete [shostak]( 3.52 s)
IMP_riesz_bounded_functionals_TCC1...proved - incomplete [shostak]( 0.14 s)
IMP_riesz_bounded_functionals_TCC2...proved - incomplete [shostak]( 0.49 s)
riesz_representation_TCC1............proved - incomplete [shostak]( 3.69 s)
riesz_representation.................proved - incomplete [shostak](28.27 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (55.85 s)
Proof summary for theory rs_integral_cont
IMP_rs_integral_prep_TCC1............proved - complete [shostak]( 0.01 s)
IMP_rs_integral_prep_TCC2............proved - complete [shostak]( 0.00 s)
RS_integrable_cont_inc_TCC1..........proved - complete [shostak]( 0.25 s)
RS_integrable_cont_inc_TCC2..........proved - complete [shostak]( 0.02 s)
RS_integrable_cont_inc...............proved - incomplete [shostak](19.68 s)
RS_integrable_cont_BV................proved - incomplete [shostak]( 0.09 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (20.05 s)
Proof summary for theory rs_integral_prep
IMP_rs_integral_def_TCC1.............proved - complete [shostak]( 0.01 s)
IMP_rs_integral_def_TCC2.............proved - complete [shostak]( 0.00 s)
integral_const_fun...................proved - incomplete [shostak]( 3.99 s)
integral_const_restrict..............proved - incomplete [shostak]( 3.89 s)
integral_scal........................proved - incomplete [shostak](12.04 s)
integral_scal_g......................proved - incomplete [shostak]( 5.71 s)
integral_sum.........................proved - incomplete [shostak]( 3.57 s)
integral_sum_g.......................proved - incomplete [shostak]( 3.54 s)
integral?_sum........................proved - incomplete [shostak]( 0.18 s)
integral?_sum_g......................proved - incomplete [shostak]( 0.17 s)
integral_diff........................proved - incomplete [shostak]( 0.25 s)
integral_diff_g......................proved - incomplete [shostak]( 7.09 s)
integral_ge_0........................proved - incomplete [shostak]( 3.72 s)
integral_restr_eq....................proved - incomplete [shostak]( 0.04 s)
integral_bound_above.................proved - incomplete [shostak]( 0.23 s)
integral_bound_below.................proved - incomplete [shostak]( 0.19 s)
integral_le..........................proved - incomplete [shostak]( 0.08 s)
Lemma_1..............................proved - incomplete [shostak]( 9.50 s)
integrable_lem.......................proved - incomplete [shostak](16.01 s)
integrable_lem2_alt..................proved - incomplete [shostak](38.51 s)
integrable_lem2......................proved - incomplete [shostak](36.47 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (145.20 s)
Proof summary for theory rs_integral_def
IMP_rs_partition_TCC1................proved - complete [shostak]( 0.01 s)
IMP_rs_partition_TCC2................proved - complete [shostak]( 0.00 s)
xis_join_TCC1........................proved - complete [shostak]( 0.02 s)
xis_join_TCC2........................proved - complete [shostak]( 0.69 s)
xis_lem..............................proved - complete [shostak]( 0.05 s)
xis_bounded..........................proved - complete [shostak]( 0.10 s)
Rie_sum_TCC1.........................proved - complete [shostak]( 0.04 s)
Rie_sum_TCC2.........................proved - complete [shostak]( 0.04 s)
Rie_sum_TCC3.........................proved - complete [shostak]( 0.04 s)
Rie_sec_TCC1.........................proved - complete [shostak]( 0.04 s)
Rie_sec_TCC2.........................proved - complete [shostak]( 0.04 s)
Rie_sum_alt_TCC1.....................proved - complete [shostak]( 0.13 s)
Rie_sum_alt_TCC2.....................proved - complete [shostak]( 0.13 s)
Rie_sum_alt_TCC3.....................proved - complete [shostak]( 0.12 s)
Rie_sum_alt_TCC4.....................proved - complete [shostak]( 0.16 s)
Rie_sum_alt_lem......................proved - complete [shostak]( 0.50 s)
Riemann_sum_strictly_sort_TCC1.......proved - incomplete [shostak]( 0.31 s)
Riemann_sum_strictly_sort............proved - incomplete [shostak]( 9.30 s)
x_in_TCC1............................proved - complete [shostak]( 0.07 s)
pick_one_TCC1........................proved - complete [shostak]( 0.07 s)
gen_xis_TCC1.........................proved - complete [shostak]( 0.04 s)
gen_xis_TCC2.........................proved - complete [shostak]( 0.15 s)
Riemann?_Rie.........................proved - complete [shostak]( 0.05 s)
integral_unique......................proved - incomplete [shostak]( 2.30 s)
integral_TCC1........................proved - incomplete [shostak]( 0.06 s)
integral_def.........................proved - incomplete [shostak]( 0.05 s)
integral_restrict_eq.................proved - incomplete [shostak]( 0.53 s)
Integral_TCC1........................proved - incomplete [shostak]( 0.02 s)
Integral_TCC2........................proved - incomplete [shostak]( 1.80 s)
Integral_TCC3........................proved - incomplete [shostak]( 1.86 s)
Rie_sum_extend_union_TCC1............proved - incomplete [shostak]( 0.08 s)
Rie_sum_extend_union_TCC2............proved - incomplete [shostak]( 0.07 s)
Rie_sum_extend_union_TCC3............proved - incomplete [shostak]( 0.35 s)
Rie_sum_extend_union.................proved - incomplete [shostak](33.33 s)
Rie_sum_restrict_union_TCC1..........proved - incomplete [shostak]( 0.67 s)
Rie_sum_restrict_union...............proved - incomplete [shostak]( 7.23 s)
Rie_sum_diff_extend_union............proved - incomplete [shostak](50.75 s)
Theory totals: 37 formulas, 37 attempted, 37 succeeded (111.22 s)
Proof summary for theory top_integral
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory integral
IMP_integral_def_TCC1................proved - complete [shostak]( 0.01 s)
IMP_integral_def_TCC2................proved - complete [shostak]( 0.01 s)
IMP_continuous_functions_more_TCC1...proved - complete [shostak]( 0.01 s)
IMP_continuous_functions_more_TCC2...proved - complete [shostak]( 0.01 s)
Integrable?_a_to_a...................proved - incomplete [shostak]( 0.01 s)
Integrable?_inside...................proved - incomplete [shostak]( 0.03 s)
Integral_a_to_a_TCC1.................proved - incomplete [shostak](74.15 s)
Integral_a_to_a......................proved - incomplete [shostak]( 0.02 s)
Integral_const_fun...................proved - incomplete [shostak]( 0.12 s)
Integral_const_restrict..............proved - incomplete [shostak]( 0.39 s)
Integral_rev.........................proved - incomplete [shostak](73.32 s)
continuous_Integrable?...............proved - incomplete [shostak]( 0.06 s)
cont_Integrable?.....................proved - incomplete [shostak]( 0.02 s)
cont_fun_Integrable?.................proved - incomplete [shostak]( 0.02 s)
Integral_scal........................proved - incomplete [shostak]( 0.13 s)
Integral_sum.........................proved - incomplete [shostak]( 0.14 s)
Integral_diff........................proved - incomplete [shostak]( 0.16 s)
Integral_split.......................proved - incomplete [shostak]( 0.39 s)
Integral_chg_one_pt..................proved - incomplete [shostak]( 0.10 s)
Integral_ge_0........................proved - incomplete [shostak]( 0.29 s)
Integral_ge_0_open...................proved - incomplete [shostak]( 0.14 s)
Integral_bound.......................proved - incomplete [shostak]( 0.16 s)
Integral_bounded.....................proved - incomplete [shostak]( 0.32 s)
Integral_le..........................proved - incomplete [shostak]( 0.07 s)
Integrable_bounded_TCC1..............proved - incomplete [shostak]( 0.03 s)
Integrable_bounded_TCC2..............proved - incomplete [shostak]( 0.04 s)
Integrable_bounded...................proved - incomplete [shostak]( 3.87 s)
Integral_neg.........................proved - incomplete [shostak]( 0.07 s)
Integral_restr_eq....................proved - incomplete [shostak]( 0.11 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (154.20 s)
Proof summary for theory integral_def
partition_TCC1........................proved - complete [shostak](0.03 s)
partition_TCC2........................proved - complete [shostak](0.04 s)
partition_TCC3........................proved - complete [shostak](0.05 s)
partition_TCC4........................proved - complete [shostak](0.07 s)
width_TCC1............................proved - complete [shostak](0.09 s)
width_TCC2............................proved - complete [shostak](0.09 s)
width_TCC3............................proved - complete [shostak](0.18 s)
width_TCC4............................proved - incomplete [shostak](0.18 s)
width_lem_TCC1........................proved - complete [shostak](0.01 s)
width_lem_TCC2........................proved - complete [shostak](0.01 s)
width_lem.............................proved - incomplete [shostak](0.22 s)
parts_order...........................proved - complete [shostak](0.18 s)
parts_order_le........................proved - complete [shostak](0.03 s)
parts_disjoint_TCC1...................proved - complete [shostak](0.01 s)
parts_disjoint_TCC2...................proved - complete [shostak](0.01 s)
parts_disjoint_TCC3...................proved - complete [shostak](0.01 s)
parts_disjoint_TCC4...................proved - complete [shostak](0.02 s)
parts_disjoint........................proved - complete [shostak](0.20 s)
in_sect?_TCC1.........................proved - complete [shostak](0.02 s)
part_in_TCC1..........................proved - complete [shostak](0.02 s)
part_in_TCC2..........................proved - complete [shostak](0.01 s)
part_in...............................proved - complete [shostak](0.29 s)
part_not_in_TCC1......................proved - complete [shostak](0.04 s)
part_not_in_TCC2......................proved - complete [shostak](0.04 s)
part_not_in...........................proved - complete [shostak](0.08 s)
part_induction_TCC1...................proved - complete [shostak](0.08 s)
part_induction_TCC2...................proved - complete [shostak](0.11 s)
part_induction........................proved - complete [shostak](0.18 s)
eq_partition_TCC1.....................proved - complete [shostak](0.01 s)
eq_partition_TCC2.....................proved - complete [shostak](0.29 s)
eq_partition_TCC3.....................proved - complete [shostak](0.47 s)
xis?_TCC1.............................proved - complete [shostak](0.00 s)
xis_lem_TCC1..........................proved - complete [shostak](0.02 s)
xis_lem_TCC2..........................proved - complete [shostak](0.06 s)
xis_lem...............................proved - complete [shostak](0.05 s)
Rie_sum_TCC1..........................proved - complete [shostak](0.03 s)
Rie_sum_TCC2..........................proved - complete [shostak](0.03 s)
Rie_sum_TCC3..........................proved - complete [shostak](0.04 s)
Rie_sum_TCC4..........................proved - complete [shostak](0.03 s)
Rie_sum_TCC5..........................proved - complete [shostak](0.02 s)
Rie_sum_TCC6..........................proved - complete [shostak](0.02 s)
Rie_sec_TCC1..........................proved - complete [shostak](0.02 s)
Rie_sec_TCC2..........................proved - complete [shostak](0.02 s)
Rie_sec_TCC3..........................proved - complete [shostak](0.03 s)
Rie_sum_alt_TCC1......................proved - complete [shostak](0.10 s)
Rie_sum_alt_TCC2......................proved - complete [shostak](0.10 s)
Rie_sum_alt_TCC3......................proved - complete [shostak](0.08 s)
Rie_sum_alt_TCC4......................proved - complete [shostak](0.13 s)
Rie_sum_alt_lem.......................proved - complete [shostak](0.64 s)
x_in_TCC1.............................proved - complete [shostak](0.07 s)
pick_one_TCC1.........................proved - complete [shostak](0.14 s)
gen_xis_TCC1..........................proved - complete [shostak](0.29 s)
len_eq_part...........................proved - complete [shostak](0.05 s)
eq_part_lem_a_TCC1....................proved - complete [shostak](0.06 s)
eq_part_lem_a.........................proved - complete [shostak](0.07 s)
eq_part_lem_b_TCC1....................proved - complete [shostak](0.05 s)
eq_part_lem_b.........................proved - complete [shostak](0.24 s)
width_eq_part_TCC1....................proved - complete [shostak](0.02 s)
width_eq_part.........................proved - incomplete [shostak](0.50 s)
N_from_delta_TCC1.....................proved - complete [shostak](0.08 s)
N_from_delta..........................proved - incomplete [shostak](0.26 s)
Riemann?_Rie..........................proved - complete [shostak](0.02 s)
integral_unique.......................proved - incomplete [shostak](1.28 s)
integral_TCC1.........................proved - incomplete [shostak](0.04 s)
integral_def..........................proved - incomplete [shostak](0.05 s)
integral_restrict_eq..................proved - incomplete [shostak](0.82 s)
Integral_TCC1.........................proved - incomplete [shostak](0.01 s)
Integral_TCC2.........................proved - incomplete [shostak](0.07 s)
Integral_TCC3.........................proved - incomplete [shostak](0.13 s)
Integrable?_rew.......................proved - incomplete [shostak](0.02 s)
Integral_rew_TCC1.....................proved - incomplete [shostak](0.14 s)
Integral_rew..........................proved - incomplete [shostak](0.02 s)
Theory totals: 72 formulas, 72 attempted, 72 succeeded (8.94 s)
Proof summary for theory integral_cont
IMP_integral_cont_scaf_TCC1..........proved - complete [shostak]( 0.01 s)
IMP_integral_cont_scaf_TCC2..........proved - complete [shostak]( 0.00 s)
in_interval_TCC1.....................proved - complete [shostak]( 0.02 s)
in_interval_TCC2.....................proved - complete [shostak]( 0.01 s)
in_interval..........................proved - complete [shostak]( 0.10 s)
continuous_integrable................proved - incomplete [shostak](64.57 s)
cont_fun_integrable..................proved - incomplete [shostak]( 0.02 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (64.73 s)
Proof summary for theory integral_cont_scaf
IMP_integral_prep_TCC1................proved - complete [shostak](0.00 s)
IMP_integral_prep_TCC2................proved - complete [shostak](0.01 s)
adh_lem...............................proved - complete [shostak](0.10 s)
cont_restrict.........................proved - complete [shostak](0.15 s)
cont_interv_TCC1......................proved - complete [shostak](0.03 s)
cont_interv_TCC2......................proved - complete [shostak](0.05 s)
cont_interv...........................proved - complete [shostak](3.06 s)
fmin_nonempty_TCC1....................proved - complete [shostak](0.06 s)
fmin_nonempty_TCC2....................proved - complete [shostak](0.05 s)
fmin_nonempty_TCC3....................proved - complete [shostak](0.15 s)
fmin_nonempty_TCC4....................proved - complete [shostak](0.09 s)
fmin_nonempty_TCC5....................proved - complete [shostak](0.06 s)
fmin_nonempty.........................proved - complete [shostak](5.53 s)
fmax_nonempty_TCC1....................proved - complete [shostak](0.06 s)
fmax_nonempty.........................proved - complete [shostak](5.55 s)
fmin_TCC1.............................proved - complete [shostak](0.02 s)
fmin_TCC2.............................proved - complete [shostak](0.01 s)
fmin_TCC3.............................proved - complete [shostak](0.11 s)
fmin_TCC4.............................proved - complete [shostak](0.25 s)
fmin_TCC5.............................proved - complete [shostak](0.06 s)
fmin_TCC6.............................proved - complete [shostak](1.64 s)
fmax_TCC1.............................proved - complete [shostak](0.06 s)
fmax_TCC2.............................proved - complete [shostak](1.64 s)
fmax_step.............................proved - complete [shostak](7.53 s)
fmin_step.............................proved - complete [shostak](7.59 s)
fmax_ge...............................proved - complete [shostak](2.41 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (36.27 s)
Proof summary for theory integral_prep
IMP_integral_def_TCC1...............proved - complete [shostak]( 0.01 s)
IMP_integral_def_TCC2...............proved - complete [shostak]( 0.01 s)
integral_const_fun..................proved - incomplete [shostak]( 21.13 s)
integral_const_restrict.............proved - incomplete [shostak]( 18.24 s)
integral_scal.......................proved - incomplete [shostak](123.48 s)
integral_sum........................proved - incomplete [shostak]( 14.23 s)
integral?_sum.......................proved - incomplete [shostak]( 0.15 s)
integral_diff.......................proved - incomplete [shostak]( 0.24 s)
integral_ge_0.......................proved - incomplete [shostak]( 15.12 s)
integral_jmp........................proved - incomplete [shostak]( 60.57 s)
integral_chg_one_pt.................proved - incomplete [shostak]( 0.17 s)
integral_restr_eq...................proved - incomplete [shostak]( 0.25 s)
integral_bound......................proved - incomplete [shostak]( 0.35 s)
integral_bound_abs..................proved - incomplete [shostak]( 0.09 s)
integral_le.........................proved - incomplete [shostak]( 0.09 s)
Lemma_1.............................proved - incomplete [shostak](186.38 s)
integrable_lem......................proved - incomplete [shostak]( 42.99 s)
gxis_TCC1...........................proved - complete [shostak]( 0.03 s)
gxis_TCC2...........................proved - complete [shostak]( 0.02 s)
gxis_TCC3...........................proved - complete [shostak]( 0.04 s)
gxis_TCC4...........................proved - complete [shostak]( 0.09 s)
gxis_TCC5...........................proved - complete [shostak]( 0.04 s)
gxis_TCC6...........................proved - complete [shostak]( 0.14 s)
gxis_TCC7...........................proved - complete [shostak]( 5.20 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (489.04 s)
Proof summary for theory integral_step
IMP_step_fun_def_TCC1...............proved - complete [shostak]( 0.01 s)
IMP_step_fun_def_TCC2...............proved - complete [shostak]( 0.00 s)
sigma_0_m1_TCC1.....................proved - complete [shostak]( 0.01 s)
sigma_0_m1_TCC2.....................proved - complete [shostak]( 0.01 s)
sigma_0_m1_TCC3.....................proved - complete [shostak]( 0.02 s)
sigma_0_m1..........................proved - complete [shostak]( 0.02 s)
pick_TCC1...........................proved - complete [shostak]( 0.01 s)
pick_TCC2...........................proved - complete [shostak]( 0.01 s)
pick_TCC3...........................proved - complete [shostak]( 0.01 s)
pick_TCC4...........................proved - complete [shostak]( 0.30 s)
stp_sect_TCC1.......................proved - complete [shostak]( 0.03 s)
stp_sect_TCC2.......................proved - complete [shostak]( 0.04 s)
stp_sect_TCC3.......................proved - complete [shostak]( 0.04 s)
stp_sect_lem_TCC1...................proved - complete [shostak]( 0.02 s)
stp_sect_lem........................proved - complete [shostak]( 2.22 s)
sigma_stp_sect_TCC1.................proved - complete [shostak]( 0.05 s)
sigma_stp_sect_TCC2.................proved - complete [shostak]( 0.06 s)
sigma_stp_sect......................proved - complete [shostak]( 2.74 s)
integral_stp_sect_TCC1..............proved - complete [shostak]( 0.01 s)
integral_stp_sect_TCC2..............proved - complete [shostak]( 0.01 s)
integral_stp_sect...................proved - incomplete [shostak]( 0.46 s)
sumof_TCC1..........................proved - complete [shostak]( 0.01 s)
sumof_TCC2..........................proved - complete [shostak]( 0.02 s)
sigma_sumof_TCC1....................proved - complete [shostak]( 0.04 s)
sigma_sumof.........................proved - complete [shostak]( 10.03 s)
integrable_sumof....................proved - incomplete [shostak]( -0.71 s)
integral_sumof_TCC1.................proved - incomplete [shostak]( 0.05 s)
integral_sumof_TCC2.................proved - complete [shostak]( 2.15 s)
integral_sumof_TCC3.................proved - complete [shostak]( 0.09 s)
integral_sumof_TCC4.................proved - complete [shostak]( 0.11 s)
integral_sumof......................proved - incomplete [shostak]( 3.75 s)
step_fun_is_sumof_n_TCC1............proved - complete [shostak]( 10.78 s)
step_fun_is_sumof_n.................proved - complete [shostak]( 10.66 s)
step_fun_is_sumof_TCC1..............proved - complete [shostak]( 0.03 s)
step_fun_is_sumof...................proved - complete [shostak]( 0.11 s)
step_function_integrable?...........proved - incomplete [shostak]( 1.33 s)
step_function_on_integral_TCC1......proved - incomplete [shostak]( 1.04 s)
step_function_on_integral_TCC2......proved - complete [shostak]( 10.75 s)
step_function_on_integral_TCC3......proved - complete [shostak]( 10.77 s)
step_function_on_integral_TCC4......proved - complete [shostak]( 10.78 s)
step_function_on_integral_TCC5......proved - complete [shostak]( 10.79 s)
step_function_on_integral_TCC6......proved - complete [shostak]( 10.78 s)
step_function_on_integral_TCC7......proved - complete [shostak]( 8.87 s)
step_function_on_integral...........proved - incomplete [shostak]( 0.76 s)
step_to_integrable..................proved - incomplete [shostak](115.77 s)
Theory totals: 45 formulas, 45 attempted, 45 succeeded (224.85 s)
Proof summary for theory step_fun_def
IMP_integral_def_TCC1.................proved - complete [shostak](0.00 s)
IMP_integral_def_TCC2.................proved - complete [shostak](0.01 s)
step_fun?_lem.........................proved - complete [shostak](0.25 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.26 s)
Proof summary for theory integral_pulse
IMP_integral_prep_TCC1..............proved - complete [shostak]( 0.00 s)
IMP_integral_prep_TCC2..............proved - complete [shostak]( 0.01 s)
EX3p_TCC1...........................proved - complete [shostak]( 0.03 s)
EX3p_TCC2...........................proved - complete [shostak]( 0.05 s)
EX3p_TCC3...........................proved - complete [shostak]( 0.02 s)
EX3p_TCC4...........................proved - complete [shostak]( 0.10 s)
EX3p_TCC5...........................proved - complete [shostak]( 0.12 s)
EX3p_TCC6...........................proved - complete [shostak]( 0.09 s)
EX3p_TCC7...........................proved - complete [shostak]( 0.10 s)
EX3p................................proved - complete [shostak]( 1.39 s)
EXse_TCC1...........................proved - incomplete [shostak]( 0.03 s)
EXse................................proved - incomplete [shostak]( 8.97 s)
Example_3_TCC1......................proved - complete [shostak]( 0.01 s)
Example_3...........................proved - incomplete [shostak](150.85 s)
zero_except?_integrable.............proved - incomplete [shostak]( 0.05 s)
zero_not_intv?_integrable_TCC1......proved - complete [shostak]( 0.02 s)
zero_not_intv?_integrable...........proved - incomplete [shostak]( 0.22 s)
zero_except_intv?_integrable_TCC1...proved - complete [shostak]( 0.01 s)
zero_except_intv?_integrable........proved - incomplete [shostak]( 74.53 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (236.60 s)
Proof summary for theory interval_minmax
min_x_TCC1............................proved - complete [shostak](0.59 s)
max_x_TCC1............................proved - complete [shostak](0.60 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.19 s)
Proof summary for theory integral_split
partition_join_TCC1..................proved - complete [shostak]( 0.01 s)
partition_join_TCC2..................proved - complete [shostak]( 0.01 s)
partition_join_TCC3..................proved - incomplete [shostak]( 0.06 s)
partition_join.......................proved - incomplete [shostak](69.04 s)
iss_prep_TCC1........................proved - complete [shostak]( 0.03 s)
iss_prep.............................proved - complete [shostak]( 6.79 s)
integrable_split_step_TCC1...........proved - incomplete [shostak]( 0.01 s)
integrable_split_step................proved - incomplete [shostak](25.79 s)
integrable_split.....................proved - incomplete [shostak]( 1.01 s)
integral_split.......................proved - incomplete [shostak](13.76 s)
integrable?_split_TCC1...............proved - complete [shostak]( 0.02 s)
integrable?_split....................proved - incomplete [shostak]( 0.92 s)
integrable?_inside_TCC1..............proved - complete [shostak]( 0.03 s)
integrable?_inside_TCC2..............proved - complete [shostak]( 0.01 s)
integrable?_inside_TCC3..............proved - complete [shostak]( 0.01 s)
integrable?_inside...................proved - incomplete [shostak]( 0.04 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (117.52 s)
Proof summary for theory integral_split_scaf
IMP_step_fun_def_TCC1................proved - complete [shostak]( 0.01 s)
IMP_step_fun_def_TCC2................proved - complete [shostak]( 0.01 s)
diff_step_is_step_on.................proved - complete [shostak]( 6.27 s)
se_not_on_TCC1.......................proved - complete [shostak]( 0.03 s)
se_not_on............................proved - complete [shostak]( 2.18 s)
find_P_sec_TCC1......................proved - complete [shostak]( 0.01 s)
find_P_sec_TCC2......................proved - complete [shostak]( 0.02 s)
find_P_sec_TCC3......................proved - complete [shostak]( 1.74 s)
find_P_sec_TCC4......................proved - complete [shostak]( 3.16 s)
find_P_sec_lem_TCC1..................proved - complete [shostak]( 0.04 s)
find_P_sec_lem_TCC2..................proved - complete [shostak]( 0.07 s)
find_P_sec_lem.......................proved - complete [shostak]( 0.04 s)
find_P_sec_in_TCC1...................proved - complete [shostak]( 0.07 s)
find_P_sec_in........................proved - complete [shostak]( 5.54 s)
F1_TCC1..............................proved - complete [shostak]( 0.03 s)
F1_TCC2..............................proved - complete [shostak]( 0.03 s)
F1_TCC3..............................proved - complete [shostak]( 0.08 s)
F1_TCC4..............................proved - complete [shostak]( 2.68 s)
F1_TCC5..............................proved - complete [shostak]( 2.80 s)
F1_F2_lem_TCC1.......................proved - incomplete [shostak]( 0.03 s)
F1_F2_lem............................proved - incomplete [shostak](25.75 s)
epsilon_is_0.........................proved - complete [shostak]( 0.05 s)
F2_F1_step_function_on...............proved - incomplete [shostak]( 0.28 s)
integrable_F2_F1.....................proved - incomplete [shostak]( 1.25 s)
integral_F2_F1_TCC1..................proved - incomplete [shostak]( 0.05 s)
integral_F2_F1_TCC2..................proved - incomplete [shostak](74.32 s)
integral_F2_F1_TCC3..................proved - incomplete [shostak](72.31 s)
integral_F2_F1_TCC4..................proved - incomplete [shostak](74.32 s)
integral_F2_F1_TCC5..................proved - incomplete [shostak]( 0.03 s)
integral_F2_F1_TCC6..................proved - incomplete [shostak](72.34 s)
integral_F2_F1_TCC7..................proved - incomplete [shostak]( 0.79 s)
integral_F2_F1_TCC8..................proved - incomplete [shostak]( 0.03 s)
integral_F2_F1.......................proved - incomplete [shostak](17.26 s)
se_prep..............................proved - incomplete [shostak](32.03 s)
get_xp_TCC1..........................proved - incomplete [shostak]( 0.03 s)
get_xp_TCC2..........................proved - incomplete [shostak]( 0.05 s)
get_xp_TCC3..........................proved - incomplete [shostak](27.20 s)
get_xpp_TCC1.........................proved - incomplete [shostak]( 5.35 s)
lt_via_epsi..........................proved - incomplete [shostak]( 0.02 s)
sigma_all_parts_TCC1.................proved - incomplete [shostak]( 0.03 s)
sigma_all_parts_TCC2.................proved - incomplete [shostak]( 0.03 s)
sigma_all_parts_TCC3.................proved - incomplete [shostak]( 0.04 s)
sigma_all_parts_TCC4.................proved - incomplete [shostak]( 0.02 s)
sigma_all_parts_TCC5.................proved - incomplete [shostak]( 0.03 s)
sigma_all_parts......................proved - incomplete [shostak]( 0.33 s)
steps_exist..........................proved - incomplete [shostak](69.64 s)
partition_exists.....................proved - incomplete [shostak]( 0.67 s)
Theory totals: 47 formulas, 47 attempted, 47 succeeded (499.10 s)
Proof summary for theory integral_bounded
IMP_integral_prep_TCC1...............proved - complete [shostak]( 0.01 s)
IMP_integral_prep_TCC2...............proved - complete [shostak]( 0.00 s)
int_to_bnd_TCC1......................proved - incomplete [shostak]( 0.03 s)
int_to_bnd_TCC2......................proved - incomplete [shostak]( 0.05 s)
int_to_bnd...........................proved - incomplete [shostak](29.50 s)
bounded_on_all?_TCC1.................proved - complete [shostak]( 0.02 s)
bounded_on_all?_TCC2.................proved - complete [shostak]( 0.05 s)
bounded_on_all_lem...................proved - incomplete [shostak]( 0.10 s)
MINj_prep_TCC1.......................proved - complete [shostak]( 0.05 s)
MINj_prep............................proved - complete [shostak]( 0.32 s)
MINj_TCC1............................proved - complete [shostak]( 0.02 s)
MINj_TCC2............................proved - complete [shostak]( 0.09 s)
MINj_lem.............................proved - complete [shostak]( 0.14 s)
MAXj_TCC1............................proved - complete [shostak]( 0.08 s)
MAXj_lem.............................proved - complete [shostak]( 0.15 s)
MIN_ALL_TCC1.........................proved - complete [shostak]( 0.18 s)
MAX_ALL_TCC1.........................proved - complete [shostak]( 0.18 s)
MIN_ALL_lem..........................proved - incomplete [shostak]( 2.05 s)
MAX_ALL_lem..........................proved - incomplete [shostak]( 2.03 s)
bounded_on_all_is....................proved - incomplete [shostak](74.35 s)
integrable_bounded...................proved - incomplete [shostak]( 0.04 s)
bnd_on_lem...........................proved - complete [shostak]( 0.10 s)
integrable_bounded_on_all............proved - incomplete [shostak]( 0.05 s)
Theory totals: 23 formulas, 23 attempted, 23 succeeded (109.59 s)
Proof summary for theory step_fun_props
IMP_step_fun_def_TCC1................proved - complete [shostak]( 0.01 s)
IMP_step_fun_def_TCC2................proved - complete [shostak]( 0.01 s)
is_step_TCC1.........................proved - complete [shostak]( 0.32 s)
is_step_TCC2.........................proved - complete [shostak]( 0.35 s)
is_step..............................proved - complete [shostak]( 7.46 s)
UUPart_TCC1..........................proved - complete [shostak]( 0.31 s)
UUPart_TCC2..........................proved - complete [shostak]( 0.75 s)
UUPart_TCC3..........................proved - complete [shostak]( 0.37 s)
UUPart_TCC4..........................proved - complete [shostak]( 0.37 s)
UUPart_TCC5..........................proved - complete [shostak]( 0.53 s)
UUPart_TCC6..........................proved - complete [shostak]( 0.63 s)
UUPart_TCC7..........................proved - complete [shostak]( 2.45 s)
split_step_is_step_TCC1..............proved - complete [shostak]( 0.32 s)
split_step_is_step...................proved - complete [shostak]( 8.08 s)
ssis_prep............................proved - incomplete [shostak](20.76 s)
sum_step_is_step.....................proved - incomplete [shostak](18.97 s)
diff_step_is_step....................proved - incomplete [shostak](10.79 s)
step_function_subrng_TCC1............proved - complete [shostak]( 0.33 s)
step_function_subrng.................proved - complete [shostak](24.53 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (97.33 s)
Proof summary for theory step_fun_scaf
IMP_partitions_scaf_TCC1.............proved - complete [shostak]( 0.00 s)
IMP_partitions_scaf_TCC2.............proved - complete [shostak]( 0.01 s)
UP_prep..............................proved - complete [shostak]( 7.25 s)
UnionPart_TCC1.......................proved - complete [shostak]( 1.67 s)
UnionPart_TCC2.......................proved - incomplete [shostak](13.04 s)
UnionPart_lem_TCC1...................proved - incomplete [shostak]( 0.39 s)
UnionPart_lem........................proved - incomplete [shostak]( 7.80 s)
Union_sym............................proved - incomplete [shostak]( 0.58 s)
Union_lem_TCC1.......................proved - incomplete [shostak]( 0.38 s)
Union_lem_TCC2.......................proved - incomplete [shostak]( 0.39 s)
Union_lem_TCC3.......................proved - incomplete [shostak]( 0.42 s)
Union_lem_TCC4.......................proved - incomplete [shostak]( 4.30 s)
Union_lem............................proved - incomplete [shostak]( 4.11 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (40.34 s)
Proof summary for theory partitions_scaf
gen_seq_lem_TCC1......................proved - complete [shostak](0.01 s)
gen_seq_lem...........................proved - complete [shostak](0.03 s)
part2set_prep_TCC1....................proved - complete [shostak](0.02 s)
part2set_prep_TCC2....................proved - complete [shostak](0.02 s)
part2set_prep.........................proved - complete [shostak](0.06 s)
part2set_TCC1.........................proved - complete [shostak](0.06 s)
part2set_lem..........................proved - complete [shostak](0.08 s)
card_part2set.........................proved - complete [shostak](0.26 s)
minmax_part2set_TCC1..................proved - complete [shostak](0.09 s)
minmax_part2set.......................proved - incomplete [shostak](2.30 s)
part2set_TCC2.........................proved - complete [shostak](0.05 s)
set2seq_TCC1..........................proved - complete [shostak](0.01 s)
set2seq_TCC2..........................proved - complete [shostak](0.03 s)
set2seq_length........................proved - incomplete [shostak](0.19 s)
set2seq_lem...........................proved - incomplete [shostak](0.18 s)
set2seq_exists........................proved - incomplete [shostak](0.56 s)
minmax_set2seq_TCC1...................proved - incomplete [shostak](0.02 s)
minmax_set2seq_TCC2...................proved - complete [shostak](0.03 s)
minmax_set2seq........................proved - incomplete [shostak](0.30 s)
set2seq_neq_TCC1......................proved - incomplete [shostak](0.02 s)
set2seq_neq_TCC2......................proved - incomplete [shostak](0.03 s)
set2seq_neq...........................proved - incomplete [shostak](0.37 s)
sort_set2seq_lem......................proved - incomplete [shostak](0.06 s)
set2part_prep_TCC1....................proved - complete [shostak](0.02 s)
set2part_prep.........................proved - incomplete [shostak](0.31 s)
sort_set2seq_neq_TCC1.................proved - incomplete [shostak](0.03 s)
sort_set2seq_neq_TCC2.................proved - incomplete [shostak](0.02 s)
sort_set2seq_neq......................proved - incomplete [shostak](0.27 s)
set2part_TCC1.........................proved - incomplete [shostak](0.02 s)
set2part_TCC2.........................proved - incomplete [shostak](0.50 s)
set2part_length.......................proved - incomplete [shostak](0.04 s)
set2part_lem..........................proved - incomplete [shostak](0.08 s)
set2part_ix...........................proved - incomplete [shostak](0.11 s)
insert_TCC1...........................proved - complete [shostak](0.14 s)
insert_TCC2...........................proved - incomplete [shostak](3.98 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (10.30 s)
Proof summary for theory fundamental_theorem
deriv_domain..........................proved - complete [shostak](0.01 s)
IMP_derivative_props_TCC1.............proved - complete [shostak](0.01 s)
IMP_derivative_props_TCC2.............proved - complete [shostak](0.01 s)
fundamental_TCC1......................proved - incomplete [shostak](0.03 s)
fundamental_TCC2......................proved - incomplete [shostak](0.01 s)
fundamental...........................proved - incomplete [shostak](2.86 s)
fundamental2_TCC1.....................proved - incomplete [shostak](0.01 s)
fundamental2..........................proved - incomplete [shostak](0.08 s)
fundamental3_TCC1.....................proved - incomplete [shostak](0.01 s)
fundamental3..........................proved - incomplete [shostak](0.66 s)
derivable_Integrable?.................proved - incomplete [shostak](0.27 s)
fundamental3b.........................proved - incomplete [shostak](0.01 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (3.96 s)
Proof summary for theory table_of_integrals
IMP_fundamental_theorem_TCC1..........proved - complete [shostak](0.01 s)
IMP_fundamental_theorem_TCC2..........proved - complete [shostak](0.00 s)
antideriv_x_to_n_TCC1.................proved - complete [shostak](0.01 s)
antideriv_x_to_n_TCC2.................proved - complete [shostak](0.02 s)
antideriv_x_to_n......................proved - complete [shostak](3.87 s)
integral_x_to_n.......................proved - incomplete [shostak](4.01 s)
integral_linear_TCC1..................proved - incomplete [shostak](0.03 s)
integral_linear.......................proved - incomplete [shostak](0.40 s)
integral_quadratic_TCC1...............proved - complete [shostak](0.01 s)
integral_quadratic_TCC2...............proved - incomplete [shostak](0.05 s)
integral_quadratic_TCC3...............proved - incomplete [shostak](0.05 s)
integral_quadratic....................proved - incomplete [shostak](0.55 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (9.02 s)
Proof summary for theory indefinite_integral
deriv_domain..........................proved - complete [shostak](0.01 s)
IMP_integral_TCC1.....................proved - complete [shostak](0.01 s)
IMP_integral_TCC2.....................proved - complete [shostak](0.00 s)
antiderivative?_TCC1..................proved - complete [shostak](0.01 s)
antiderivative_lem....................proved - complete [shostak](0.21 s)
derivs_eq.............................proved - complete [shostak](0.02 s)
cont_fun_integrable?..................proved - incomplete [shostak](0.25 s)
integral_TCC1.........................proved - complete [shostak](0.03 s)
integral_lem..........................proved - complete [shostak](0.02 s)
deriv_integ...........................proved - complete [shostak](0.01 s)
indef_integral_thm_TCC1...............proved - complete [shostak](0.51 s)
indef_integral_thm....................proved - complete [shostak](0.02 s)
fundamental_indef_TCC1................proved - incomplete [shostak](0.01 s)
fundamental_indef.....................proved - incomplete [shostak](0.03 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.14 s)
Proof summary for theory integral_chg_var
deriv_domain_T........................proved - complete [shostak](0.08 s)
deriv_domain_U........................proved - complete [shostak](0.07 s)
int_chg_var_prep_TCC1.................proved - complete [shostak](0.01 s)
int_chg_var_prep_TCC2.................proved - complete [shostak](0.01 s)
int_chg_var_prep_TCC3.................proved - complete [shostak](0.01 s)
int_chg_var_prep......................proved - incomplete [shostak](0.07 s)
Int_chg_var_TCC1......................proved - complete [shostak](0.01 s)
Int_chg_var_TCC2......................proved - complete [shostak](0.01 s)
Int_chg_var_TCC3......................proved - incomplete [shostak](0.03 s)
Int_chg_var_TCC4......................proved - complete [shostak](0.01 s)
Int_chg_var_TCC5......................proved - complete [shostak](0.01 s)
Int_chg_var_TCC6......................proved - incomplete [shostak](0.03 s)
Int_chg_var_TCC7......................proved - complete [shostak](0.01 s)
Int_chg_var...........................proved - incomplete [shostak](0.22 s)
int_chg_var_TCC1......................proved - incomplete [shostak](0.04 s)
int_chg_var_TCC2......................proved - incomplete [shostak](0.04 s)
int_chg_var...........................proved - incomplete [shostak](0.07 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (0.74 s)
Proof summary for theory integral_diff_doms
int_diff_dom_TCC1....................proved - complete [shostak]( 0.01 s)
int_diff_dom_TCC2....................proved - complete [shostak]( 0.01 s)
int_diff_dom_TCC3....................proved - incomplete [shostak]( 0.01 s)
int_diff_dom_TCC4....................proved - incomplete [shostak]( 0.01 s)
int_diff_dom_TCC5....................proved - incomplete [shostak]( 0.02 s)
int_diff_dom_TCC6....................proved - incomplete [shostak]( 0.01 s)
int_diff_dom.........................proved - incomplete [shostak](69.55 s)
Int_diff_dom_TCC1....................proved - incomplete [shostak]( 0.01 s)
Int_diff_dom_TCC2....................proved - incomplete [shostak]( 0.01 s)
Int_diff_dom_TCC3....................proved - incomplete [shostak]( 0.01 s)
Int_diff_dom_TCC4....................proved - incomplete [shostak]( 0.01 s)
Int_diff_dom_TCC5....................proved - incomplete [shostak]( 0.03 s)
Int_diff_dom_TCC6....................proved - incomplete [shostak]( 0.04 s)
Int_diff_dom.........................proved - incomplete [shostak]( 0.10 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (69.83 s)
Proof summary for theory integral_mean_value
deriv_domain..........................proved - complete [shostak](0.09 s)
IMP_fundamental_theorem_TCC1..........proved - complete [shostak](0.00 s)
IMP_fundamental_theorem_TCC2..........proved - complete [shostak](0.01 s)
mean_value_integral_TCC1..............proved - incomplete [shostak](0.04 s)
mean_value_integral...................proved - incomplete [shostak](0.24 s)
mvi_cor1_TCC1.........................proved - incomplete [shostak](0.27 s)
mvi_cor1..............................proved - incomplete [shostak](0.11 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.76 s)
Proof summary for theory integration_by_parts
IMP_fundamental_theorem_TCC1..........proved - complete [shostak](0.00 s)
IMP_fundamental_theorem_TCC2..........proved - complete [shostak](0.00 s)
integ_parts_prep_TCC1.................proved - complete [shostak](0.01 s)
integ_parts_prep......................proved - incomplete [shostak](0.05 s)
integ_parts_TCC1......................proved - incomplete [shostak](0.03 s)
integ_parts_TCC2......................proved - incomplete [shostak](0.05 s)
integ_parts...........................proved - incomplete [shostak](0.36 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.51 s)
Grand Totals: 1540 proofs, 1540 attempted, 1540 succeeded (2724.57 s)
[Dauer der Verarbeitung: 0.28 Sekunden, vorverarbeitet 2026-04-26]
|
2026-05-26
|
|
|
|
|
