Quelle  analysis.summary   Sprache: unbekannt

*** 
*** 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)